2.2 Complete Clausal Algorithms.................. 7

In the first part of this paper we survey a number of algorithms for solving the propositional satisfiability problem (SAT). We dedicate a large amount of attention to the non-clausal SAT algorithms, that is, the algorithms that work on arbitrary propositional formulas, and to the circuit SAT algorithms that work on Boolean circuit representation of formulas. We also discuss some of the non-mainstream clausal SAT algorithms. The second part of this paper discusses some of the practical applica-tions of SAT, particularly to Bounded Model Checking and to Satisfiability Modulo Theories