Truth Assignments as Conditional Autarkies
From MaRDI portal
Publication:3297584
DOI10.1007/978-3-030-31784-3_3zbMath1437.68132OpenAlexW2982005812MaRDI QIDQ3297584
Armin Biere, Marijn J. H. Heule, Benjamin Kiesl
Publication date: 20 July 2020
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-31784-3_3
Related Items
Uses Software
Cites Work
- Simulating circuit-level simplifications on CNF
- Solving satisfiability in less than \(2^ n\) steps
- The first collision for full SHA-1
- \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
- On a generalization of extended resolution
- Incremental inprocessing in SAT solving
- QRATPre+: effective QBF preprocessing via strong redundancy properties
- What a difference a variable makes
- Solution validation and extraction for QBF preprocessing
- Short proofs without new variables
- Efficient certified RAT verification
- A unifying principle for clause elimination in first-order logic
- Super-Blocked Clauses
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Inprocessing Rules
- Clause Elimination for SAT and QSAT
- A SAT Attack on the Erdős Discrepancy Conjecture
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
- Blocked Clause Elimination
- GRASP: a search algorithm for propositional satisfiability
- Blocked Clauses in First-Order Logic
- Clause Elimination Procedures for CNF Formulas
- Blocked Clause Elimination for QBF
- Theory and Applications of Satisfiability Testing
- Efficient verified (UN)SAT certificate checking
- Bounded model checking using satisfiability solving
- Encoding Redundancy for Satisfaction-Driven Clause Learning
