Single-solver algorithms for 2QBF (Poster presentation)

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. © 2012 Springer-Verlag.