Solving QBF with Counterexample Guided Refinement

Abstract

We propose two novel approaches for using Counterexample-Guided Abstraction Refinement (CEGAR) in Quantified Boolean Formula (QBF) solvers. The first approach develops a recursive algorithm whose search is driven by CEGAR (rather than by DPLL). The second approach employs CEGAR as an additional learning technique in an existing DPLL-based QBF solver. Experimental evaluation of the implemented prototypes shows that the CEGAR-driven solver outperforms existing solvers on a number of families in the QBF-LIB and that the DPLL solver benefits from the additional type of learning. Thus this article opens two promising avenues in QBF: CEGAR-driven solvers as an alternative to existing approaches and a novel type of learning in DPLL.

References in corpus (1)

• Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription

Cited by in corpus (14)

• Solving QBF by Clause Selection
• The QBF Gallery: Behind the Scenes
• Synchronous Counting and Computational Algorithm Design
• Propositional Abduction with Implicit Hitting Sets
• Synthesis of a simple self-stabilizing system
• Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning
• QBF Solving by Counterexample-guided Expansion
• Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications
• On QBF Proofs and Preprocessing
• Towards Uniform Certification in QBF
• Local Redundancy in SAT: Generalizations of Blocked Clauses
• Solving QSAT problems with neural MCTS
• Model Checking for Rectangular Hybrid Systems: A Quantified Encoding Approach
• Extending Prolog for Quantified Boolean Horn Formulas