You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Encoding Nested Boolean Functions as Quantified Boolean Formulas

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.