Simulating strong practical proof systems with extended resolution
From MaRDI portal
Publication:2209554
DOI10.1007/s10817-020-09554-zzbMath1468.68293OpenAlexW3046591311MaRDI QIDQ2209554
Marijn J. H. Heule, Benjamin Kiesl, Adrián Rebola-Pardo, Armin Biere
Publication date: 2 November 2020
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-020-09554-z
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Classical propositional logic (03B05) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)
Related Items
Never trust your solver: certification for SAT and QBF, Clause redundancy and preprocessing in maximum satisfiability
Uses Software
Cites Work
- Unnamed Item
- Methods of cut-elimination
- Producing and verifying extremely large propositional refutations
- Computer-aided proof of Erdős discrepancy properties
- The intractability of resolution
- Efficient, verified checking of propositional proofs
- Extended resolution simulates \({\mathsf{DRAT}}\)
- Mutilated chessboard problem is exponentially hard for resolution
- On a generalization of extended resolution
- Strong extension-free proof systems
- What a difference a variable makes
- Short proofs without new variables
- Efficient certified RAT verification
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Inprocessing Rules
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Extended Resolution Proofs for Conjoining BDDs
- Blocked Clause Elimination
- Hard examples for resolution
- The relative efficiency of propositional proof systems
- GRASP: a search algorithm for propositional satisfiability
- Towards a Semantics of Unsatisfiability Proofs with Inprocessing
- The Complexity of Propositional Proofs
- A Theory of Satisfiability-Preserving Proofs in SAT Solving
- Extended Resolution Proofs for Symbolic SAT Solving with Quantification
