Single-Solver Algorithms for 2QBF (Poster Presentation)

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

Récupéré en direct depuis OpenAlex et désinversé. Les résumés ne sont pas conservés dans cette base de données : les index inversés représentent 8,6 Go des 9,3 Go de texte de la base, et le serveur dispose de 13 Go libres.