Las Vegas algorithm to satisfy most clauses in SAT

Question

Consider an instance of SAT with $m$ clauses, where every clause has exactly $k$ literals. Give a Las Vegas algorithm (i.e., an algorithm that always gives the correct result) that finds an assignment satisfying at least $m(1-2^{-k})$ clauses, and analyze its expected running time.

A possible Las Vegas algorithm is to randomly assign true/false to every variable, each with probability $1/2$. If the assignment satisfies less than $m(1-2^{-k})$ clauses, rerandomize all variables. Keep doing this until we get an assignment satisfying at least $m(1-2^{-k})$ clauses.

This is a valid Las Vegas algorithm, but I'm not sure it's one that would be expected by the question. Also, to analyze the expected running time, we would need to compute the probability that a random assignment works. This means the random assignment satisfies at least $m(1-2^{-k})$ clauses, and it doesn't seem easy to compute. What would be a better Las Vegas algorithm?

Answer 1

A random assignment has probability $1 - 2^{-k}$ of satisfying an "or" clause with $k$ literals, because it is only false if all $k$ literals are false. Thus the expected number of clauses satisfied is $m (1 - 2^{-k})$. For typical problems one might hope that the probability of at least $m (1-2^{-k})$ clauses being satisfied is about $1/2$, but this will not always be the case.

For example, consider $m = 2^k - 1$ clauses, consisting of all but one of the $2^k$ possible clauses with $k$ literals formed from $k$ distinct variables and their negations. The probability of satisfying at least $m (1-2^{-k})$ clauses is only $2^{-k}$ (with probability $1 - 2^{-k}$ you will satisfy $m-1$ of the clauses, but $m - 1 < m (1 - 2^{-k})$). In this example, the expected number of iterations of your algorithm is $2^k$. Moreover, no algorithm that looks only at the number of clauses satisfied by assignments can do better than that (because this number will always be either $m-1$ or $m$, and is only $m$ for the one correct assignment).

EDIT: It may be true that the probability of success in an iteration is at least $1/2^k$, but I haven't been able to prove it. The best I can do with a simple argument is this. Suppose $r$ is the least number of unsatisfied clauses that makes the number satisfied less than $m (1 - 2^{-k})$, i.e. $r = \lfloor 1 + m/2^k \rfloor$, and $b = 2^k r - m$, so that $1 \le b \le 2^k$. In the previous example $r=1$ and $b = 1$. The expected number of unsatisfied clauses is $m/2^k$. If $P$ is the probability of success in an iteration, i.e. having at most $r-1$ unsatisfied clauses, we have $m/2^k \ge r (1-P)$, which makes $$P \ge 1 - \dfrac{m}{2^{k} r} = \dfrac{b}{2^k r} \ge \dfrac{1}{2^k r}$$

Answer 2

Here's the naïve, derandomized algorithm:

First, we can convert between variable assignments and binary numbers: We use the number 1 to designate a true variable assignment, and 0 to designate false. n We now have the means of mapping a binary number to a variable assignment. Then, adopting the convention that $x_i$ means the $i$th variable, the number $000...000$ in binary corresponds to $x_1 = $ false, $x_2 = $ false, ... $x_n = $ false. The number $000...001$ corresponds to $x_1 = $ true, $x_2 = $ false, ... $x_n = $ false. $3=000...010$ corresponds to $x_1 = $ false, $x_2 = $ true, ... $x_n = $ false. And so on...

Now set $c$, our maximum count of satisfied clauses, to $0$. We will cycle through each binary number. In the loop, we simply calculate the formula that the binary number maps to, and count the number of satisfied clauses. If this is greater than the current $c$ value, our current maximum satisfied clauses, update $c$ and remember the binary number (we could call it $b$).

Then, when the loop completes, we will have the count of the maximum satisfied clauses, along with the actual variable assignments, which are stored in $b$. This algorithm requires practically no space, except to store the formula and $b$ and $c$. Its runtime is of course $2^n$, and it will find the maximum amount of satisfied clauses possible.