U. Bubeck and H. Kleine Büning.
Learning Boolean Specifications.
Journal Artificial Intelligence (ARTINT), Elsevier, 2015.
[Original Publication at Elsevier ScienceDirect]

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]

U. Bubeck.
Model-Based Transformations for Quantified Boolean Formulas.
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 Full Text] [Original Publication at 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.

U. Bubeck and H. Kleine Büning.
Nested Boolean Functions as Models for Quantified Boolean Formulas.
Proc. 16th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2013), Springer LNCS 7962, pp. 267-275, 2013.
[PDF Accepted Author Manuscript] [Original Publication at www.springerlink.com]

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]

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.

U. Bubeck.
Dependency Quantified Boolean Formulas.
Universität Hannover, Institut für Theoretische Informatik, Germany, 2013.
[PDF Presentation Slides]

U. Bubeck.
Quantified Boolean Formulas: Complexity and Expressiveness.
Dagstuhl Seminar 12471 "SAT Interactions", Schloss Dagstuhl Leibniz-Zentrum für Informatik, Germany, 2012.
[PDF Presentation Slides]

U. Bubeck.
Model-Based Transformations for Quantified Boolean Formulas.
Chinese Academy of Sciences, Institute of Software (ISCAS), Beijing, China, 2009.

U. Bubeck.
Model-Based Transformations for Quantified Boolean Formulas.
Sun Yat-Sen University, Institute of Logic and Cognition, Guangzhou, China, 2009.

U. Bubeck.
Design of a Modular Platform for Automated Theorem Proving in Multiple Logics.
M.S. Thesis, San Diego State University, San Diego, USA, 2003.
[Software]

U. Bubeck.
Multibiometric Authentication: An Overview of Recent Developments.
Term Project CS574, San Diego State University, San Diego, USA, 2003.
[PDF Full Text]

U. Bubeck and D. Sanchez.
Biometric Authentication: Technology and Evaluation.
Term Project CS574, San Diego State University, San Diego, USA, 2003.
[PDF Full Text]