Solving QBF by abstraction

MaRDI QIDQ3384880zbMATH OpenFDO

Authors Jesko Hecking-Harbusch, Leander Tentrup

Publication date 17 December 2021

Full work available at URL https://arxiv.org/abs/1604.06752, http://eptcs.web.cse.unsw.edu.au/paper.cgi?GandALF18.7

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Applications of game theory (91A80)

Recommendations

• CAQE and QuAbS: Abstraction Based QBF Solvers
• Solving QBF with counterexample guided refinement
• Unified QBF certification and its applications
• Clausal abstraction for DQBF
• Abstraction-based algorithm for 2QBF

Cites work

• A non-prenex, non-clausal QBF solver with game-state learning
• A solver for QBFs in negation normal form
• A structure-preserving clause form translation
• Beyond CNF: A Circuit-Based QBF Solver
• Bounded synthesis for Petri games
• Circuit-based search space pruning in QBF
• Dependency learning for QBF
• Detecting unrealizability of distributed fault-tolerant systems
• Encodings of bounded synthesis
• Expansion-based QBF solving versus Q-resolution
• Exploiting circuit representations in QBF solving
• Lower bounds: from circuits to QBF proof systems
• Nenofex: Expanding NNF for QBF Solving
• Non-prenex QBF solving using abstraction
• On expansion and resolution in CEGAR based QBF solving
• Petri games: synthesis of distributed systems with causal memory
• QELL: QBF reasoning with extended clause learning and levelized SAT solving
• SAT-Based Synthesis Methods for Safety Specs
• Solving QBF with counterexample guided refinement
• Unified QBF certification and its applications

Cited in

(8)

• Bounded model checking for hyperproperties
• Antichain-Based QBF Solving
• Efficient trace encodings of bounded synthesis for asynchronous distributed systems
• CAQE and QuAbS: Abstraction Based QBF Solvers
• BOCoSy: Small but Powerful Symbolic Output-Feedback Control
• Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification
• Quantifier shifting for quantified Boolean formulas revisited
• Booleguru, the propositional polyglot (short paper)

This page was built for publication: Solving QBF by abstraction

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