CISPA
Browse
cispa_all_2943.pdf (342.04 kB)

Encoding Redundancy for Satisfaction-Driven Clause Learning

Download (342.04 kB)
conference contribution
posted on 2023-11-29, 18:11 authored by Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
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 satisfiable 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 first time, we are able to generate and automatically check clausal proofs for large instances of these problems.

History

Preferred Citation

Marijn Heule, Benjamin Kiesl and Armin Biere. Encoding Redundancy for Satisfaction-Driven Clause Learning. In: TACAS Tools and Algorithms for Construction and Analysis of Systems (TACAS). 2019.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

TACAS Tools and Algorithms for Construction and Analysis of Systems (TACAS)

Legacy Posted Date

2019-07-03

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_2943, title = "Encoding Redundancy for Satisfaction-Driven Clause Learning", author = "Heule, Marijn J. H. and Kiesl, Benjamin and Biere, Armin", booktitle="{TACAS Tools and Algorithms for Construction and Analysis of Systems (TACAS)}", year="2019", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC