Covered clauses are not propagation redundant

DOI10.1007/978-3-030-51074-9_3MaRDI QIDQ2096437zbMATH OpenOpenAlexFDO

Authors Lee A. Barnett, Armin Biere, 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

clause eliminationredundancySAT

Mathematics Subject Classification ID

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

Cites work

• Applications of SAT Solvers to Cryptanalysis of Hash Functions
• Blocked clause elimination
• Bounded model checking using satisfiability solving
• Clause elimination for SAT and QSAT
• Clause elimination procedures for CNF formulas
• Computer-aided proof of Erdős discrepancy properties
• DRAT proofs, propagation redundancy, and extended resolution
• Encoding Redundancy for Satisfaction-Driven Clause Learning
• scientific article; zbMATH DE number 3930351 (Why is no real title available?)
• scientific article; zbMATH DE number 3988706 (Why is no real title available?)
• Incremental inprocessing in SAT solving
• Inprocessing rules
• On a generalization of extended resolution
• Short proofs without new variables
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Strong extension-free proof systems
• Super-blocked clauses
• The complexity of facets (and some facets of complexity)
• The complexity of the pigeonhole principle
• The intractability of resolution
• Truth assignments as conditional autarkies
• What a difference a variable makes

Cited in

(4)

• Non-clausal redundancy properties
• Preprocessing of propagation redundant clauses
• Does This Set of Clauses Overlap with at Least One MUS?
• Dynamic blocked clause elimination for projected model counting

Describes a project that uses

Uses Software

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

This page was built for publication: Covered clauses are not propagation redundant

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2096437)