Simulating strong practical proof systems with extended resolution

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

zbMATH Keywords

propositional logicresolutionproof complexitySATSAT solvingblocked clausesDRATDPR

Mathematics Subject Classification ID

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 (2)

Never trust your solver: certification for SAT and QBF ⋮ Clause redundancy and preprocessing in maximum satisfiability

Uses Software

• Chaff
• DRAT-trim
• SaDiCaL

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

This page was built for publication: Simulating strong practical proof systems with extended resolution