scientific article; zbMATH DE number 7029312
From MaRDI portal
Publication:4625702
Recommendations
- Size, cost and capacity: a semantic technique for hard random QBFs
- Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- An empirical study of QBF encodings: from treewidth estimation to useful preprocessing
- Query complexity in errorless hardness amplification
- Query complexity in errorless hardness amplification
- scientific article; zbMATH DE number 3873306
- Universal quantifiers and time complexity of random access machines
- Term Rewriting and Applications
- Hardness-randomness tradeoffs for bounded depth arithmetic circuits
Cites work
- A characterization of tree-like resolution size
- A game characterisation of tree-like Q-resolution size
- A new upper bound for 3-SAT
- A threshold for unsatisfiability
- Are Short Proofs Narrow? QBF Resolution Is Not So Simple
- Automated testing and debugging of SAT and QBF solvers
- Conformant planning as a case study of incremental QBF solving
- Contributions to the theory of practical quantified Boolean formula solving
- Evaluating and certifying QBFs: a comparison of state-of-the-art tools
- Exact location of the phase transition for random (1,2)-QSAT
- Expansion-based QBF solving versus Q-resolution
- Fault Localization and Correction with QBF
- Feasible interpolation for QBF resolution calculi
- scientific article; zbMATH DE number 5542982 (Why is no real title available?)
- scientific article; zbMATH DE number 3560737 (Why is no real title available?)
- scientific article; zbMATH DE number 1256700 (Why is no real title available?)
- scientific article; zbMATH DE number 1256733 (Why is no real title available?)
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- scientific article; zbMATH DE number 1850736 (Why is no real title available?)
- scientific article; zbMATH DE number 819737 (Why is no real title available?)
- scientific article; zbMATH DE number 1445296 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Logical foundations of proof complexity
- Long distance Q-resolution with dependency schemes
- Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
- Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
- Lower bounds: from circuits to QBF proof systems
- On Stronger Calculi for QBFs
- On the complexity of cutting-plane proofs
- On Unification of QBF Resolution-Based Calculi
- Planning as quantified Boolean formula
- Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
- Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness
- Proof complexity of resolution-based QBF calculi
- Q-resolution with generalized axioms
- QBF Resolution Systems and Their Proof Complexities
- Random 2-SAT: Results and problems
- Random CNF's are hard for the polynomial calculus
- Resolution for quantified Boolean formulas
- SAT-Based Synthesis Methods for Safety Specs
- Short proofs are narrow—resolution made simple
- Space Complexity in Propositional Calculus
- The Complexity of Propositional Proofs
- The intractability of resolution
- The relative efficiency of propositional proof systems
- Theory and Applications of Satisfiability Testing
- Towards an understanding of polynomial calculus: new separations and lower bounds (extended abstract)
- Towards NP-P via proof complexity and search
- Understanding cutting planes for QBFs
- Understanding Gentzen and Frege Systems for QBF
- Unified QBF certification and its applications
Cited in
(27)- Lower bound techniques for QBF expansion
- Building strategies into QBF proofs
- QBFFam: a tool for generating QBF families from proof complexity
- Lower bounds for QCDCL via formula gauge
- Proof complexity of symbolic QBF reasoning
- Characterising tree-like Frege proofs for QBF
- A simple proof of QBF hardness
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- Size, cost and capacity: a semantic technique for hard random QBFs
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- Term Rewriting and Applications
- Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
- Lower bounds for QCDCL via formula gauge
- Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
- Classes of hard formulas for QBF resolution
- Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
- Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
- QBF merge resolution is powerful but unnatural
- Runtime vs. extracted proof size: an exponential gap for CDCL on QBFs
- Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
- Strong (D)QBF dependency schemes via implication-free resolution paths
- Hard QBFs for merge resolution
- QCDCL with cube learning or pure literal elimination -- what is best?
- Understanding the relative strength of QBF CDCL solvers and QBF resolution
- Polynomial calculus for quantified Boolean logic: lower bounds through circuits and degree
- Extending merge resolution to a family of QBF-proof systems
- Proof complexity of modal resolution
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4625702)
