Quantifier shifting for quantified Boolean formulas revisited

DOI10.1007/978-3-031-63498-7_20MaRDI QIDQ7034856zbMATH OpenFDO

Authors Simone Heisinger, Maximilian Heisinger, Adrián Rebola-Pardo, Martina Seidl

Publication date 31 January 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-63498-7_20

zbMATH Keywords

normal form transformationprenexingquantified Boolean formulas

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A non-prenex, non-clausal QBF solver with game-state learning
• A structure-preserving clause form translation
• Backdoor sets of quantified Boolean formulas
• Blocked clause elimination for QBF
• Booleguru, the propositional polyglot (short paper)
• Circuit-based search space pruning in QBF
• Computing small clause normal forms
• Dependency learning for QBF
• Dependency Learning for QBF
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Exploiting circuit representations in QBF solving
• Integrating dependency schemes in search-based QBF solvers
• Lower bounds for multiplayer noncooperative games of incomplete information
• Moving definition variables in quantified Boolean formulas
• Non-prenex QBF solving using abstraction
• Reasons for hardness in QBF proof systems
• Solving QBF by abstraction
• Solving QBF with counterexample guided refinement
• Theory and Applications of Satisfiability Testing
• Twelve years of QBF evaluations: QSAT is PSPACE-hard and it shows

Cited in

(1)

• Booleguru, the propositional polyglot (short paper)

This page was built for publication: Quantifier shifting for quantified Boolean formulas revisited

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7034856)