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.

- 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

- 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.

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.