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

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

Cites work

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

Describes a project that uses

Uses Software

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

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)