Previous: TR 93-18 Next: TR 94-03

Intellektik: Technical report 94-01

GSAT and Simulated Annealing --- a comparison

A. Beringer and G. Aschemann and H. Hoos and M. Metzger and A. Weiß

The question of satisfiability for a given propositional formula arises in many areas of AI. Especially finding a model for a satisfiable formula is very important though known to be NP-complete. There exist complete algorithms for satisfiability testing like the Davis-Putnam-Algorithm, but they often do not construct a satisfying assignment for the formula. Furthermore, existing complete procedures are not practically applicable for more than 400 or 500 variable problems and in practice take too much time to find a solution. Recently, a (in practice) very fast, though incomplete, procedure, the model generating algorithm GSAT, has been introduced and several refined variants were created. Another method is Simulated Annealing (SA). Both approaches have already been compared with different results. We clarify these differences and do a more elaborate comparison using identical problems for both algorithms. We show that the performance of an already optimized variant of GSAT and an ordinary SA algorithm are more or less the same and that these attempts to further improve the performance of basic GSAT have lead to a procedure very similar to SA. Moreover we investigate how these algorithms can be parallelized.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry