Preprocessing of Propagation Redundant Clauses
Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant · Lecture notes in computer science · 2022
Abstract Thepropagation redundant(PR) proof system generalizes theresolutionandresolution asymmetric tautologyproof systems used byconflict-driven clause learning(CDCL) solvers. PR allows short proofs of unsatisfiability for some problems that are difficult for CDCL solvers. Previous attempts to automate PR clause learning used hand-crafted heuristics that work well on some highly-structured problems. For example, the solverSaDiCaLincorporates PR clause learning into the CDCL loop, but it cannot compete with modern CDCL solvers due to its fragile heuristics. We presentPReLearn, a preprocessing technique that learns short PR clauses. Adding these clauses to a formula reduces the search space that the solver must explore. By performing PR clause learning as a preprocessing stage, PR clauses can be found efficiently without sacrificing the robustness of modern CDCL solvers. On a large portion of SAT competition benchmarks we found that preprocessing withPReLearnimproves solver performance. In addition, there were several satisfiable and unsatisfiable formulas that could only be solved after preprocessing withPReLearn.PReLearnsupports proof logging, giving a high level of confidence in the results.