Constraints

23 March 2010

Immediate SAT restarts?

Filed under: Commentary,Question — András Salamon @ 20:28
Tags:

SAT solvers have been moving to more frequent restarts. Can restarts completely replace local search?

Uwe Schöning‘s randomised Walksat algorithm for k-SAT assumes some local search. The algorithm in his 2002 paper A Probabilistic Algorithm for k-SAT Based on Limited Local Search and Restart, guesses a random assignment for the {n} variables, then {3n} times tries randomly flipping one of the literals in one of the non-satisfied clauses. This procedure is repeated {30(4/3)^n} times (for {k=3}). This has a one-sided error of at most {2.1\times 10^-9}. In other words, it achieves an {O((4/3)^n)} runtime bound for satisfiable instances of 3-SAT, with probability very, very nearly 1. In contrast, the brute force algorithm for SAT may require {\Omega(n2^n)} time.

Walksat without local search will find a satisfying assignment with probability depending on the density of solutions, the number of guesses, and whether guesses are repeated. The probability of finding a solution from one guess can be as low as {p = 2^{-n}}, if there is just a single solution. Repeated guessing {t} times (with no checking for duplicate guesses) will then find a solution with probability {1 - (1-p)^t}. If we want this to be greater than {1/2}, then in the worst case of a single solution, {t} must be greater than {(-\log(1 - 2^{-n}))^{-1}}.

With no duplicate guesses (which is more difficult to ensure), the probability of finding no solution is

\displaystyle  1 - \prod_{i=0}^{t-1} ((1-p)2^n - i)/(2^n - i),

which for {t} small relative to {2^n} is still close to

\displaystyle  1 - \prod_{i=0}^{t-1} ((1-p)2^n)/(2^n) = 1 - (1-p)^t.

On the other hand, Paturi et al. showed this can be improved in some cases. Their approach is to first saturate the clause set by doing resolution to generate clauses up to some fixed size. Then they pick a random variable ordering and a random assignment, and assign the variables in order to satisfy unit clauses, or otherwise from the assignment. This is then repeated many times to boost probability of success. This is discussed in An Improved
Exponential-Time Algorithm for k-SAT
. (This appeared in 2005, based on a preliminary version at FOCS 1998!) When solutions are far apart, they say this “causes frequent occurrence of unit clauses in the process, thus the probability that a satisfying assignment is found is high”. This seems to indicate that immediate restarts might be a good policy in this setup.

At least at first glance, Schöning’s algorithm doesn’t try very hard to exploit structure; the Paturi et al. algorithm appears to dig a little deeper. Schöning in the abstract of his invited talk Comparing Two Stochastic Local Search Algorithms for Constraint Satisfaction Problems, to be presented at CSR 2010 in June, suggests that Moser’s algorithm presented at STOC 2009 might be worth looking at it in more detail, as another possible approach.

In contrast, SAT solvers try very hard to exploit structure, through clause learning.

Armin Biere’s talk on the history of SAT up to 2007 mentions how restarts have been getting more and more frequent (see page 31, slide 30/44).

In particular, as of 2007,

  • ZChaff restarted every 10000 conflicts,
  • MiniSAT restarted every 100 conflicts, and
  • PicoSAT restarted every 100 conflicts but could be more frequent.

In addition to the above heuristics based on SAT solving in practice, Schöning suggested in 2007 that restarts were important on theoretical grounds, in the paper Principles of Stochastic Local Search.

Question 1 Can an immediate-restart policy work for 3-SAT?

Or has this been done already?

(Edit 20100415: fixed link to paper by Paturi et al.)

Advertisements

Leave a Comment »

No comments yet.

RSS feed for comments on this post. TrackBack URI

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Create a free website or blog at WordPress.com.

%d bloggers like this: