Marijn Heule, Benjamin Kiesl, Armin Biere,
"Encoding Redundancy for Satisfaction-Driven Clause Learning"
, in TACAS'19: Proc. 25th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), Serie LNCS, Vol. 11427, Springer, Seite(n) 41-58, 2019
Encoding Redundancy for Satisfaction-Driven Clause Learning
Sprache des Titels:
Proc. 25th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19)
Satisfaction-Driven Clause Learning (SDCL) is a recent SAT solving paradigm that aggressively trims the search space of possible truth assignments. To determine if the SAT solver is currently exploring a dispensable part of the search space, SDCL uses the so-called positive reduct of a formula: The positive reduct is an easily solvable propositional formula that is satis?able if the current assignment of the solver can be safely pruned from the search space. In this paper, we present two novel variants of the positive reduct that allow for even more aggressive pruning. Using one of these variants allows SDCL to solve harder problems, in particular the well-known Tseitin formulas and mutilated chessboard problems. For the ?rst time, we are able to generate and automatically check clausal proofs for large instances of these problems.