On the accuracy and running time of GSAT

TL;DR

This paper introduces a formal measure of accuracy for randomized SAT algorithms and studies how the GSAT algorithm's running time and accuracy depend on input properties, showing exponential growth in certain cases.

Contribution

It defines a formal notion of accuracy for randomized algorithms and analyzes GSAT's performance relative to input formula characteristics.

Findings

GSAT's running time grows exponentially with the number of variables.

Accuracy depends on clause-to-variable ratio and number of solutions.

Exponential growth observed for random 3-CNF and graph coloring formulas.

Abstract

Randomized algorithms for deciding satisfiability were shown to be effective in solving problems with thousands of variables. However, these algorithms are not complete. That is, they provide no guarantee that a satisfying assignment, if one exists, will be found. Thus, when studying randomized algorithms, there are two important characteristics that need to be considered: the running time and, even more importantly, the accuracy --- a measure of likelihood that a satisfying assignment will be found, provided one exists. In fact, we argue that without a reference to the accuracy, the notion of the running time for randomized algorithms is not well-defined. In this paper, we introduce a formal notion of accuracy. We use it to define a concept of the running time. We use both notions to study the random walk strategy GSAT algorithm. We investigate the dependence of accuracy on properties of input formulas such as clause-to-variable ratio and the number of satisfying assignments. We demonstrate that the running time of GSAT grows exponentially in the number of variables of the input formula for randomly generated 3-CNF formulas and for the formulas encoding 3- and 4-colorability of graphs.