On exponential lower bounds for partially ordered resolution

DOI10.3233/SAT190110MaRDI QIDQ5015597zbMATH OpenFDO

Authors Mikoláš Janota

Publication date 9 December 2021

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

Full work available at URL https://doi.org/10.3233/SAT190110

zbMATH Keywords

lower boundspartial orderresolutionresolution order

Mathematics Subject Classification ID

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

Recommendations

• An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
• On the relative complexity of resolution refinements and cutting planes proof systems
• An Exponential Lower Bound for Width-Restricted Clause Learning
• Short proofs are narrow -- resolution made simple
• Short proofs are narrow—resolution made simple

Cites work

• Davis-Putnam resolution versus unrestricted resolution
• Expansion-based QBF solving versus Q-resolution
• GRASP: a search algorithm for propositional satisfiability
• scientific article; zbMATH DE number 5899257 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• Limitations of restricted branching in clause learning
• Linear resolution with selection function
• On the complexity of regular resolution and the Davis-Putnam procedure
• On the power of clause-learning SAT solvers as resolution engines
• On the relative complexity of resolution refinements and cutting planes proof systems
• Proof complexity of resolution-based QBF calculi
• Solving propositional satisfiability problems
• The Complexity of Propositional Proofs
• The intractability of resolution
• The relative efficiency of propositional proof systems
• Unrestricted resolution versus N-resolution
• Unrestricted vs restricted cut in a tableau method for Boolean circuits

Cited in

(4)

• Resolution with counting: dag-like lower bounds and different moduli
• scientific article; zbMATH DE number 1929954 (Why is no real title available?)
• scientific article; zbMATH DE number 7650367 (Why is no real title available?)
• Strategy extraction by interpolation

This page was built for publication: On exponential lower bounds for partially ordered resolution

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