On Improving the Backjump Level in PB Solvers

The CDCL architecture [14] and the use of efficient data structures and heuristics [4, 16] are at the core of the practical efficiency of modern SAT solvers. Even though these solvers can deal with very large benchmarks, containing millions of variables and clauses, some relatively small problems (with only few variables and clauses) remain completely out of their reach. This is particularly true for problems that require the ability to "count", such as those known as pigeonhole-principle formulae, stating that n pigeons cannot fit into n 1 holes. For such problems, the resolution proof system used internally by SAT solvers is too weak: it can only prove unsatisfiability with an exponential number of derivation steps [7]. This has motivated the generalization of the CDCL architecture to handle pseudo-Boolean (PB) problems [18]. Doing so, one can take advantage of the strength of the cutting planes proof system [6], which p-simulates resolution: any resolution proof can be translated into a cutting planes proof of polynomial size w.r.t. the size of the original proof.