Abstract
In this paper, we consider the problem of compactly representing nested instantiations of propositional subformulas with different arguments as quantified Boolean formulas (QBF). We develop a generic QBF encoding pattern which combines and generalizes existing QBF encoding techniques for simpler types of redundancy.
We obtain an equivalence-preserving transformation in linear time from the PSPACE-complete language of nested Boolean functions (NBF), also called Boolean programs, to prenex QBF. A transformation in the other direction from QBF to NBF is also possible in at most quadratic time by simulating quantifier expansion.