Inference and search for the propositional satisfiability problem

Lyndon Drake

(York University)

Propositional satisfiability (SAT) is the archetypal NP-complete problem, with important practical applications. Backtracking search is the most effective way of solving many SAT problems. It is sometimes possible to improve the performance of search-based SAT solvers by using inference methods. I will present an overview of existing methods, such as unit propagation and conflict recording, as well as my own work over the course of my PhD.
Tuesday 1st July 2003, 14:00
Robert Recorde Room
Department of Computer Science