Previous: TR 94-12 Next: TR 95-02

Intellektik: Technical report 94-17

The GSAT/SA-Familiy -- Relating greedy satisifability testing to simulated annealing

S. Hölldobler and H. Hoos and A. Strohmaier and A. Weiß

In this paper, we investigate and relate various variants of \the greedy satisfiability tester GSAT. We present these algorithms as members of a whole family of algorithms for finding a model for satisfiable propositional logic formulas. In particular, all algorithms can be formulated as instances of the same generic frame GenSAT. Comparing the algorithms, we do not only concentrate on their overall performance, but are also interested in how properties like locality or different kinds of randomness influence the performance. To the end we define a new, theoretically complete instance of GenSAT. This variant can be viewed as a reformulation of simulated annealing (SA) within the GSAT family and, thus, defines a link between GSAT and SA. For most of the algorithms experiments have been performed using very hard, randomly generated propositional logic formulas. The results of these experiments are also reported.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry