Building Efficient Decision Procedures on top of SAT solvers

Many verification problems can be naturally represented as satisfiability problems in some decidable fragments of first order logic. Efficient decision procedures for such problems can be obtained by combining technology for prepositional satisfiability and solvers able to deal with the theory component. We provide a unifying and abstract, theory-independent perspective on the various integration schemas and techniques. Within this framework, we survey, analyze and classify the most effective integration techniques and optimizations for the development of decision procedures. We also discuss the relative benefits and drawbacks of the various techniques, and we analyze the features for SAT solvers and theory-specific solvers which make them more suitable for an integration. © Springer-Verlag Berlin Heidelberg 2006.