|
PROBABILISTIC ANALYSIS OF A GENERALIZATION OF THE UNIT CLAUSE LITERAL SELECTION HEURISTIC FOR THE K-SATISFIABILITY PROBLEM?
MIN-TE CHAOy AND JOHN FRANCOz
Abstract. Two algorithms for the k-Satisfiability problem are presented and a probabilistic analysis is performed. The analysis is based on an instance distribution which is parameterized to simulate a variety of sample characteristics. The algorithms assign values to literals appearing in a given instance of k-Satisfiability, one at a time, until a solution is found or it is discovered that further assignments cannot lead to finding a solution. One algorithm chooses the next literal from a unit clause if one exists and randomly from the set of remaining literals otherwise. The other algorithm uses a generalization of the Unit-Clause rule as a heuristic for selecting the next literal: at each step a literal is chosen randomly from a clause containing the least number of literals. The algorithms run in polynomial time and it is shown that they find a solution to a random instance of k-Satisfiability with probability bounded from below by a constant greater than zero for two different ranges of parameter values. It is also shown that the second algorithm mentioned finds a solution with probability approaching one for a wide range of parameter values.
Key words. Satisfiability, NP-complete, Probabilistic Analysis, Resolution
1. Introduction. This paper is concerned with the probabilistic performance of heuristics for the k-Satisfiability problem (k-SAT). k-SAT is the problem of determining whether all of a collection of k-literal disjunctions (clauses) of Boolean variables are true for some truth assignment to the variables. This problem is NP-complete so there is no known polynomial time algorithm for solving it. k-SAT is a special case of the Satisfiability problem (SAT) which is the problem of determining whether all of a collection of disjunctions of Boolean variables are true for some truth assignment to the variables.
The analysis is based on an equally likely instance distribution which has been used in other studies of algorithms for this problem. This model has two parameters in addition to k: n, the number of disjunctions, and r, the number of variables from which disjunctions are composed. The model (which we refer to as M (n; r; k)) is described in greater detail in the next section. In [8] it was shown that, under M (n; r; k), if limn;r!1 nr > 2k ln 2 then random instances have no solution with probability approaching 1. In [1] it was shown that Backtracking solves k-SAT in exponential average time for all limiting ratios of n to r which are constant. In [8] it was shown that a variant of the Davis-Putnam Procedure [4] which searches for all solutions to a given instance requires exponential time in probability under M (n; r; k) for all limiting ratios of n to r which are constant. But, in [6] it was shown that, for all k >= 3, the Pure-Literal heuristic can be used to solve random instances of k-SAT in polynomial time with probability approaching 1 when limn;r!1 nr < 1. In [3] it was shown that the Unit-Clause and maximum occurring literal heuristics can be used to solve instances of 3-SAT generated according to M (n; r; 3) in polynomial time with probability bounded from below by a constant when limn;r!1 nr < 2:9. In this paper it is shown that a generalization of the Unit-Clause rule can be used as a literal selection heuristic to solve random instances of k-SAT, for 4 <= k <= 40, in polynomial
? This work is based on research supported in part by the Air Force Office of Scientific Research,
Grant No. AFOSR 84-0372.
y Department of Computer Engineering and Science, Case Western Reserve University, Cleveland,
OH 44106
z Department of Computer Science, Indiana University, Bloomington, Indiana 47405