Journal Publications

U. Bubeck and H. Kleine Büning.
Encoding Nested Boolean Functions as Quantified Boolean Formulas.
Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 8(1):101-116, IOS Press, 2012.
[PDF Full Text]

U. Bubeck and H. Kleine Büning.
The Power of Auxiliary Variables for Propositional and Quantified Boolean Formulas.
Studies in Logic, 3(3):1-23, Chinese Association of Logic, 2010.
[PDF Full Text]

U. Bubeck and H. Kleine Büning.
A New 3-CNF Transformation by Parallel-Serial Graphs.
Journal Information Processing Letters, 109(7):376-379, Elsevier, 2009.
[PDF Accepted Author Manuscript] [Original Publication at Elsevier ScienceDirect]

U. Bubeck and H. Kleine Büning.
Models and Quantifier Elimination for Quantified Horn Formulas.
Journal Discrete Applied Mathematics, 156(10):1606-1622, Elsevier, 2008.
[PDF Accepted Author Manuscript] [Original Publication at Elsevier ScienceDirect]

Books and Book Chapters

U. Bubeck.
Model-Based Transformations for Quantified Boolean Formulas.
Doctoral Dissertation.
In: Dissertations in Artificial Intelligence (DISKI), vol. 329, Wolfgang Bibel (Ed.), IOS Press / Akademische Verlagsgesellschaft AKA, Amsterdam NL / Heidelberg DE, ISBN 978-1-60750-545-7, 2010.
[PDF Abstract German / English] [IOS Press]

H. Kleine Büning and U. Bubeck.
Theory of Quantified Boolean Formulas.
In: Handbook of Satisfiability, A. Biere, M. Heule, H. van Maaren, and T. Walsh (Eds.), IOS Press, ISBN 978-1-58603-929-5, pp. 735-760, 2009.

Conference Publications (Peer-Reviewed)

H. Kleine Büning, X. Zhao, and U. Bubeck.
Transformations into Normal Forms for Quantified Circuits.
Proc. 14th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2011), Springer LNCS 6695, pp. 245-258, 2011.
[PDF Accepted Author Manuscript] [Original Publication at www.springerlink.com]

U. Bubeck and H. Kleine Büning.
Rewriting (Dependency-)Quantified 2-CNF with Arbitrary Free Literals into Existential 2-HORN.
Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2010), Springer LNCS 6175, pp. 58-70, 2010.
[PDF Accepted Author Manuscript] [Original Publication at www.springerlink.com] [PDF Presentation Slides]

C. Peschiera, L. Pulina, A. Tacchella, U. Bubeck, O. Kullmann, and I. Lynce.
The Seventh QBF Solvers Evaluation (QBFEVAL'10).
Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2010), Springer LNCS 6175, pp. 237-250, 2010.
[Original Publication at www.springerlink.com]

H. Kleine Büning, X. Zhao, and U. Bubeck.
Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits.
Proc. 12th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2009), Springer LNCS 5584, pp. 391-397, 2009.
[PDF Accepted Author Manuscript] [Original Publication at www.springerlink.com]

U. Bubeck and H. Kleine Büning.
Bounded Universal Expansion for Preprocessing QBF.
Proc. 10th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2007), Springer LNCS 4501, pp. 244–257, 2007.
[PDF Accepted Author Manuscript] [Original Publication at www.springerlink.com]

U. Bubeck and H. Kleine Büning.
Dependency Quantified Horn Formulas: Models and Complexity.
Proc. 9th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2006), Springer LNCS 4121, pp. 198–211, 2006.
[PDF Accepted Author Manuscript] [Original Publication at www.springerlink.com]

U. Bubeck, H. Kleine Büning, and X. Zhao.
Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas.
Proc. 8th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2005), Springer LNCS 3569, pp. 386–392, 2005.
[PDF Accepted Author Manuscript] [Original Publication at www.springerlink.com]

Workshops

U. Bubeck and H. Kleine Büning.
Encoding Nested Boolean Functions as Quantified Boolean Formulas.
Proc. 3rd Guangzhou Symposium on Satisfiability in Logic-Based Modeling, pp. 10-11, Zhuhai, China, 2010.
[PDF Presentation Slides]

U. Bubeck, H. Kleine Büning, A. Remshagen, and X. Zhao.
Expressiveness and Complexity of Subclasses of Quantified Boolean Formulas.
Workshop on Propositional Proof Complexity, Federated Logic Conference (FLoC) 2010, Edinburgh, UK, 2010.
[PDF Full Text]

U. Bubeck and H. Kleine Büning.
Dependency Quantified Boolean Formulas.
Poster, Deduktionstreffen 2007 der Gesellschaft für Informatik (GI), Koblenz, Germany, 2007.

U. Bubeck and H. Kleine Büning.
Dependency Quantified Horn Formulas.
Proc. 2nd Guangzhou Symposium on Satisfiability in Logic-Based Modeling, pp. 21-34, Guangzhou, China, 2006.

Master's Thesis