New Resolution-Based QBF Calculi and Their Proof Complexity

DOI10.1145/3352155zbMath1496.68362OpenAlexW2972754151WikidataQ127239097 ScholiaQ127239097MaRDI QIDQ5205822

Olaf Beyersdorff, Mikoláš Janota, Leroy Chew

Publication date: 16 December 2019

Published in: ACM Transactions on Computation Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3352155

zbMATH Keywords

separationsproof complexityQBFlower-bound techniques

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (14)

Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ Proof complexity of modal resolution ⋮ A simple proof of QBF hardness ⋮ Never trust your solver: certification for SAT and QBF ⋮ True crafted formula families for benchmarking quantified satisfiability solvers ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Towards Uniform Certification in QBF ⋮ Subsumption-linear Q-resolution for QBF theorem proving ⋮ Lower bounds for QCDCL via formula gauge ⋮ Building strategies into QBF proofs ⋮ QBFFam: a tool for generating QBF families from proof complexity ⋮ Lower bounds for QCDCL via formula gauge ⋮ Hardness and optimality in QBF proof systems modulo NP ⋮ Proof complexity of symbolic QBF reasoning

This page was built for publication: New Resolution-Based QBF Calculi and Their Proof Complexity