On Exponential Lower Bounds for Partially Ordered Resolution

DOI10.3233/SAT190110zbMath1484.03121MaRDI QIDQ5015597

Mikoláš Janota

Publication date: 9 December 2021

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

zbMATH Keywords

lower boundspartial orderresolutionresolution order

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• On the power of clause-learning SAT solvers as resolution engines
• Unrestricted vs restricted cut in a tableau method for Boolean circuits
• The intractability of resolution
• Unrestricted resolution versus N-resolution
• On the complexity of regular resolution and the Davis-Putnam procedure
• Davis-Putnam resolution versus unrestricted resolution
• Solving propositional satisfiability problems
• Limitations of restricted branching in clause learning
• Expansion-based QBF solving versus Q-resolution
• Linear resolution with selection function
• On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems
• The relative efficiency of propositional proof systems
• GRASP: a search algorithm for propositional satisfiability
• The Complexity of Propositional Proofs
• Unnamed Item
• Unnamed Item
• Unnamed Item