On Linear Resolution

DOI10.3233/SAT190112zbMath1484.03120MaRDI QIDQ5015599

Jan Johannsen, Samuel R. Buss

Publication date: 9 December 2021

Published in: Journal on Satisfiability, Boolean Modeling and Computation (Search for Journal in Brave)

zbMATH Keywords

proof complexitylinear resolutionregular resolutiontree-like resolutions-resolution

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Related Items

Between Hilbert and Gentzen: four-valued consequence systems and structural reasoning

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the power of clause-learning SAT solvers as resolution engines
• The relative complexity of analytic tableaux and SL-resolution
• Short proofs for tricky formulas
• Optimality of size-width tradeoffs for resolution
• Short resolution proofs for a sequence of tricky formulas
• Linear resolution with selection function
• Separation results for the size of constant-depth propositional proofs
• An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning
• Optimality of size-degree tradeoffs for polynomial calculus
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• An Exponential Lower Bound for Width-Restricted Clause Learning
• GRASP: a search algorithm for propositional satisfiability
• A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution
• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
• Improved Separations of Regular Resolution from Clause Learning Proof Systems
• The complexity of resolution refinements
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution