Logic and Proof MT24, Walk-SAT


Flashcards

  • Input: CNF formula $\Phi$ (suppose we have $m$ clauses)
  • Output: Whether $\Phi$ is satisfiable

Describe the $\mathbf{WalkSAT}$ @algorithm, which is a randomised algorithm for solving this problem and analyse it when:

  • $\Phi$ is a 2CNF formula
  • $\Phi$ is a Horn formula
  • $\Phi$ is a 3CNF formula

Suppose there are $n$ variables in $\Phi$. Then run the following several times (we will shortly see how many times several is in order to get a good chance of outputting the correct answer)

  • Let $\mathsf v$ be a random truth assignment to the variables
  • Repeat $r$ times:
    • Otherwise, pick an unsatisfied clause $C$ and a variable $x$ in $C$ uniformly at random
    • Flip the value of $x$ in $\mathsf v$
    • If $\Phi$ is satisfied by $\mathsf v$, return the current assignment
  • Return “unsat”

Let $\mathsf v^\ast$ be some satisfying assignment.

Define the distance between two assignments to be the number of variables on which they differ. Let $T _ i$ be the maximum over all assignments $\mathsf v$ at distance $i$ from $\mathsf v^\ast$ of the number of expected variable-flipping steps to reach $\mathsf v^\ast$ from $\mathsf v$.

By definition $T _ 0 = 0$, and $T _ n = 1 + T _ {n-1}$.

In 2CNF:

In 2CNF, we have when we choose from two literals in a clause that is not satisfied by the current assignment, at least one of those literals must have a different value under $\mathsf v^\ast$ than $\mathsf v$. Thus

\[\begin{aligned} T_0 &= 0 \\\\ T_n &= 1 + T_{n-1} \\\\ T_i &\le 1 + (T_{i+1} + T_{i-1}) / 2 &&\text{for } 0 < i < n \end{aligned}\]

To obtain an upper bound on the $T _ i$, we consider the situation in which these bounds hold with equality

\[\begin{aligned} H_0 &= 0 \\\\ H_n &= 1 + H_{n-1} \\\\ H_i &= 1 + (H_{i+1} + H_{i-1}) / 2 &&\text{for } 0 < i < n \end{aligned}\]

so we have $T _ i \le H _ i$ for $i = 0, \ldots, n$.

Adding these equations together yields $H _ 1 = 2n - 1$. Then solving for $H _ 1$ in $H _ 2$ gives $H _ 2 = 4n - 4$. Continuing we see that $2in - i^2$. So the worst expected time to hit $\mathsf v$ is $H _ n = n^2$.

Hence set $r = 2mn^2$. Then the expected number of iterations from any starting point is at most $n^2$, and thus by Markov’s inequality in each of the $m$ phases of $2n^2$ iterations

\[\mathbb{P}[\text{takes more than }2n^2 \text{ iterations}] \le \frac{n^2}{2n^2} = \frac{1}{2}\]

and so the probability that an unsatisfying valuation is not found over all $m$ phases is at most $2^{-m}$.

In Horn formulas:

In a Horn formula, we have when we choose from the many literals in a clause that is not satisfied by the current assignment, we either move closer to the current assignment with probability $1/2$ or move further from it with probability $1/2$. This is because in an unsatisfied clause

\[(p_1 \land \cdots \land p_k) \to p_{k+1}\]

$\mathsf v$ must differ from $\mathsf v^\ast$ on at least $k$ of the variables, which is at least $1/2$ the variables in the clause.

Thus the analysis proceeds exactly as before.

In 3CNF formulas:

In a 3CNF formula, when we flip the value of a variable in a clause, we move closer to the satisfying assignment with probability $1/3$ and move further with probability $2/3$. Thus we have

\[\begin{aligned} H_0 &= 0 \\\\ H_n &= 1 + H_{n-1} \\\\ H_i &= 1 + \frac{H_{i-1} }{3} + \frac{2H_{i-1} }{3} &&\text{for } 0 < i < n \end{aligned}\]

Alternative proof that WalkSAT on 3CNF formulas runs in time $O(1.732^n)$:

Suppose there are $n$ variables in $\Phi$. Then run the following several times (we will shortly see how many times several is in order to get a good chance of outputting the correct answer)

  • Let $\sigma$ be a random truth assignment to the variables
  • For $t = 1, 2, \cdots, 3n$:
    • If $\Phi$ is satisfied by $\sigma$, exit the loop
    • Otherwise, pick an unsatisfied clause $c$ and a variable $x$ in $c$ uniformly at random
    • Flip the value of $x$ in $\sigma$
  • See if $\sigma$ satisfies the formula

If any output $\sigma$ satisfies the formula, output that $\Phi$ is satisfiable, otherwise output that $\Phi$ is satisfiable.

We want to estimate the probability that one run of this algorithm generates a satisfying assignment.

Suppose:

  • $\sigma^\star$ is an arbitrary satisfying assignment of $\Phi$
  • $\sigma$ is the current truth assignment maintained in this run
  • $d _ t$ is the number of variables where $\sigma$ and $\sigma^\star$ disagree on step $t$ in this run

Then:

  • With probability $\ge 1/3$, $d _ {t+1} = d _ t - 1$ (i.e. we move closer to $\sigma^\star$)
  • With probability $\le 2/3$, $d _ {t _ 1} = d _ t + 1$ (i.e. we move further from $\sigma^\star$)

Why is this true? Consider an unsatisfied clause $(\ell _ 1 \vee \ell _ 2 \vee \ell _ 3)$ in $\Phi$. This clause is satisfied under $\sigma^\star$, so at least one of the variables needs to be opposite to its current value. With probability $\ge 1/3$ we pick a correct variable to flip, and with probability $\le 2/3$, we flip the wrong one.

Initially $P(d _ 0 \le n/2) \ge 1/2$. Then if this run is lucky, it satisfies $\Phi$ in the first $n/2$ steps. Thus the probability that this run satisfies $\Phi$ is

\[\text{prob. starts with at least n/2 correct} \times \text{makes n/2 steps in right direction}\]

which is equal to $\frac{1}{2 \cdot 3^{n/2} }$.

We can use the standard “boosting” technique in order to improve the probability of success, by running the algorithm multiple times. If we want the probability that it outputs the correct answer to be $\ge 1 - 10^{-4}$, then running it $20 \cdot 3^{n/2} \approx 1.732^n$ times gives the result.

@sheets~




Related posts