Research on the Satisfiability Problem, Its Implementations, and Applications

Department of Computer Science, Aalto University

Research Outline

Our research develops better methods for solving hard combinatorial problems in different areas of computer science, with a particular focus on constraint-based representation and reasoning methods. We have addressed problems arising in machine learning and probabilistic reasoning, including the structure learning problem for Markov networks.

We have observed the challenges to current constraint-based methods posed by simple graph properties. For example, solutions of structure learning for Bayesian networks and some classes of Markov networks require the acyclicity of the network itself (for Bayesian networks) or a related structure (the separator graph for Markov networks). We have identified other graph properties that pose difficulties for standard constraint-based methods, including reachability and path properties in the representation of network-structured systems such as electricity networks.

We have developed methods for handling graph properties more directly, leading to substantially better scalability than existing methods. Specifically, we have introduced high-performance SAT solvers that often handle graph properties much better than what is possible by encoding these properties as conventional clausal constraints (disjunctions of literals.) We have called this "Satisfiability modulo Graphs" because of the analogy with the "Satisfiability modulo Theories" framework.

We have implemented the results of our research as extensions to the high-performance SAT solvers MiniSAT and Glucose. The implementations currently publicly available support graph acyclicity and s-t-reachability.

Applications

The main applications for our work we see the solution of hard combinatorial problems about graphs and networked systems, as well as reasoning with very expressive knowledge representation languages.

design, analysis and control of networked systems such as telecom networks, electricity networks, water networks, transportation networks
learning and analyzing probabilistic graphical models such as Bayesian networks and Markov networks
reasoning about knowledge represented as inductive definitions or rule-based languages such as Answer Set Programming by using high performance general-purpose Boolean satisfiability solvers

The standard frameworks for solving many of these problems have been satisfiability (SAT) and Satisfiability modulo Theories (SMT). Unlike in many other important applications of SAT and SMT, such as those arising in computer-aided verification CAV or AI planning, encoding of graph properties in SAT or SMT is not very effective: either the encoding size is prohibitively high, or the inferences enabled by the encodings are weaker than what is satisfactory. This has prompted us to address the graph problems more directly in our Satisfiability modulo Graphs framework.

Downloads

Binaries (64-bit linux): graphsat_static graphsat_simp_static (version with _simp includes the variable-eliminating preprocessor from Minisat.)
Preliminary documentation
Example demonstrating the input syntax for the solvers: test.cnf
Source code for the solvers available on request. Contact Jussi Rintanen.

Publications

J. Corander, T. Janhunen, J. Rintanen, H. Nyman and J. Pensar. Learning chordal Markov networks by constraint satisfaction. In Advances in Neural Information Processing Systems 26, Proceedings of the Neural Information Processing Conference (NIPS'13), pages 1349-1357, 2014.

M. Gebser, T. Janhunen, and J. Rintanen. Answer Set Programming as SAT modulo Acyclicity. In ECAI 2014. Proceedings of the 21st European Conference on Artificial Intelligence, to appear, 2014.

M. Gebser, T. Janhunen, and J. Rintanen. ASP encodings of acyclicity properties. In Proceeding of the International Conference on Knowledge Representation and Reasoning, AAAI Press, 2014.

M. Gebser, T. Janhunen, and J. Rintanen. SAT modulo Graphs: Acyclicity. In Proceedings of the European Conference on Logic in Artificial Intelligence, Lecture Notes in Computer Science 8761, Springer-Verlag, 2014.