Proof complexity of symbolic QBF reasoning

DOI10.1007/978-3-030-80223-3_28MaRDI QIDQ2118330zbMATH OpenOpenAlexFDO

Authors Stefan Mengel, Friedrich Slivovsky

Publication date 22 March 2022

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

Mathematics Subject Classification ID

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

Cites work

• scientific article; zbMATH DE number 7029312 (Why is no real title available?)
• scientific article; zbMATH DE number 7250156 (Why is no real title available?)
• A self-adaptive multi-engine solver for quantified Boolean formulas
• Branching Programs and Binary Decision Diagrams
• Communication Complexity
• Contributions to the theory of practical quantified Boolean formula solving
• Dependency Learning for QBF
• Expander graphs and their applications
• Frege systems for quantified Boolean logic
• Graph-Based Algorithms for Boolean Function Manipulation
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
• Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
• Lower bound techniques for QBF expansion
• Lower bounds for linear decision lists
• New resolution-based QBF calculi and their proof complexity
• Non-prenex QBF solving using abstraction
• Principles and Practice of Constraint Programming – CP 2004
• Principles and Practice of Constraint Programming – CP 2004
• QBF Resolution Systems and Their Proof Complexities
• Resolution for quantified Boolean formulas
• Solving QBF with counterexample guided refinement
• The PACE 2017 parameterized algorithms and computational experiments challenge: the second iteration
• The relative efficiency of propositional proof systems
• Theory and Applications of Satisfiability Testing
• Treewidth in Verification: Local vs. Global
• Unified QBF certification and its applications

Cited in

(8)

• QBF Resolution Systems and Their Proof Complexities
• On QBF Proofs and Preprocessing
• QBF as an alternative to Courcelle's theorem
• Short proofs in QBF expansion
• Theory and Applications of Satisfiability Testing
• Shortening QBF proofs with dependency schemes
• On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
• scientific article; zbMATH DE number 7278086 (Why is no real title available?)

Describes a project that uses

Uses Software

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

This page was built for publication: Proof complexity of symbolic QBF reasoning

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