test Browse by Author Names Browse by Titles of Works Browse by Subjects of Works Browse by Issue Dates of Works
       

Advanced Search
Home   
 
Browse   
Communities
& Collections
  
Issue Date   
Author   
Title   
Subject   
 
Sign on to:   
Receive email
updates
  
My Account
authorized users
  
Edit Profile   
 
Help   
About T-Space   

T-Space at The University of Toronto Libraries >
School of Graduate Studies - Theses >
Doctoral >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1807/11124

Title: Solving Quantified Boolean Formulas
Authors: Samulowitz, Horst Cornelius
Advisor: Bacchus, Fahiem
Department: Computer Science
Keywords: Artificial Intelligence
Satisfiability
Search
Quantified Boolean Formulas
Issue Date: 28-Jul-2008
Abstract: 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.
URI: http://hdl.handle.net/1807/11124
Appears in Collections:Doctoral
Department of Computer Science - Doctoral theses

Files in This Item:

File Description SizeFormat
Samulowitz_Horst_C_200803_PhD_thesis.pdf1.16 MBAdobe PDF
View/Open

Items in T-Space are protected by copyright, with all rights reserved, unless otherwise indicated.

uoft