Title: Transformations into Normal Forms for Quantified Circuits
Abstract: We consider the extension of Boolean circuits to quantified Boolean circuits by adding universal and existential quantifier nodes with semantics adopted from quantified Boolean formulas ( $\mbox{\rm QBF}$ ). The concept allows not only prenex representations of the form $\forall x_{1}\exists y_{1}...\forall x_{n}\exists y_{n}\ c$ where c is an ordinary Boolean circuit with inputs x 1,...,x n ,y 1,...,y n . We also consider more general non-prenex normal forms with quantifiers inside the circuit as in non-prenex $\mbox{\rm QBF}$ , including circuits in which an input variable may occur both free and bound. We discuss the expressive power of these classes of circuits and establish polynomial-time equivalence-preserving transformations between many of them. Additional polynomial-time transformations show that various classes of quantified circuits have the same expressive power as quantified Boolean formulas and Boolean functions represented as finite sequences of nested definitions ( $\mbox{\rm NBF}$ ). In particular, universal quantification can be simulated efficiently by circuits containing only existential quantifiers if overlapping scopes of variables are allowed.
Publication Year: 2011
Publication Date: 2011-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 3
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot