Building a Hybrid SAT Solver via Conflict-Driven, Look-Ahead and XOR Reasoning Techniques

摘要

The paper develops a new hybrid SAT solver, called MoRsat. The framework of the solver is based on a look-ahead technique, and its core is a conflict-driven search. A look-ahead technique is used to split the original problem to sub-problems, each of them is either solved or aborted by a conflict-driven DPLL. Aborted sub-problems are solved recursively. We present new properties of XOR clauses, which are used to incorporate XOR reasoning into our conflict-driven DPLL. Compared with the latest versions of Rsat and March, the Gold Medal winners in the industrial and handmade SAT category of the SAT 2007 competition, MoRsat achieves remarkable improvements. Moreover, MoRsat can solve some industrial instances that were not solved in the SAT 2007 competition.