Augmenting Local Search for Satisfiability

I hereby declare that I am the sole author of this thesis. This is a true copy of the thesis, including any required final revisions, as accepted by my examiners. I understand that my thesis may be made electronically available to the public. ii This dissertation explores approaches to the satisfiability problem, focusing on local search methods. The research endeavours to better understand how and why some local search methods are effective. At the root of this understanding are a set of metrics that characterize the behaviour of local search methods. Based on this understanding, two new local search methods are proposed and tested, the first, SDF, demonstrating the value of the insights drawn from the metrics, and the second, ESG, achieving state-of-the-art performance and generalizing the approach to arbitrary 0-1 integer linear programming problems. This generality is demonstrated by applying ESG to combinatorial auction winner determination. Further augmentations to local search are proposed and examined, exploring hybrids that incorporate aspects of backtrack search methods. iii Acknowledgements I owe thanks to many people for the completion of this dissertation. • To Jim Linders and Fakhri Karray for the opportunities they afforded me. • To my committee members, Nancy Day and Peter van Beek, for their insights. • To Bart Selman and John Thistle, for kindly agreeing to act as examiners. • To Rob Holte and everyone at the University of Alberta. • To my advisor, Dale Schuurmans, with whom it has been a pleasure and privilege to work (albeit often in the wee hours). • To my schoolmates, colleagues, and friends for their comments, criticism, and fun: Relu, Ali, Dana, Fuchun, and Paul (Remember: Aim high... fall hard)