Research on the Satisfiability Problem, Its Implementations, and Applications
Department of Information and Computer Science, Aalto University
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
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.
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.
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.