Asynchronous Multi-Core Incremental SAT Solving

Abstract. Solvers for propositional logic formulas, so called SAT solvers, are used in many practical applications. As multi-core and multi-processor hard-ware has become widely available, parallelizations of such solvers are actively researched. Such research typically ignores the incremental problem specifica-tion feature that modern SAT solvers possess. This feature is, however, crucial for many of the real-life applications of SAT solvers. Such applications include formal verification, equivalence checking, and typical artificial intelligence tasks such as scheduling, planning and reasoning. We have developed a multi-core SAT solver called Tarmo, which provides an in-terface that is compatible with conventional incremental solvers. It enables sub-stantial performance improvements for many applications, without requiring code modifications. We present the asynchronous interface, a natural extension to the conventional solver interface that allows the construction of efficient application specific parallelizations. Through the asynchronous interface multiple problems can be given to the solver simultaneously. This enables conceptually simple but efficient parallelization of the solving process. Moreover, an asynchronous solver is easier to run in parallel with other independent tasks, simplifying the con-struction of so called coarse grained parallelizations. We provide an extensive experimental evaluation to illustrate the performance of the proposed techniques.