Proof complexity of symbolic QBF reasoning

DOI10.1007/978-3-030-80223-3_28OpenAlexW3184676641MaRDI QIDQ2118330

Stefan Mengel, Friedrich Slivovsky

Publication date: 22 March 2022

Full work available at URL: https://arxiv.org/abs/2104.02563

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational aspects of satisfiability (68R07)

Uses Software

• CUDD
• Quaffle
• DepQBF
• CAQE
• RAReQS
• QESTO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Solving QBF with counterexample guided refinement
• A self-adaptive multi-engine solver for quantified Boolean formulas
• Resolution for quantified Boolean formulas
• Lower bound techniques for QBF expansion
• Unified QBF certification and its applications
• Non-prenex QBF Solving Using Abstraction
• Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
• QBF Resolution Systems and Their Proof Complexities
• Expander graphs and their applications
• Graph-Based Algorithms for Boolean Function Manipulation
• The relative efficiency of propositional proof systems
• Branching Programs and Binary Decision Diagrams
• Communication Complexity
• Contributions to the Theory of Practical Quantified Boolean Formula Solving
• Dependency Learning for QBF
• Frege Systems for Quantified Boolean Logic
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
• New Resolution-Based QBF Calculi and Their Proof Complexity
• Treewidth in Verification: Local vs. Global
• Theory and Applications of Satisfiability Testing
• Principles and Practice of Constraint Programming – CP 2004
• Principles and Practice of Constraint Programming – CP 2004