Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
From MaRDI portal
Publication:896919
DOI10.1016/j.tcs.2015.10.020zbMath1332.68204OpenAlexW2191125414MaRDI QIDQ896919
Stefan Szeider, Friedrich Slivovsky
Publication date: 15 December 2015
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2015.10.020
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (11)
Solution validation and extraction for QBF preprocessing ⋮ Small Resolution Proofs for QBF using Dependency Treewidth ⋮ Long-distance Q-resolution with dependency schemes ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Dependency Schemes for DQBF ⋮ Long Distance Q-Resolution with Dependency Schemes ⋮ Unnamed Item ⋮ The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17) ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ Certified DQBF solving by definition extraction
Cites Work
- Backdoor sets of quantified Boolean formulas
- An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
- Resolution for quantified Boolean formulas
- Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
- Unified QBF certification and its applications
- Computing Resolution-Path Dependencies in Linear Time ,
- On Unification of QBF Resolution-Based Calculi
- Variable Independence and Resolution Paths for Quantified Boolean Formulas
- A Unified Proof System for QBF Preprocessing
- Integrating Dependency Schemes in Search-Based QBF Solvers
- On Propositional QBF Expansions and Q-Resolution
- Variable Dependencies of Quantified CSPs
- A machine program for theorem-proving
- Lower bounds for multiplayer noncooperative games of incomplete information
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
