Simulating strong practical proof systems with extended resolution

DOI10.1007/S10817-020-09554-ZzbMATH Open1468.68293OpenAlexW3046591311MaRDI QIDQ2209554FDOQ2209554

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

Recommendations

• Extended resolution simulates \({\mathsf{DRAT}}\)
• DRAT proofs, propagation redundancy, and extended resolution
• Strong extension-free proof systems
• What a difference a variable makes
• On the power of clause-learning SAT solvers as resolution engines

zbMATH Keywords

resolutionSATproof complexitySAT solvingpropositional logicblocked 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)

Cites Work

• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Title not available (Why is that?)
• Extended Resolution Proofs for Symbolic SAT Solving with Quantification
• Hard examples for resolution
• GRASP: a search algorithm for propositional satisfiability
• Inprocessing Rules
• The relative efficiency of propositional proof systems
• The Complexity of Propositional Proofs
• Blocked Clause Elimination
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Computer-aided proof of Erdős discrepancy properties
• On a generalization of extended resolution
• The intractability of resolution
• Mutilated chessboard problem is exponentially hard for resolution
• Extended Resolution Proofs for Conjoining BDDs
• Methods of cut-elimination
• Producing and verifying extremely large propositional refutations
• Efficient certified RAT verification
• A Theory of Satisfiability-Preserving Proofs in SAT Solving
• Efficient, verified checking of propositional proofs
• Extended resolution simulates \({\mathsf{DRAT}}\)
• What a difference a variable makes
• Strong extension-free proof systems
• Short proofs without new variables
• Towards a Semantics of Unsatisfiability Proofs with Inprocessing

Cited In (4)

• Clause redundancy and preprocessing in maximum satisfiability
• Sub-core solutions of the problem of strong implementation
• Never trust your solver: certification for SAT and QBF
• Monotone simulations of non-monotone proofs.

Uses Software

• Chaff
• DRAT-trim
• SaDiCaL

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2209554)