On expansion and resolution in CEGAR based QBF solving
From MaRDI portal
Publication:2164249
DOI10.1007/978-3-319-63390-9_25zbMATH Open1494.68293arXiv1803.09559OpenAlexW2734351583MaRDI QIDQ2164249FDOQ2164249
Authors: Leander Tentrup 
Publication date: 12 August 2022
Abstract: A quantified Boolean formula (QBF) is a propositional formula extended with universal and existential quantification over propositions. There are two methodologies in CEGAR based QBF solving techniques, one that is based on a refinement loop that builds partial expansions and a more recent one that is based on the communication of satisfied clauses. Despite their algorithmic similarity, their performance characteristics in experimental evaluations are very different and in many cases orthogonal. We compare those CEGAR approaches using proof theory developed around QBF solving and present a unified calculus that combines the strength of both approaches. Lastly, we implement the new calculus and confirm experimentally that the theoretical improvements lead to improved performance.
Full work available at URL: https://arxiv.org/abs/1803.09559
Recommendations
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- On propositional QBF expansions and Q-resolution
- Solving QBF with counterexample guided refinement
- Expansion-based QBF solving versus Q-resolution
- Theory and Applications of Satisfiability Testing
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cited In (15)
- Solving QBF with counterexample guided refinement
- Solving QBF with counterexample guided refinement
- Title not available (Why is that?)
- Expansion-based QBF solving on tree decompositions
- Nenofex: Expanding NNF for QBF Solving
- On propositional QBF expansions and Q-resolution
- Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
- Expansion-based QBF solving versus Q-resolution
- QELL: QBF reasoning with extended clause learning and levelized SAT solving
- Theory and Applications of Satisfiability Testing
- CAQE and QuAbS: Abstraction Based QBF Solvers
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- Enhancing search-based QBF solving by dynamic blocked clause elimination
- Never trust your solver: certification for SAT and QBF
- True crafted formula families for benchmarking quantified satisfiability solvers
This page was built for publication: On expansion and resolution in CEGAR based QBF solving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2164249)
