Quantified Boolean Formulas (QBF)

Quantified Boolean formulas generalize propositional logic by allowing variables to be quantified universally or existentially. This enhancement allows problems from many areas, such as planning or verification, to be encoded in a natural way. The resulting formulas are often significantly more compact than their propositional equivalents, but also more difficult to solve. Not all usage patterns of quantifiers seem equally effective, which makes it important to balance clarity and conciseness versus decision complexity. We are therefore investigating

• relationships between formula structure and quantifier expressiveness,

• preprocessing that eliminates weak quantifiers,

• useful subclasses with lower complexity,

• and suitable encoding patterns.

Furthermore, we are interested in comparing the expressive power of quantified Boolean formulas with different representations, for example Boolean circuits.

Contact Persons

• Prof. Dr. Hans Kleine Büning
• Dr. Uwe Bubeck

• Prof. Dr. Xishun Zhao (Sun Yat-Sen University, Guangzhou, China)

Publications

U. Bubeck, H. Kleine Büning.
Encoding Nested Boolean Functions as Quantified Boolean Formulas.
In Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 8, no. 1, pp. 101-116,. IOS Press 2012

[Show BibTeX]

@article{Bubeck-2012a,
  author = {U. Bubeck AND H. Kleine B{\"u}ning},
  title = {Encoding Nested Boolean Functions as Quantified Boolean Formulas},
  journal = {Journal on Satisfiability, Boolean Modeling and Computation (JSAT)},
  year = {2012},
  volume = {8},
  number = {1},
  pages = {101-116},
  month = {},
  note = {}
}

H. Kleine Büning, X. Zhao, U. Bubeck.
Transformations into Normal Forms for Quantified Circuits.
In Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing (SAT 2011). Springer, Lecture Notes in Computer Science, vol. 6695, pp. 245-258, 2011

[Show BibTeX]

@inproceedings{Bubeck-2011,
  author = {H. Kleine B{\"u}ning AND X. Zhao AND U. Bubeck},
  title = {Transformations into Normal Forms for Quantified Circuits},
  booktitle = {Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing (SAT 2011)},
  year = {2011}
}

C. Peschiera, L. Pulina, A. Tacchella, U. Bubeck, O. Kullmann, I. Lynce.
The Seventh QBF Solvers Evaluation (QBFEVAL'10).
In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing –(SAT 2010). Springer, Lecture Notes in Computer Science, vol. 6175, pp. 237-250, 2010

[Show BibTeX]

@inproceedings{Peschiera-2010,
  author = {C. Peschiera AND L. Pulina AND A. Tacchella AND U. Bubeck AND O. Kullmann AND I. Lynce},
  title = {The Seventh QBF Solvers Evaluation (QBFEVAL'10)},
  booktitle = {Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing –(SAT 2010)},
  year = {2010}
}

U. Bubeck, H. Kleine Büning.
Rewriting (Dependency-)Quantified 2-CNF with Arbitrary Free Literals into Existential 2-HORN.
In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010). Springer, Lecture Notes in Computer Science, vol. 6175, pp. 58-70, 2010

[Show BibTeX]

@inproceedings{Bubeck-2010,
  author = {U. Bubeck AND H. Kleine B{\"u}ning},
  title = {Rewriting (Dependency-)Quantified 2-CNF with Arbitrary Free Literals into Existential 2-HORN},
  booktitle = {Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010)},
  year = {2010}
}

U. Bubeck, H. Kleine Büning.
The Power of Auxiliary Variables for Propositional and Quantified Boolean Formulas.
In Studies in Logic, vol. 3, no. 3, pp. 1-23,. 2010

[Show BibTeX]

@article{Bubeck-2010b,
  author = {U. Bubeck AND H. Kleine B{\"u}ning},
  title = {The Power of Auxiliary Variables for Propositional and Quantified Boolean Formulas},
  journal = {Studies in Logic},
  year = {2010},
  volume = {3},
  number = {3},
  pages = {1--23},
  month = {},
  note = {}
}

U. Bubeck.Wolfgang Bibel (eds.):
Model-Based Transformations for Quantified Boolean Formulas., vol. 329
. IOS Press 2010

[Show BibTeX]

@book{Bubeck-2010d,
  author = {U. Bubeck},
  editor = {Wolfgang Bibel},
  title = {Model-Based Transformations for Quantified Boolean Formulas},
  publisher = {IOS Press},
  year = {2010}
}

U. Bubeck, H. Kleine Büning.
A new 3-CNF Transformation by Parallel-Serial Graphs.
In Information Processing Letters, vol. 109, no. 7, pp. 376-379,. 2009

[Show BibTeX]

@article{Bubeck-2009b,
  author = {U. Bubeck AND H. Kleine B{\"u}ning},
  title = {A new 3-CNF Transformation by Parallel-Serial Graphs},
  journal = {Information Processing Letters},
  year = {2009},
  volume = {109},
  number = {7},
  pages = {376--379},
  month = {},
  note = {}
}

H. Kleine Büning, U. Bubeck.
Theory of Quantified Boolean Formulas.
In Biere, Armin and Heule, Marijin and van Maaren, Hans and Walsh, Toby (eds.): Handbook of Satisfiability, pp. 735-760,. IOS Press 2009

[Show BibTeX]

@incollection{KB-2009a,
  author = {H. Kleine B{\"u}ning AND U. Bubeck},
  title = {Theory of Quantified Boolean Formulas},
  booktitle = {Handbook of Satisfiability},
  publisher = {IOS Press},
  year = {2009}
}

H. Kleine Büning, X. Zhao, U. Bubeck.
Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits.
In Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing –(SAT 2009). Springer, Lecture Notes in Computer Science, vol. 5584, pp. 391-397, 2009

[Show BibTeX]

@inproceedings{KB-2009b,
  author = {H. Kleine B{\"u}ning AND X. Zhao AND U. Bubeck},
  title = {Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits},
  booktitle = {Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing –(SAT 2009)},
  year = {2009}
}

U. Bubeck, H. Kleine Büning.
Models and Quantifier Elimination for Quantified Horn Formulas.
In Discrete Applied Mathematics, vol. 156, no. 10, pp. 1606-1622,. 2008

[Show BibTeX]

@article{Bubeck-2008,
  author = {U. Bubeck AND H. Kleine B{\"u}ning},
  title = {Models and Quantifier Elimination for Quantified Horn Formulas},
  journal = {Discrete Applied Mathematics},
  year = {2008},
  volume = {156},
  number = {10},
  pages = {1606--1622},
  month = {},
  note = {}
}

U. Bubeck, H. Kleine Büning.
Bounded Universal Expansion for Preprocessing QBF.
In Marques-Silva, Joao and Sakallah, Karem (eds.): Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing –(SAT 2007). Springer, Lecture Notes in Computer Science, vol. 4501, pp. 244-257, 2007

[Show BibTeX]

@inproceedings{Bubeck-2007,
  author = {U. Bubeck AND H. Kleine B{\"u}ning},
  title = {Bounded Universal Expansion for Preprocessing QBF},
  booktitle = {Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing –(SAT 2007)},
  year = {2007}
}

U. Bubeck, H. Kleine Büning.
Dependency Quantified Horn Formulas: Models and Complexity.
In Biere, Armin and Gomes, Carla (eds.): Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT 2006). Springer, Lecture Notes in Computer Science, vol. 4121, pp. 198-211, 2006

[Show BibTeX]

@inproceedings{Bubeck-2006,
  author = {U. Bubeck AND H. Kleine B{\"u}ning},
  title = {Dependency Quantified Horn Formulas: Models and Complexity},
  booktitle = {Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT 2006)},
  year = {2006}
}

U. Bubeck, H. Kleine Büning, X. Zhao.
Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas.
In Bacchus, Fahiem and Walsh, Toby (eds.): Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005). Springer, Lecture Notes in Computer Science, vol. 3569, pp. 386-392, 2005

[Show BibTeX]

@inproceedings{Bubeck-2005,
  author = {U. Bubeck AND H. Kleine B{\"u}ning AND X. Zhao},
  title = {Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas},
  booktitle = {Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005)},
  year = {2005}
}