Expansion-based QBF solving versus Q-resolution
From MaRDI portal
Publication:2339467
DOI10.1016/j.tcs.2015.01.048zbMath1309.68168DBLPjournals/tcs/JanotaM15OpenAlexW2051846104WikidataQ62047279 ScholiaQ62047279MaRDI QIDQ2339467
Mikoláš Janota, João P. Marques-Silva
Publication date: 1 April 2015
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2015.01.048
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (36)
Solution validation and extraction for QBF preprocessing ⋮ Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ The QBF Gallery: behind the scenes ⋮ Feasible Interpolation for QBF Resolution Calculi ⋮ Unnamed Item ⋮ Relating size and width in variants of Q-resolution ⋮ Conformant planning as a case study of incremental QBF solving ⋮ A simple proof of QBF hardness ⋮ Lower Bound Techniques for QBF Proof Systems ⋮ Unnamed Item ⋮ Never trust your solver: certification for SAT and QBF ⋮ A game characterisation of tree-like Q-resolution size ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Towards Uniform Certification in QBF ⋮ Level-ordered \(Q\)-resolution and tree-like \(Q\)-resolution are incomparable ⋮ Unnamed Item ⋮ Lower bound techniques for QBF expansion ⋮ Lower bounds for QCDCL via formula gauge ⋮ Characterising tree-like Frege proofs for QBF ⋮ Understanding cutting planes for QBFs ⋮ Building strategies into QBF proofs ⋮ On Q-Resolution and CDCL QBF Solving ⋮ Q-Resolution with Generalized Axioms ⋮ Lifting QBF Resolution Calculi to DQBF ⋮ Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations ⋮ Unnamed Item ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF ⋮ Unnamed Item ⋮ Unnamed Item ⋮ How QBF expansion makes strategy extraction hard ⋮ On Exponential Lower Bounds for Partially Ordered Resolution ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ Solving QBF with counterexample guided refinement ⋮ QBFFam: a tool for generating QBF families from proof complexity ⋮ Lower bounds for QCDCL via formula gauge ⋮ Hardness and optimality in QBF proof systems modulo NP
Uses Software
Cites Work
- Theory and applications of satisfiability testing -- SAT 2012. 15th international conference, Trento, Italy, June 17--20, 2012. Proceedings
- Satisfiability, branch-width and Tseitin tautologies
- Davis-Putnam resolution versus unrestricted resolution
- An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
- Resolution for quantified Boolean formulas
- Unified QBF certification and its applications
- On Sequent Systems and Resolution for QBFs
- Solving QBF with Counterexample Guided Refinement
- Abstraction-Based Algorithm for 2QBF
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Quantified propositional calculi and fragments of bounded arithmetic
- Nenofex: Expanding NNF for QBF Solving
- Bounded Universal Expansion for Preprocessing QBF
- The relative efficiency of propositional proof systems
- Contributions to the Theory of Practical Quantified Boolean Formula Solving
- On Propositional QBF Expansions and Q-Resolution
- Logic for Programming, Artificial Intelligence, and Reasoning
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Expansion-based QBF solving versus Q-resolution
