Preprocessing of propagation redundant clauses
From MaRDI portal
Publication:2104502
Recommendations
- Preprocessing of propagation redundant clauses
- Clause redundancy and preprocessing in maximum satisfiability
- scientific article; zbMATH DE number 4164189
- How to avoid the derivation of redundant clauses in reasoning systems
- Propagation via lazy clause generation
- scientific article; zbMATH DE number 1183246
- Covered clauses are not propagation redundant
- Eliminating Redundant Clauses in SAT Instances
- Recognizing unnecessary clauses in resolution based systems
Cites work
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
- Community structure in industrial SAT instances
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Evaluating CDCL variable scoring schemes
- Expressing symmetry breaking in DRAT proofs
- Improved static symmetry breaking for SAT
- Inprocessing rules
- Learning rate based branching heuristic for SAT solvers
- Mutilated chessboard problem is exponentially hard for resolution
- Narrow proofs may be maximally long
- Non-uniqueness of minimal superpermutations
- 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 intractability of resolution
- Theory and Applications of Satisfiability Testing
Cited in
(7)- PReLearn
- Preprocessing of propagation redundant clauses
- Minimizing the number of clauses by renaming
- On Incremental Pre-processing for SMT
- Removing redundancy from a clause
- Improving and understanding the power of satisfaction-driven clause learning
- Extended resolution clause learning via dual implication points
This page was built for publication: Preprocessing of propagation redundant clauses
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104502)
