Title:　 Transformations and Expressiveness Relations for Quantified Boolean Formulas, Boolean Circuits, and Boolean Functions.

Speaker: Hans Kleine Büning (University of Paderborn, Germany)

Time:　  3pm, Thursday, March 17

Venue:　 Lecture room, Lab for Computer Science, Level 3 Building #5, Institute of Software, CAS

Abstract:

Nowadays, SAT-solvers are widely used for various applications as bounded model checking etc. In comparison to propositional formulas quantified Boolean formulas (QBF), Boolean circuits, and Boolean functions allow sharing of common sub-expressions which can lead to significantly shorter encodings. We consider the extension of Boolean circuits to quantified Boolean circuits by adding universal and existential quantifier nodes with a semantics adopted from QBF. The concept allows not only prenex representations. Instead, we also consider more general non-prenex normal forms with quantifiers inside the circuit as in non-prenex  QBF, including circuits in which an input variable may occur both free and bound. Besides a discussion of the expressive power of these classes of circuits, we establish polynomial-time equivalence-preserving transformations between many of them, with additional links to and from QBF and Boolean functions represented as finite sequences of nested definitions NBF.

SHORT VITA of the speaker:

Prof. Dr. Hans KleineBüning, born on June 4, 1948 in Innsbruck, Austria, graduated as "Diplom-Mathematiker" in 1975 at the University of Münster, Germany. In 1977 he received his PhD summa cum laude in Mathematics from the University of Münster. Between 1982 and 1987 he was an Associate Professor at the TH Karlsruhe, Germany and then until 1991 full Professor of Computer Science at the University of Duisburg, Germany. As of 1991 he is a full Professor of Computer Science at the University of Paderborn, Germany. In 1991 he turned down an offer from the RWTH Aachen, Germany. In 1986 he worked at the IBM Scientific Center in Heidelberg, Germany for nine months. He is the co-founder of two conference series: CSL (Computer Science Logic) and SAT (Theory and Applications of Satisfiability Testing). He is member of the Board of Directors of the C-Lab, the s-lab (Software Quality Lab, a joint research and development institute run by the University of Paderborn along with six industrial partners), the International Graduate School on Dynamical Intelligent Systems, and of the Paderborn Institute of Advanced Studies in Computer Science and Engineering (PACE). He is president of the international scientific association SAT (Theory and Applications of Satisfiability Testing).