Primal and dual encoding from applications into quantified boolean formulas

Abstract

Quantified Boolean Formulas (QBF) provide a good language for modeling many complex questions about deterministic systems, especially questions involving control of such systems and optimizing choices. However, translators typically have one set way to encode the description of a system and a property, or question about the system, often without distinguishing between the two. In many cases there are choices about encoding methods, and one method will be much easier for a particular solver. This paper shows how to encode a large class of problems into primal and dual versions with opposite answers, while avoiding the blow-up associated with a simple negation of the first encoding. The main point is that these encodings require knowledge of the underlying application; they are not automatic translations on a QBF. Trying to divide an arbitrary QBF into a system part and a property part is actually co-NP-hard. For proof of concept, primal and dual encodings were implemented for several problem families in QBFLIB. (The primal encodings were already in QBFLIB.) For leading publicly available QBF solvers, solving times often differed by factors over 100, between the primal and dual encoding of the same underlying problem. Therefore, running both encodings in parallel and stopping when one encoding is solved is an attractive strategy, even though CPU time on both processors is charged. For some families and some solvers, this strategy was significantly faster than running only the primal on all problems, or running only the dual on all problems. Implications for certificates are also discussed briefly. © 2013 Springer-Verlag.