Preprocessing of propagation redundant clauses

DOI10.1007/978-3-031-10769-6_8OpenAlexW4289104012MaRDI QIDQ2104502

Randal E. Bryant, Joseph E. Reeves, Marijn J. H. Heule

Publication date: 7 December 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_8

Mathematics Subject Classification ID

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

Related Items (2)

PReLearn ⋮ Preprocessing of propagation redundant clauses

Uses Software

• MiniSat
• Chaff
• DRAT-trim
• CaDiCaL
• SaDiCaL

Cites Work

• Non-uniqueness of minimal superpermutations
• The intractability of resolution
• Mutilated chessboard problem is exponentially hard for resolution
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• Strong extension-free proof systems
• Short proofs without new variables
• Super-Blocked Clauses
• Improved Static Symmetry Breaking for SAT
• Learning Rate Based Branching Heuristic for SAT Solvers
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Inprocessing Rules
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Evaluating CDCL Variable Scoring Schemes
• Expressing Symmetry Breaking in DRAT Proofs
• Community Structure in Industrial SAT Instances
• Narrow Proofs May Be Maximally Long
• Theory and Applications of Satisfiability Testing

This page was built for publication: Preprocessing of propagation redundant clauses