Lower Bound Techniques for QBF Proof Systems

DOI10.4230/LIPIcs.STACS.2018.2zbMath1487.03067OpenAlexW2789336854MaRDI QIDQ3304096

Meena Mahajan

Publication date: 5 August 2020

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2018/8536/pdf/LIPIcs-STACS-2018-2.pdf/

zbMATH Keywords

resolutionproof complexityquantified Boolean formulaslower 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)

Uses Software

• QuBE++
• Quaffle
• QUBE
• CAQE
• RAReQS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Resolution for quantified Boolean formulas
• Expansion-based QBF solving versus Q-resolution
• Unified QBF certification and its applications
• A combinatorial characterization of resolution width
• Lower Bounds
• Solving QBF with Counterexample Guided Refinement
• On Unification of QBF Resolution-Based Calculi
• QBF Resolution Systems and Their Proof Complexities
• Counterexample-guided abstraction refinement for symbolic model checking
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Short proofs are narrow—resolution made simple
• Understanding Gentzen and Frege Systems for QBF
• Contributions to the Theory of Practical Quantified Boolean Formula Solving
• A Non-prenex, Non-clausal QBF Solver with Game-State Learning
• Formal Methods in Computer-Aided Design