Improved Upper Bounds for 3-SAT Kazuo Iwama 1 CNF Satisfiability The CNF Satisfiability problem is to determine, given a CNF formula F , whether or not there exists a satisfying assignment for F . If each clause of F contains at most k literals, then F is called a k -CNF formula and the problem is called k -SAT. For small k 's, especially for k = 3, there exists a lot of algorithms which run significantly faster than the trivial 2n bound. The following list summarizes those algorithms where a constant c means that the algorithm runs in time O(cn ). Roughly speaking most algorithms are based on Davis-Putnam. [Sch99] is the first local search algorithm which gives a guaranteed performance for general instances and [DGH+02], [HSSW02], [BS03] and [Rol03] follow up this Schšning's approach. o 3-SAT 1.782 1.618 1.588 1.579 1.505 1.481 1.362 1.334 1.3302 1.3290 1.3280 1.324 4-SAT 1.835 1.839 1.682 1.6 1.476 1.5 1.474 5-SAT 1.867 1.928 1.742 1.667 1.569 1.6 6-SAT 1.888 1.966 1.782 1.75 1.637 1.667 type det. det. prob. det. det. det. prob. prob. prob. prob. prob. prob. ref. [PPZ97] [MS85] [PPZ97] [Sch92] [Kul99] [DGH+02] [PPSZ98] [Sch99] [HSSW02] [BS03] [Rol03] [*] Suguru Tamaki the 4-SAT case is very similar and may be omitted. The same approach does not improve the bounds for 5-SAT or more. 3 Background The algorithm of [PPSZ98] is called ResolveSat, which is based on a randomized Davis-Putnam combined with bounded resolution. ResolveSat behaves like local search algorithms, that is, it takes an random assignment and a random variable ordering as an input and tries to modify initial assignment to be satisfiable one by using Davis-Putnam procedure. This algorithm has the unique feature that it achieves a quite nice performance, O(1.3071n ), for a unique 3-CNF formula, i.e., a formula which has only one satisfying assignment. As the number m of satisfying assignments grows, the bound, denoted by TPPSZ (m), degenerates, i.e., TPPSZ (m) is an increasing function. [PPSZ98] needed a lot of effort to stop this degeneration by formalizing the intuition that if the formula has many satisfying assignments, then finding one should be easy. In contrast, the algorithm of [Sch99] is based on the standard local search for which the above intuition is obviously true. Namely its running time TSCH (m) is the worst when m = 1 and then decreases. Recall that TPPSZ (1) < TSCH (1) = O(1.334n ). So, if we run the two algorithms in parallel, then the running time is bounded by min{TPPSZ (m), TSCH (m)} which becomes maximum (= TPPSZ (m0 ) = TSCH (m0 )) at m = m0 . Obviously TSCH (m0 ) < TSCH (1). Although TSCH (1) is not the currently best, there is a lot of hope of breaking it since TPPSZ (1) is much better than the current best. Unfortunately, this approach has an obstacle. We know the value of TPPSZ (m) but we do not know that of TSCH (m) for the following reason. To obtain TSCH (m), it appears that we need to know the Hamming distance between the (randomly chosen) initial assignment and its closest satisfying assignment. However, there is no obvious way of doing so, since it is quite hard to analyze how (multi) satisfying assignments of a 3-CNF formula can distribute in the whole space of 2n assignments. 4 Our solution Both [PPSZ98] and [Sch99] repeat an exponential number of tries. Each try of [Sch99], denoted by SCH, looks like: 2 Our Contribution Our new bounds are denoted by [*] in the above list, namely we prove: Theorem 2.1. For any satisfiable n-variable 3-CNF ( 4-CNF ) formula F , there exists a randomized algorithm that finds a satisfying assignment of F in expected running time O(1.324n ) (O(1.474n )). The basic idea is to combine two existing algorithms, the one by Paturi, PudlŽk, Saks and Zane [PPSZ98] and the a other by Schšning [Sch99]. It should be noted, however, o that simply running the two algorithms independently does not seem to work. Also, our approach can escape one of the most complicated portions in the analysis of [PPSZ98]. In this paper we focus on the 3-SAT case; Scho ol of Informatics, Kyoto University, Kyoto 606-8501, Japan. Email: {iwama, tamak}@kuis.kyoto-u.ac.jp Copyright © 2004 by the Association for Computing Machinery, Inc. and the Society for industrial and Applied Mathematics. All Rights reserved. Printed in The United States of America. No part of this book may be reproduced, stored, or transmitted in any manner without the written permission of the publisher. For information, write to the Association for Computing Machinery, 1515 Broadway, New York, NY 10036 and the Society for Industrial and Applied Mathematics, 3600 University City Science Center, Philadelphia, PA 19104-2688 328 (1) Generate a random initial assignment y . (2) Execute a local search for 3n steps starting from y . Each try of [PPSZ98], denoted by PPSZ, has a similar structure, namely: (1) Generate a random initial assignment y . (2) Generate a random initial permutation of [1, n]. (3) Execute Davis-Putnam based on y and , which takes at most n steps. As mentioned previously, we cannot analyze a simple repetition of SCH and PPSZ. Our solution is to use the same random assignment for each execution of SCH and PPSZ. Namely, our algorithm is: rep eat I times (1) Generate a random initial assignment y . (2) Only (2) of SCH; if a satisfying assignment is found, then answer YES. (3) Only (2) and (3) of PPSZ; if a satisfying assignment is found, then answer YES. end Answer NO. Now let p0 be the probability that the above single try (a single execution of (1)-(3)) finds a satisfying assignment if the given formula is satisfiable. To obtain p0 , there are two key lemmas, for which we need some definitions. Let S (F ) be the set of satisfying assignments of the formula F . A set of assignments, B {0, 1}n , is called a subcube, if B is determined by fixing a certain number of variables. For example, {0000, 0001, 0010, 0011} is a subcube obtained by fixing x1 = x2 = 0. Now it turns out that the whole space, {0, 1}n , can always be partitioned into a family {Bz | z S (F )} of disjoint subcubes so that Bz contains z S (F ) but no other z S (F ) - {z }. (This fact can be easily shown by induction.) Note that the existence (not explicit construction) of such partition suffices for our purpose. Now, given the formula F and the subcube Bz , (F, z |Bz ) ( (F, z |Bz ), resp.) is defined as the probability (averaged over y ) that a single execution of (2) and (3) of PPSZ (a single execution of (2) of SCH, resp.) finds the assignment z under the condition that the initial assignment y Bz . z is defined as log2 (2n /|Bz |) , n namely, it is the ratio of the number of the variables fixed to determine Bz . z = Lemma 4.1. ([PPSZ98]) For any satisfiable 3-CNF formula F and any partition Bz described above, the value (F, z |Bz ) is bounded as fol lows: (F, z |Bz ) 2-((1- )-(1- - )z )n-o(n) , where = 2 - 2 ln 2 and = 1.115. Lemma 4.2. For any satisfiable 3-CNF formula F and any partition Bz described above, the value (F, z |Bz ) is bounded as fol lows: 3 (1-z )n (F, z |Bz ) 4 . Proof of Lemma 4.2 follows the next lemma: Lemma 4.3. ([Sch99]) Suppose that SCH starts from the initial assignment y and there is a satisfying assignment z . Let d(y , z ) be the Hamming distance between y and z . Then the probability that a single try of SCH starting from y finds z is at least (1/2)d(y,z) . Recall that our new try uses the same y for both SCH and PPSZ. If y Bz , then apparently z n variables are assigned correct values, i.e., d(y , z ) (1 - z )n. Now our success probability of a single try is at least the probability of Lemmas 4.1 and 4.2, i.e., p0 max{ (F, z |Bz ), (F, z |Bz )}, which becomes minimum (= (1.3238-n )) when z = 0.02513. Now the standard probabilistic argument allows us to claim that our algorithm finds a satisfying assignment with high probability for I = O(1.324n ). Recall that I is the number of repetitions. References [BS03] S. Baumer and R. Schuler. Improving a probabilistic 3SAT Algorithm by Dynamic Search and Independent Clause Pairs. ECCC TR03-010, 2003. Also presented at SAT 2003. [DGH+02] E. Dantsin, A. Goerdt, E. A. Hirsch, R. Kannan, J. Kleinberg, C. Papadimitriou, P. Raghavan, and 2 U. Schšning. A deterministic 2 - k+1 algorithm for k-SAT o based on local search. TCS, 289(1):69­83, 2002. [HSSW02] T. Hofmeister, U. Schšning, R. Schuler and O. Watano abe. Probabilistic 3-SAT Algorithm Further Improved. Proc. 19th STACS, LNCS 2285, 2002. [Kul99] O. Kullmann, New metho ds for 3-SAT decision and worst-case analysis. TCS, 223(1-2):1­72, 1999. [MS85] B. Monien and E. Speckenmeyer. Solving satisfiability less than 2n steps. Discrete Appl. Math., 10:287­295, 1985. [PPSZ98] R. Paturi, P. PudlŽk, M. E. Saks, and F. Zane. An a improved exp onential-time algorithm for k-SAT. Proc. 39th FOCS, 1998. [PPZ97] R. Paturi, P. PudlŽk, and F. Zane. Satisfiability coding a lemma. Proc. 38th FOCS, 1997. [Rol03] D. Rolf. 3-SAT RTIME (O(1.32793n )). ECCC TR03054, 2003. [Sch92] I. Schiermeyer. Solving 3-Satisfiability in less than 1.579n steps. CSL 92, LNCS 702, 1992. [Sch99] U. Schšning. A probabilistic algorithm for k-SAT and o constraint satisfaction problems. Proc. 40th FOCS, 1999. 329