Understanding cutting planes for QBFs
From MaRDI portal
Publication:1784953
DOI10.1016/J.IC.2018.08.002zbMATH Open1477.03245OpenAlexW2887013560WikidataQ63378008 ScholiaQ63378008MaRDI QIDQ1784953FDOQ1784953
Authors: Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil K. Shukla 
Publication date: 27 September 2018
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: http://eprints.whiterose.ac.uk/147855/8/manuscript.pdf
Recommendations
Cites Work
- Resolution for quantified Boolean formulas
- Expansion-based QBF solving versus Q-resolution
- Unified QBF certification and its applications
- On Unification of QBF Resolution-Based Calculi
- Proof complexity of resolution-based QBF calculi
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Contributions to the theory of practical quantified Boolean formula solving
- Computational Complexity
- Title not available (Why is that?)
- Analysis of Boolean Functions
- Title not available (Why is that?)
- Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
- QBF Resolution Systems and Their Proof Complexities
- Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
- Logical foundations of proof complexity
- A Machine-Oriented Logic Based on the Resolution Principle
- Some consequences of cryptographical conjectures for \(S_2^1\) and EF
- The relative efficiency of propositional proof systems
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- On the complexity of cutting-plane proofs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Bounded-width QBF is PSPACE-complete
- Open-WBO: a modular MaxSAT solver
- On Cutting Planes
- The intractability of resolution
- Edmonds polytopes and weakly hamiltonian graphs
- Uniform constant-depth threshold circuits for division and iterated multiplication.
- Non-automatizability of bounded-depth Frege proofs
- Polynomial size proofs of the propositional pigeonhole principle
- Towards NP-P via proof complexity and search
- Title not available (Why is that?)
- The Complexity of Propositional Proofs
- Dual weak pigeonhole principle, Boolean complexity, and derandomization
- Conformant planning as a case study of incremental QBF solving
- On the correspondence between arithmetic theories and propositional proof systems – a survey
- Title not available (Why is that?)
- Feasible interpolation for QBF resolution calculi
- Learning curves of the clipped Hebb rule for networks with binary weights
- Using combinatorial benchmarks to probe the reasoning power of pseudo-Boolean solvers
- Lower bounds: from circuits to QBF proof systems
- Semantic versus syntactic cutting planes
- A game characterisation of tree-like Q-resolution size
- On sequent systems and resolution for QBFs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
- Understanding Gentzen and Frege Systems for QBF
- Understanding cutting planes for QBFs
Cited In (7)
- Towards Uniform Certification in QBF
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- How QBF expansion makes strategy extraction hard
- Understanding cutting planes for QBFs
- QBF merge resolution is powerful but unnatural
- Achieving consistency with cutting planes
- Title not available (Why is that?)
Uses Software
This page was built for publication: Understanding cutting planes for QBFs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1784953)
