An Empirical Analysis of Search in GSAT

TL;DR

This paper provides an empirical study of GSAT's search process for propositional satisfiability, revealing detailed behavior patterns and scaling properties through extensive experiments on random 3SAT problems.

Contribution

It offers a detailed analysis of GSAT's two-phase search process and introduces numerical conjectures about its behavior, aiding future theoretical work.

Findings

GSAT's search exhibits simple scaling with problem size.

The hill-climbing phase's length and gradient follow predictable patterns.

Plateau search's score and branching rate decay exponentially.

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 accounts. We describe in detail the two phases of search: rapid hill-climbing followed by a long plateau search. We demonstrate that when applied to randomly generated 3SAT problems, there is a very simple scaling with problem size for both the mean number of satisfied clauses and the mean branching rate. 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.