On expansion and resolution in CEGAR based QBF solving

DOI10.1007/978-3-319-63390-9_25MaRDI QIDQ2164249zbMATH OpenOpenAlexFDO

Authors Leander Tentrup

Publication date 12 August 2022

Full work available at URL https://arxiv.org/abs/1803.09559

zbMATH Keywords

quantified Boolean formulasclauseresolution proofpolynomial simulationunique calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

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

Cited in

(15)

• Solving QBF with counterexample guided refinement
• Solving QBF with counterexample guided refinement
• scientific article; zbMATH DE number 7447736 (Why is no real title available?)
• 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
• Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
• CAQE and QuAbS: Abstraction Based QBF Solvers
• 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)