Abstract
Solving Quantified Boolean Formulas
Horst Samulowitz
Doctor of Philosophy
Graduate Department of Computer Science
University of Toronto
2008
Many real-world problems do not have a simple
algorithmic solution and casting these
problems as search problems is often not only
the simplest way of casting them, but also
the most efficient way of solving them.
In this thesis we will present several
techniques to advance search-based algorithms
in the context of solving quantified boolean
formulas (QBF). QBF enables complex realworld
problems including planning, two-player games
and verification to be captured in a compact
and quite natural fashion. We will discuss
techniques ranging from straight forward
pre-processing methods utilizing strong rules
of inference to more sophisticated online
approaches such as dynamic partitioning.
Furthermore, we will show that all of the
presented techniques achieve an essential
improvement of the search process when
solving QBF. At the same time the displayed
empirical results also reveal the
orthogonality of the different techniques
with respect to performance. Generally
speaking each approach performs well on a
particular subset of benchmarks, but performs
poorly on others. Consequently, an adaptive
employment of the available techniques that
maximizes the performance would result in
further improvements.
We will demonstrate that such an adaptive
approach can pay off in practice, by
presenting the results of using machine
learning methods to dynamically select the
best variable ordering heuristics during
search.
| Identifer | oai:union.ndltd.org:TORONTO/oai:tspace.library.utoronto.ca:1807/11124 |
| Date | 28 July 2008 |
| Creators | Samulowitz, Horst Cornelius |
| Contributors | Bacchus, Fahiem |
| Source Sets | University of Toronto |
| Language | en_ca |
| Detected Language | English |
| Type | Thesis |
| Format | 1188014 bytes, application/pdf |
Page generated in 0.0019 seconds