Return to search

Solving Quantified Boolean Formulas

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.

Identiferoai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:OTU.1807/11124
Date28 July 2008
CreatorsSamulowitz, Horst Cornelius
ContributorsBacchus, Fahiem
Source SetsLibrary and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada
Languageen_ca
Detected LanguageEnglish
TypeThesis
Format1188014 bytes, application/pdf

Page generated in 0.0019 seconds