Source-linked AI summary
Solving QBF with Counterexample Guided Refinement
Mikoláš Janota, William Klieber, Joao Marques-Silva, Edmund Clarke
TL;DR
QBF solving is difficult because DPLL, dominant in SAT, is not sufficient for QBF. The paper introduces a CEGAR-driven recursive solver and CEGAR-based learning for DPLL, finding strong benchmark performance and useful additional learning despite memory costs.
Problem
DPLL-based SAT solving does not provide a sufficient general solution for QBF, motivating additional QBF solving techniques.
Method
The paper develops RAReQS, which recursively drives search with CEGAR, and adds CEGAR-based learning to an existing DPLL QBF solver.
Results
RAReQS solved approximately 33% more considered benchmark instances than QuBE7.2, while CEGAR learning was useful for DPLL-based solvers.
Takeaways & Limitations
CEGAR-based solvers and learning provide two promising approaches for QBF solving, including an alternative to existing solvers and stronger pruning in DPLL.
Takeaways & Limitations
RAReQS may require the same full expansion as traditional expansion-based solvers, with additional intermediate testing overhead.
Abstract
from arXiv · showhide
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.
1 Introduction
The paper applies CEGAR to QBF solving in two ways: a recursive solver and an additional learning technique for DPLL-based solving. Experiments show benefits across many QBF-LIB families.
- CEGAR is used to develop RAReQS, a recursive solver that gradually expands QBF formulas into propositional formulas.Unlike existing expansion-based solvers, RAReQS can terminate before full expansion, mitigating memory blowup.
- CEGAR is also introduced as an additional learning technique in an existing DPLL-based QBF solver.The technique enables more aggressive pruning but consumes more memory.
- Experimental evaluation demonstrates that CEGAR-based techniques are useful for a large number of QBF-LIB instance families.
2 Preliminaries
The preliminaries define QBF syntax, quantifier structure, assignments, substitutions, CNF notation, and the game-theoretic notion of winning moves.
- A QBF consists of a quantifier prefix followed by a propositional matrix, usually in prenex form.Quantifier blocks are maximal subsequences of universal or existential quantifiers.
- Variables are ordered by quantifier scope: upstream variables receive values before downstream variables.
- An assignment gives each variable exactly one truth value and can be substituted into Boolean formulas or QBFs.For QBFs, substitution removes the assigned variables’ quantifiers before replacing their occurrences.
- A QBF can be viewed as a game in which existential and universal players assign variables in prefix order.The existential player wins when the formula evaluates to 1; the universal player wins when it evaluates to 0.
- A winning move is an assignment to the current block that produces the appropriate truth outcome for its quantifier.For existential blocks the residual formula must be true, whereas for universal blocks it must be false.
3 Recursive CEGAR-based Algorithm
The recursive CEGAR algorithm searches for winning moves by maintaining and refining an abstraction of the QBF. It proceeds recursively through quantifier blocks and uses SAT at the one-quantifier base case.
- The recursion follows the prefix from upstream to downstream variables and seeks a winning move for each block.Recursive calls obtain winning moves for downstream variables.
- The one-quantifier base case is solved with a SAT solver.
- The algorithm builds an abstraction that proposes candidate winning moves and gradually strengthens it during refinement.Strengthening reduces the set of possible winning moves through conjunction and disjunction.
- The recursive procedure returns a winning move when one exists and otherwise returns NULL.
17 end
The full CEGAR procedure incrementally expands and verifies abstractions, while multi-games reduce duplicated work across recursive subproblems. The approach terminates with bounded iterations but can incur substantial memory growth.
- 3 Recursive CEGAR-based Algorithm: CEGAR represents a QBF abstraction as a partial expansion and adds counterexamples when the current expansion is too weak.A candidate winning the abstraction is verified against the original formula before being returned.
- 3 Recursive CEGAR-based Algorithm: Each loop iteration solves the abstraction, verifies its candidate, and either returns it or refines the abstraction with a counterexample.
- 3.1 Improving Recursive CEGAR-based Algorithm: The basic recursive algorithm can have high memory consumption because each iteration enlarges the abstraction and may double its variables.
- 3.1 Improving Recursive CEGAR-based Algorithm: Multi-games encode several subgames sharing a top-level move, allowing one candidate to be tested against multiple formulas simultaneously.A counterexample from a failing subgame is used to strengthen the multi-game abstraction.
- 3.2 Properties of the Algorithms: The CEGAR loops terminate because candidates do not repeat, with iteration bounds based on assignments to the relevant variables.For multi-games, the stated bound is min(2^|X|, n × 2^|Y|).
4 CEGAR as a learning technique in DPLL
The paper adds CEGAR learning to DPLL-based QBF solving by identifying counterexample assignments and refining the solver’s current formula. This supplements standard DPLL learning with a memory-conscious refinement procedure.
- CEGAR learning in DPLL: CEGAR learning extends an existing DPLL QBF solver with an additional learning technique.The procedure is inserted after standard DPLL learning and modifies the current input formula.
- CEGAR learning in DPLL: CEGAR learning is applied only when the last decision literal is owned by the winner of the current subproblem.The procedure is justified by observations based on the definitions of quantification and idempotence of conjunction and disjunction.
- CEGAR learning in DPLL: The procedure operates on a quantifier block associated with the last decision literal and constructs a complete assignment πc for that block.Unassigned variables in the block receive arbitrary values, while variables from other blocks are removed.
- CEGAR learning in DPLL: The assignment πc serves as the counterexample corresponding to the recursive CEGAR approach.The procedure uses this assignment to guide refinement of the formula.
- Implementation: The GhostQ prototype substitutes counterexamples into the original input formula rather than the current learned formula to reduce memory consumed per refinement.This may reduce effectiveness because refinements of refinements cannot be learned.
- Implementation: A quantifier block can be completely eliminated after extending its counterexample, and adjacent blocks with the same quantifier type can then be merged.Merging provides greater freedom in selecting variable order.
5 Experimental Results
The evaluation compares RAReQS and GhostQ-CEGAR with established QBF solvers on selected formal-verification and planning benchmarks. RAReQS solved the most instances overall, while GhostQ generally benefited from the added CEGAR learning despite some family-specific regressions.
- Evaluation setup: The experiments target formal-verification and planning families from QBF-LIB, using selected benchmark samples under fixed time and memory limits.Comparisons include QuBE7.2, Quantor, and Nenofex; most instances were preprocessed by bloqqer, except for GhostQ and the Debug family.
- Overall results: RAReQS solved the most considered instances, approximately 33% more than the second solver, QuBE7.2.It was also the best solver for most considered instance types.
- Overall results: Only 50 of the 801 instances on which the solver was aborted ran out of memory.This result accompanies RAReQS’s overall lead in solved instances.
- Family-level results: GhostQ-CEGAR worsened performance in several families, although the decline was slight except for Robots2D.It uniquely solved instances in irqlkeapclte, where no other solver solved any instance.
- Family-level results: CEGAR was especially effective on incrementer-encoder, conformant-planning, trafficlight-controller, Sorting-networks, and BMC families.RAReQS solved significantly more instances than existing solvers, and GhostQ-CEGAR improved significantly over GhostQ on these families.
6 Related Work
The paper situates RAReQS among CEGAR applications and expansion-based QBF solvers. Its expansion strategy differs by starting from outermost variables and expanding only selected assignments rather than both values of every scheduled variable.
- CEGAR applications: CEGAR has been applied to model checking, SMT solving, quantified SMT, and special-case QBF problems with limited quantification.Earlier QBF applications include vertex eccentricity, nonmonotonic reasoning, and two-level quantification.
- CEGAR and QBF solving: Prior QBF work used SAT to guide DPLL search or abstraction during preprocessing, but the abstraction notion in preprocessing differs from RAReQS’s.The preprocessing abstraction treats universally quantified variables as existentially quantified.
- Expansion-based solving: RAReQS expands QBF into a propositional formula solved by a SAT solver, like several existing expansion-based solvers.Related solvers include QUBOS, Quantor, and Nenofex, which also use techniques to mitigate expansion blowup.
- Expansion strategy: Unlike related solvers that begin with innermost variables, RAReQS starts expansion from the outermost variables.The paper identifies this as a significant difference in how expansion is carried out.
- Expansion strategy: RAReQS expands only a selected assignment to a variable block and checks whether that expansion is sufficient.Abstraction can therefore stop expansion early, producing easier SAT formulas and mitigating memory blowup.
7 Conclusions and Future Work
The paper develops two CEGAR-based QBF techniques: the RAReQS solver and an additional learning mechanism for DPLL solvers. Experiments show benefits for both approaches, while their limitations motivate further refinement.
- The paper develops two novel techniques: the CEGAR-driven RAReQS solver and an additional learning technique for DPLL solvers.
- RAReQS expands formulas step-by-step using counterexamples, avoiding full expansion when a sufficient partial expansion can be found.
- RAReQS avoids expansion solvers’ inherent memory blowup and outperforms a traditional DPLL-based approach on many practical instances.
- CEGAR-based learning is more powerful than standard clause/cube learning, but it requires more memory.
- Future work targets full CEGAR learning in DPLL, tuning its cost, and integrating further capabilities into RAReQS.