Covered clauses are not propagation redundant

DOI10.1007/978-3-030-51074-9_3OpenAlexW3038140734MaRDI QIDQ2096437

Armin Biere, Lee A. Barnett, David M. Cerna

Publication date: 9 November 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_3

zbMATH Keywords

redundancySATclause elimination

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Non-clausal redundancy properties

Uses Software

• Plingeling
• Easychair
• Treengeling
• Coprocessor
• Lingeling
• SaDiCaL

Cites Work

• Unnamed Item
• Unnamed Item
• Computer-aided proof of Erdős discrepancy properties
• The complexity of facets (and some facets of complexity)
• The intractability of resolution
• The complexity of the pigeonhole principle
• On a generalization of extended resolution
• DRAT proofs, propagation redundancy, and extended resolution
• Incremental inprocessing in SAT solving
• Strong extension-free proof systems
• What a difference a variable makes
• Short proofs without new variables
• Super-Blocked Clauses
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Inprocessing Rules
• Clause Elimination for SAT and QSAT
• Truth Assignments as Conditional Autarkies
• Blocked Clause Elimination
• Clause Elimination Procedures for CNF Formulas
• Applications of SAT Solvers to Cryptanalysis of Hash Functions
• Bounded model checking using satisfiability solving
• Encoding Redundancy for Satisfaction-Driven Clause Learning