Lemma and model caching in decision procedures for quantified boolean formulas

Abstract. The increasingrole of quantified Boolean logic in many applications calls for practically efficient decision procedures. One of the most promisingparadigms is the semantic tree format implemented in the style of the DPLL procedure. In this paper, so-called learningtechniques like intelligent backtrackingand cachingof lemmas which proved useful in the pure propositional case are generalised to the quantified Boolean case and the occuringdifferences are discussed. Due to the strongrestriction of the variable selection in semantic tree procedures for quantified Boolean formulas, learningmethods are more important than in the propositional case, as we demonstrate. Furthermore, in addition to the cachingof lemmas, significant advances can be achieved by techniques based on the caching of models, too. The theoretical effect of these improvements is illustrated by a comparison of the search spaces on pathological examples. We also describe the basic features of the system Semprop, which is an efficient implementation of (some of) the developed techniques, and give the results of an experimental evaluation of the system on a number of practical examples.