Backtracking Based k-SAT Algorithms
- PDF / 2,846,404 Bytes
- 37 Pages / 547.087 x 737.008 pts Page_size
- 46 Downloads / 165 Views
B
B
Backtracking Based k-SAT Algorithms 2005; Paturi, Pudlák, Saks, Zane RAMAMOHAN PATURI 1 , PAVEL PUDLÁK2 , MICHAEL SAKS3 , FRANCIS Z ANE4 1 Department of Computer Science and Engineering, University of California at San Diego, San Diego, CA, USA 2 Mathematical Institute, Academy of Science of the Czech Republic, Prague, Czech Republic 3 Department of Mathematics, Rutgers, State University of New Jersey, Piscataway, NJ, USA 4 Bell Laboraties, Lucent Technologies, Murray Hill, NJ, USA
Problem Definition Determination of the complexity of k-CNF satisfiability is a celebrated open problem: given a Boolean formula in conjunctive normal form with at most k literals per clause, find an assignment to the variables that satisfies each of the clauses or declare none exists. It is well-known that the decision problem of k–CNF satisfiability is NP-complete for k 3. This entry is concerned with algorithms that significantly improve the worst case running time of the naive exhaustive search algorithm, which is poly(n)2n for a formula on n variables. Monien and Speckenmeyer [8] gave the first real improvement by giving a simple algorithm whose running time is O(2(1"k )n ), with " k > 0 for all k. In a sequence of results [1,3,5,6,7,9,10,11,12], algorithms with increasingly better running times (larger values of " k ) have been proposed and analyzed. These algorithms usually follow one of two lines of attack to find a satisfying solution. Backtrack search algorithms make up one class of algorithms. These algorithms were originally proposed by Davis, Logemann and Loveland [4] and are sometimes called Davis–Putnam procedures. Such algorithms search for a satisfying assignment
by assigning values to variables one by one (in some order), backtracking if a clause is made false. The other class of algorithms is based on local searches (the first guaranteed performance results were obtained by Schöning [12]). One starts with a randomly (or strategically) selected assignment, and searches locally for a satisfying assignment guided by the unsatisfied clauses. This entry presents ResolveSat, a randomized algorithm for k-CNF satisfiability which achieves some of the best known upper bounds. ResolveSat is based on an earlier algorithm of Paturi, Pudlák and Zane [10], which is essentially a backtrack search algorithm where the variables are examined in a randomly chosen order. An analysis of the algorithm is based on the observation that as long as the formula has a satisfying assignment which is isolated from other satisfying assignments, a third of the variables are expected to occur as unit clauses as the variables are assigned in a random order. Thus, the algorithm needs to correctly guess the values of at most 2/3 of the variables. This analysis is extended to the general case by observing that there either exists an isolated satisfying assignment, or there are many solutions so the probability of guessing one correctly is sufficiently high. ResolveSat combines these ideas with resolution to obtain significantly improved bounds [9]. In fact
Data Loading...
