Single-Solver Algorithms for 2QBF (Poster Presentation)
Why this work is in the frame
A frame that forgets how it found something cannot be audited. These are the routes that admitted this work.
Bibliographic record
Abstract
2QBF is a restriction of QBF, in which at most one quantifier alternation is allowed. This simplifying assumption makes the problem easier to reason about, and allows for simpler unit propagation and clause/cube learning procedures. We introduce two new 2QBF algorithms that take advantage of 2QBF specifically. The first improves upon earlier work by Ranjan, Tang, and Malik (2004), while the second introduces a new ‘free’ decision heuristic that doesn’t need to respect quantifier order. Implementations of both new algorithms perform better than two state-of-the-art general QBF solvers on formal verification and AI planning instances. Ranjan, Tang, and Malik [4] introduced an algorithm for 2QBF in which two standard SAT solvers cooperate to solve the formula; in brief, ‘Solver B’ solves the (complements of) the learnt cubes, while ‘Solver A’ solves the input formula φ under Solver B’s current assignment to the universally quantified variables. The solvers iterate back and forth until either fails to find a satisfying solution. We improved upon this algorithm so that it can be implemented in just a single augmented SAT solver, rather than two. This solver stores two different types of learnt clauses: a set φ∃ of existential clauses (corresponding to the clauses in Solver A) and a set φ∀ containing the complements of learnt cubes (corresponding to those in Solver B). As in a standard DPLL-based QBF solver, this algorithm requires all universals to be assigned before any existentials can be chosen as decision variables. This algorithm resembles a special case of standard cube-learning QBF solvers, however, we introduce some new termination conditions that are specific to 2QBF. These termination conditions are sufficient to ensure that the solver never has to handle the case where the implication graph of a conflict contains both universally and existentially quantified literals at the same decision level. This dramatically simplifies clause/cube learning: any valid cut in the implication graph at the current decision level is a learnt existential clause iff the decision variable was existential, and is (the complement of) a learnt cube iff the decision variable was universal. In contrast, Quaffle-based QBF solvers require several additional conditions to be met to ensure that conflict resolution does not resolve learnt cubes with clauses [1], which complicate both clause learning and unit propagation; these conditions are implicitly met in 2QBF (so long as the two shortcuts above are handled), and are met by the standard 1-UIP clause learning algorithm [2] without modification. We implement this simple 2QBF algorithm in Mini2QBF, based on MiniSat (version 1.14), and find that it is faster than state-of-the-art QBF solvers DepQBF [5] and QuBE [6] on real-world formal
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
Full frame distilled prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. Learned from the 10,348 direct Codex labels and 10,348 direct Gemma labels. Candidate is the union of thresholded teacher heads; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels or direct frontier model labels.
Codex and Gemma teacher scores by category
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.003 | 0.001 |
| Meta-epidemiology (narrow) | 0.000 | 0.000 |
| Meta-epidemiology (broad) | 0.000 | 0.000 |
| Bibliometrics | 0.000 | 0.000 |
| Science and technology studies | 0.000 | 0.000 |
| Scholarly communication | 0.000 | 0.001 |
| Open science | 0.000 | 0.000 |
| Research integrity | 0.000 | 0.000 |
| Insufficient payload (model declined to judge) | 0.000 | 0.000 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from it