Motivations

The last decade has witnessed an increasing interest in SAT, with a boost in the performances of SAT solvers, which has brought large previously intractable problems at the reach of state-of-the-art solvers. As a consequence, instances of some hard real-world problems --like, e.g., boolean circuit verification, planning and model checking-- have been successfully solved by encoding them into SAT. Unfortunately, simple propositional logic is often not expressive enough to solve complex real-world problems. In fact, important problems --like, e.g., reasoning in modal and description logics, resource planning, temporal reasoning, formal verification of timed systems, formal verification of circuits at an abstract level-- require determining the satisfiability of boolean combinations of ``atoms'' in some domain-specific theories --e.g., boxed atoms like $\Box_i (A_1 \vee \Box_2 A_2)$, concepts like $\exists$ CHILD MALE, unquantified mathematical expressions like $(x-y\le C)$, unquantified terms with equality and uninterpreted functions like e=select(store(a,i,e),i). This requires the ability of combining boolean reasoning with domain-specific solving.

To this extent, more recently (complete) SAT techniques --mainly DPLL and OBDDs-- have been extended and integrated with domain-specific reasoners (decision procedures, linear/integer programs, numerical algorithms, computer algebra procedures) to produce efficient ``SAT+domain specific reasoners''. Such reasoners have proven to be very effective in various fields, including those highlighted above.

In the integration schema, SAT solvers are used to enumerate complete sets of truth assignments propositionally satisfying the input formula, whose consistency in the domain theory is verified by domain-specific procedures. Unfortunately, neither the correctness/completeness nor the efficiency of the integrated systems comes straightforwardly from that of the component solvers. For instance, DPLL with pure literal rule is a correct and complete SAT solver, nevertheless it leads to incorrect integrated solvers; moreover, a very efficient DPLL implementation integrated with a very efficient domain-specific solver (say, a symplex tool) may turn out to be dramatically inefficient if the integration is done naively.

Thus, the integration of SAT techniques with domain-specific reasoners involves a set of theoretical and practical problems, solutions, techniques and tricks, coming from various application fields, which are very useful or even indispensable to know. This tutorials aims at surveying of all of them within an organic framework.