On expansion and resolution in CEGAR based QBF solving

DOI10.1007/978-3-319-63390-9_25zbMath1494.68293arXiv1803.09559OpenAlexW2734351583MaRDI QIDQ2164249

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)

Related Items (6)

Never trust your solver: certification for SAT and QBF ⋮ True crafted formula families for benchmarking quantified satisfiability solvers ⋮ Unnamed Item ⋮ Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers

This page was built for publication: On expansion and resolution in CEGAR based QBF solving