Encoding Reachability with Quantification

ABSTRACT. We report on techniques for translating bounded propositional reachability problems into Quantified Boolean Formulae (QBF). The techniques exploit the binary-tree structure of the QBF quantification to produce encodings logarithmic in the size of the instance and thus exponentially smaller than the corresponding SAT encoding with the same bound. We briefly describe our experimental results, and discuss the challenging structure that is implicit in these encodings.