Preprocessing of propagation redundant clauses
From MaRDI portal
Publication:6053844
DOI10.1007/s10817-023-09681-3MaRDI QIDQ6053844
Randal E. Bryant, Joseph E. Reeves, Marijn J. H. Heule
Publication date: 24 October 2023
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Cites Work
- The intractability of resolution
- Mutilated chessboard problem is exponentially hard for resolution
- Preprocessing of propagation redundant clauses
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
- Strong extension-free proof systems
- Short proofs without new variables
- 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
- Symmetry and Satisfiability: An Update
- 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