Proof complexity of symbolic QBF reasoning
From MaRDI portal
Publication:2118330
DOI10.1007/978-3-030-80223-3_28OpenAlexW3184676641MaRDI QIDQ2118330FDOQ2118330
Authors: Stefan Mengel, Friedrich Slivovsky 
Publication date: 22 March 2022
Full work available at URL: https://arxiv.org/abs/2104.02563
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
- Theory and Applications of Satisfiability Testing
- Graph-Based Algorithms for Boolean Function Manipulation
- Resolution for quantified Boolean formulas
- Unified QBF certification and its applications
- Solving QBF with counterexample guided refinement
- Contributions to the theory of practical quantified Boolean formula solving
- Principles and Practice of Constraint Programming – CP 2004
- Expander graphs and their applications
- Branching Programs and Binary Decision Diagrams
- Dependency Learning for QBF
- A self-adaptive multi-engine solver for quantified Boolean formulas
- Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
- QBF Resolution Systems and Their Proof Complexities
- Communication Complexity
- The relative efficiency of propositional proof systems
- Treewidth in Verification: Local vs. Global
- Principles and Practice of Constraint Programming – CP 2004
- Frege systems for quantified Boolean logic
- Non-prenex QBF solving using abstraction
- Title not available (Why is that?)
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- New resolution-based QBF calculi and their proof complexity
- Lower bounds for linear decision lists
- Lower bound techniques for QBF expansion
- Title not available (Why is that?)
- The PACE 2017 parameterized algorithms and computational experiments challenge: the second iteration
Cited In (8)
- On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
- QBF as an alternative to Courcelle's theorem
- Shortening QBF proofs with dependency schemes
- Theory and Applications of Satisfiability Testing
- On QBF Proofs and Preprocessing
- QBF Resolution Systems and Their Proof Complexities
- Short proofs in QBF expansion
- Title not available (Why is that?)
Uses Software
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)
