Detailed outline

In this tutorial we show how (complete) SAT solvers can be efficiently integrated with domain-specific procedures so that to provide efficient solvers for expressive domains:

• we briefly describe the main (complete) SAT techniques (e.g., DPLL, OBDDs, tableaux) and optimizations (e.g., backjumping, learning, splitting heuristics);
• we provide some logical foundations and basic results;
• we show how SAT procedures can be correctly and efficiently used as enumerators of truth assignments so that to be integrated with domain-specific procedures;
• we describe the main techniques and optimizations --e.g., early pruning, enhanced early pruning, domain-dependent backjumping and learning, triggering-- which maximize the benefits of the integration;
• we describe the features of SAT solvers and domain-specific reasoners which are desirable to maximize the benefits of their integration. We compare the main SAT engines (DPLL, OBDDs, tableaux) w.r.t. those features;

• we describe some examples of implemented procedures in different domains --including modal and description logics, boolean combinations of mathematical constraints-- and show how the techniques and optimizations previously described above are applied to these domains;

• we indicate the main open problems and research directions.

The tutorial is an evolution of the courses:

• ``Efficient Boolean Reasoning'', International Graduate School in Information and Communication Technologies, University of Trento, May 2003,
  
• ``SAT Beyond Propositional Satisfiability'', 14th European Summer School on Logic, Language and Information - ESSLLI 2002, August 2002
• ``SAT: Reasoning Within Booleans and Beyond'', International Graduate School in Information and Communication Technologies, University of Trento, May-June 2002,
  

both given by Roberto Sebastiani. Thus, sample material for the tutorial is that available at the addresses above.