On Efficiently Integrating Boolean and Theory-Specific Solving Procedures

Efficient decision procedures have been conceived in different communities for a very heterogeneous collection of expressive decidable theories. However, despite in the last years we have witnessed an impressive advance in the efficiency of SAT procedures, techniques for efficiently integrating boolean reasoning and theory-specific decision procedures have been deeply investigated only recently, producing impressive performance improvements when applied. The goal of this paper is to analyze, classify and represent within a uniform framework the most effective techniques which have been proposed in various communities in order to maximize the efficiency of boolean reasoning within decision procedures.