
PROBABILISTIC ANALYSIS OF A GENERALIZATION OF THE UNIT CLAUSE LITERAL SELECTION HEURISTIC FOR THE KSATISFIABILITY PROBLEM?
MINTE CHAOy AND JOHN FRANCOz
Abstract. Two algorithms for the kSatisfiability 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 kSatisfiability, 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 UnitClause 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 kSatisfiability 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, NPcomplete, Probabilistic Analysis, Resolution
1. Introduction. This paper is concerned with the probabilistic performance of heuristics for the kSatisfiability problem (kSAT). kSAT is the problem of determining whether all of a collection of kliteral disjunctions (clauses) of Boolean variables are true for some truth assignment to the variables. This problem is NPcomplete so there is no known polynomial time algorithm for solving it. kSAT 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 kSAT 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 DavisPutnam 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 PureLiteral heuristic can be used to solve random instances of kSAT in polynomial time with probability approaching 1 when limn;r!1 nr < 1. In [3] it was shown that the UnitClause and maximum occurring literal heuristics can be used to solve instances of 3SAT 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 UnitClause rule can be used as a literal selection heuristic to solve random instances of kSAT, 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 840372.
y Department of Computer Engineering and Science, Case Western Reserve University, Cleveland,
OH 44106
z Department of Computer Science, Indiana University, Bloomington, Indiana 47405