Soundness of Q-resolution with dependency schemes
From MaRDI portal
Publication:896919
DOI10.1016/J.TCS.2015.10.020zbMATH Open1332.68204OpenAlexW2191125414MaRDI QIDQ896919FDOQ896919
Authors: Friedrich Slivovsky, Stefan Szeider 
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
Recommendations
Cites Work
- Resolution for quantified Boolean formulas
- Unified QBF certification and its applications
- On Unification of QBF Resolution-Based Calculi
- Title not available (Why is that?)
- On propositional QBF expansions and Q-resolution
- Title not available (Why is that?)
- A unified proof system for QBF preprocessing
- Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
- A machine program for theorem-proving
- Lower bounds for multiplayer noncooperative games of incomplete information
- Backdoor sets of quantified Boolean formulas
- Computing Resolution-Path Dependencies in Linear Time ,
- Variable independence and resolution paths for quantified Boolean formulas
- Integrating dependency schemes in search-based QBF solvers
- Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
- An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
- Variable Dependencies of Quantified CSPs
Cited In (17)
- Dependency schemes for DQBF
- The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
- Certified DQBF solving by definition extraction
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- Understanding the Relative Strength of QBF CDCL Solvers and 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
- Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
- Variable dependencies and Q-resolution
- A resolution-style proof system for DQBF
- Solution validation and extraction for QBF preprocessing
- Should Decisions in QCDCL Follow Prefix Order?
- Small resolution proofs for QBF using dependency treewidth
- Long-distance Q-resolution with dependency schemes
- Title not available (Why is that?)
- Strong (D)QBF dependency schemes via tautology-free resolution paths
- Long distance Q-resolution with dependency schemes
This page was built for publication: Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q896919)
