The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #634

Title:An Empirical Analysis of Search in Gsat
Authors:Gent,I; Walsh,T
Date:Jun 1993
Presented:Submitted to Journal of Artificial Intelligence Research
Abstract:We describe an extensive study of search in GSAT, an approximation procedure for propositional satisfiability. GSAT performs greedy hill-climbing on the number of satisfied clauses in a truth assignment. Our experiments provide a more complete picture of GSAT's search than previous informal accounts. We describe in detail the two phases of search: rapid hill-climbing followed by long plateau search. We demonstrate that when applied to randomly generated 3-SAT problems, both the number of satisfied clauses and the branching rate scale linearly with N, the number of variables. Our results allow us to make detailed numerical conjectures about the length of the hill-climbing phase, the average gradient of this phase, and to conjecture that both the average score and average branching rate decay exponentially during plateau search. We end by showing how these results can be used to direct future theoretical analysis. This work provides a case study of how computer experiments can be used to improve understanding of the theoretical properties of algorithms.

[Search These Pages] [DAI Home Page] [Comment]