Propositional Satisfiablity: the SAT Problem

Propositional Logic

propositional logic is one of the simplest useful logics

you should already know about this from programming, and discrete math

but lets quickly review it …

here is an example propositional logic sentence: P -> ~(Q & R)

• -> is the logical connective implication
• ~ is the logical connective negation
• & is the logical connective and
• v is the logical connective or (not shown in this expression)
• <-> is the logical connective equivalence (not shown in this expression)
• P, Q, and R are variables that can be either true or false (and no other possible values)
• we also will sometimes use special symbols True and False, indicating the constant values of true and false

a grammar for the syntax of propositional logic is given in Figure 7.7 (p. 244) of the text

the semantics of propositional logic is usually defined in English, or with truth tables, e.g.

S & T is true when S is true and T is true, and false otherwise

S T  S & T
----------
0 0    0             0 - false
0 1    0             1 - true
1 0    0
1 1    1

the special symbol True is always true, and the special symbol False is always false

we define an atomic sentence to be either the special symbols True or False, or a variable (e.g. P, Q, R, …)

an atomic sentence is a positive literal), and the negation of an atomic sentence is a negative literal; a literal is a positive literal or a negative literal

e.g. True, False, ~True, P, ~P, A, B, ~M are all literals

e.g. True, False, P, A, and B are all positive literals

e.g. ~True, ~P, ~M are all negative literals

given a propositional logic sentence like P -> ~(Q & R), we are usually interested in whether it is true or false

if we know the truth values of P, Q, and R, then we can use the definitions of the logical connectives to calculate the truth value of the sentence

e.g. suppose P=true, Q=true, and R=false; then P -> ~(Q & R) is true

• truth tables can be used to find all evaluations of a propositional sentence
• however, a sentence with \(n\) variables will have a truth table with \(2^n\) rows, which is an exponential number of rows and so this is not a practical technique for sentences with many variables

another question we might ask is if, given some propositional logic expression, there any assignment of truth-values to P, Q, and R that make it true …

The SAT Problem

… this is known as SAT, or the satisfiability problem, and it turns out to have many practical applications

• many problems can be cast as SAT problems, including CSPs (!)
• very efficient SAT solvers have been created and refined over the years

e.g. does P -> ~(Q & R) have a satisfying assignment? yes: from the definition of -> we know that “false -> anything” is true, and so setting P=false, and Q and R to any other values, is a satisfying assignment

when discussing the SAT problem, we will often talk about models

for propositional logic, a model of a sentence is a particular assignment of values to variables (of that sentence) that make it true

• an assignment of truth values to all variables in a sentence is called an interpretation, and so a model can be defined as a true interpretation

e.g. P=false, Q=true, and R=false is a model of P -> ~(Q & R), because the sentence evaluates to true with those assignments

e.g. P=true, Q=true, and R=false is also a model of P -> ~(Q & R)

e.g. P=true, Q=true, and R=true is not a model of P -> ~(Q & R) because the expression evaluate to false with those values

sometimes we use the notation M(s) to denote all models of a sentence s

• if M(s) contains all possible assignments of values to variables, then s is a tautology
• if M(s) is empty, then s is a contradiction

e.g. here is the truth table for P -> ~(Q & R):

P Q R   P -> ~(Q & R)
---------------------
0 0 0     1               0 - false
0 0 1     1               1 - true
0 1 0     1
0 1 1     1
1 0 0     1
1 0 1     1
1 1 0     1
1 1 1     0

this shows that P=true, Q=true, and R=true is the only assignment of values to variables that does not model P -> ~(Q & R)

so M(P -> ~(Q & R)) = { (0,0,0), (0,0,1), (0,1,0), (0,1,1), (1,0,0), (1,0,1), (1,1,0) }

the SAT problem thus asks for a given sentence s if M(s) is non-empty, and what is one element in it

Modelling with Propositional Logic

to see how we can use propositional logic and SAT to solve problems, lets model the n-queens problem in propositional logic

recall that the N-queens problem asks you to place N chess queens on an NxN so that no two queens are on the same row, column, or diagonal

The N=2 Queens Problem as a SAT Problem

we’ll start with n=2; this obviously has no solutions, but it’s a good warm-up

we’ll represent the n=2 problem with 4 logical variables, one for each square of the board:

A B
C D

the idea is that if a variable is true if there is a queen at that board location, and false if there is no queen

now we add constraints on these variables

x!=y to means sentences x and y have different values, i.e.:

x y   x!=y
----------
0 0    0       0 - false
0 1    1       1 - true
1 0    1
1 1    0

!= is known as exclusive-or, but here we’ll call it “not equal”

there are three groups of constraints for the n-queens problem: row constraints, column constraints, and diagonal constraints

row constraints: A!=B, C!=D

column constraints: A!=C, B!=D

diagonal constraints: A!=D, B!=C

we can join all these constraints together with & to make a single propositional logic expression:

A!=B & C!=D & A!=C & B!=D & A!=D & B!=C

if this expression is satisfiable, then that means there is a way to place 2 queens on the board that don’t attack each other

but we know this is impossible, so we know this expression is not satisfiable

we used != here for convenience, but in practice SAT solvers might not directly support the != (exclusive-or) connective

we can re-write the constraints using just &, v (or), and ~ (not)

row constraints:

(
     ( A & ~B)
   v (~A &  B)
)

(
     ( C & ~D)
   v (~C &  D)
)

column constraints:

(
     ( A & ~C)
   v (~A &  C)
)

(
     ( B & ~D)
   v (~B &  D)
)

diagonal constraints:

(
     ( A & ~D)
   v (~A &  D)
)

(
     ( B & ~C)
   v (~B &  C)
)

and-ing all of these together gives one big sentence:

   (
        ( A & ~B)
      v (~A &  B)
   )
&
   (
        ( C & ~D)
      v (~C &  D)
   )
&
   (
        ( A & ~C)
      v (~A &  C)
   )
&
   (
        ( B & ~D)
      v (~B &  D)
   )
&
   (
        ( A & ~D)
      v (~A &  D)
   )
&
   (
        ( B & ~C)
      v (~B &  C)
   )

some SAT solvers require that the sentence being solved be in conjunction normal form (CNF)

a sentence is in CNF if it consists of a series of literals or-ed together all joined by &, e.g. this sentence is in CNF:

  (P v ~Q v R)    // conjunctive normal form (CNF)
& (~P v ~Q v R)
& (P v Q v ~R)

all propositional logic sentences can be converted to CNF (see p.253-4 of the textbook)

unfortunately, the following constraint on B and C is not in CNF:

(
     ( B & ~C)
   v (~B &  C)
)

to convert it CNF, we can apply the distributivity rule (see p.249) twice to get this logically equivalent expression:

  ( B v  C)
& (~B v ~C)

you can use a truth-table to verify that these two expressions are, in fact, logically equivalent

so the entire 2-queens expression in CNF is this:

  ( A v  B)
& (~A v ~B)
& ( C v  D)
& (~C v ~D)
& ( A v  C)
& (~A v ~C)
& ( B v  D)
& (~B v ~D)
& ( A v  D)
& (~A v ~D)
& ( B v  C)
& (~B v ~C)

if we agree to put one clause (a clause is a disjunction of literals) per line, then we can get rid of the & operators and brackets:

 A v  B
~A v ~B
 C v  D
~C v ~D
 A v  C
~A v ~C
 B v  D
~B v ~D
 A v  D
~A v ~D
 B v  C
~B v ~C

there is also no need for the v either, so it can be further simplified to:

 A  B
~A ~B
 C  D
~C ~D
 A  C
~A ~C
 B  D
~B ~D
 A  D
~A ~D
 B  C
~B ~C

for SAT solvers, another simplification is usually made: for the variables, numbers are used instead of letters, and negation is represented by a - (minus sign)

so if we let A=1, B=2, C=3, and D=4, our expression becomes:

 1  2
-1 -2
 3  4
-3 -4
 1  3
-1 -3
 2  4
-2 -4
 1  4
-1 -4
 2  3
-2 -3

we’re almost done! standard SAT solver input requires a bit more:

• the first line should indicate the number of variables and number of clauses (a clause is a disjunction of literals), in this format:

  p cnf <num_vbles> <num_clauses>
  

• every clause must end with a 0

• a line that beings with a c is a comment that is ignored by the solver

so here is the final input:

 c N=2 queens problem
 p cnf 4 12
 1  2 0
-1 -2 0
 3  4 0
-3 -4 0
 1  3 0
-1 -3 0
 2  4 0
-2 -4 0
 1  4 0
-1 -4 0
 2  3 0
-2 -3 0

to solve this with minisat, we put the above input into a file named queens2.txt, and then run this command:

$ minisat queens2.txt out
... lots of info about the solution ...

UNSATISFIABLE

$ cat out
UNSAT

which variables are true/false are written to the output file (named out here); if, as in this example, there are no satisfying assignments, then UNSAT is written

The N=3 Queens Problem as a SAT Problem

now lets try the N=3 queens problem; we will use these 9 variables:

A B C
D E F
G H I

through a bit of trial and error, it’s not hard to see that this cannot be solved either

again, there are row constraints, column constraints, and diagonal constraints

lets list all the constraints

consider the first row: A B C

exactly one of these must be true, and the others false; we can write that constraint like this:

   ( A & ~B & ~C)   // first row
v  (~A &  B & ~C)
v  (~A & ~B &  C)

but this is not in CNF; so lets think about how to make this constraint CNF

exactly one of A, B, or C must be true, so this constraint holds:

A v B v C

suppose that A is true; that means B is false and C is false; symbolically, this means A->~B and A->~C, and those can be re-written as the logically equivalent sentences ~A v ~B and ~A v ~C

we can do the same thing for B and C, and so we get these constraints in CNF:

A v B v C
~A v ~B
~A v ~C
~B v ~A   // repeat!
~B v ~C
~C v ~A   // repeat!
~C v ~B   // repeat!

removing the repeated clauses gives:

A v B v C  // first row
~A v ~B
~A v ~C
~B v ~C

intuitively, this says that at least one of A, B, or C is true, and also if you pick any pair of variables, at least one of the variables in the pair will be false

• this amounts to saying exactly one of A, B, or C is true

we do the same thing for the next two rows:

D v E v F  // second row
~D v ~E
~D v ~F
~E v ~F

G v H v I  // third row
~G v ~H
~G v ~I
~H v ~I

the column constraints have the same format — be careful to get all the variables names correct!

A v D v G  // column 1
~A v ~D
~A v ~G
~D v ~G

B v E v H  // column 2
~B v ~E
~B v ~H
~E v ~H

C v F v I  // column 3
~C v ~F
~C v ~I
~F v ~I

for the diagonal constraints, there are two main diagonals (AEI and CEG), and 4 short diagonals (BF, FH, HD, DB)

the constraint on the diagonals is different than the constraint on the rows and columns: at most one queen can appear on any diagonal (i.e. it’s okay for a diagonal to have no queens, something that can’t happen with rows and columns)

so for the diagonal constraints, we will not have the “or” of all the variables involved, just the following 2-variable constraints:

~A v ~E  // AEI
~A v ~I
~E v ~I

~C v ~E  // CEG
~C v ~G
~E v ~G

~B v ~F  // BF

~F v ~H  // FH

~H v ~D  // HD

~D v ~B  // DB

now, as we did for the N=2 case, we join together all these constraints using & to get one (big!) CNF sentence that is true just when 3 non-attacking queens on a 3x3 board

since we know that puzzle is not solvable, we know that this sentence has no satisfying assignment

here is the input formatted for minisat:

c 3-queens problem
p cnf 9 34
1 2 3 0
-1 -2 0
-1 -3 0
-2 -3 0
4 5 6 0
-4 -5 0
-4 -6 0
-5 -6 0
7 8 9 0
-7 -8 0
-7 -9 0
-8 -9 0
1 4 7 0
-1 -4 0
-1 -7 0
-4 -7 0
2 5 8 0
-2 -5 0
-2 -8 0
-5 -8 0
3 6 9 0
-3 -6 0
-3 -9 0
-6 -9 0
-1 -5 0
-1 -9 0
-5 -9 0
-3 -5 0
-3 -7 0
-5 -7 0
-2 -6 0
-6 -8 0
-8 -4 0
-4 -2 0

The N=4 Queens Problem as a SAT Problem

for the N=4 queens problem, the constraints are similar to the ones for N=3, but there are more of them and they are a little bigger

there are 16 variables:

A B C D
E F G H
I J K L
M N O P

to help with this, we’ll use the notation exactly_one(W,X,Y,Z) to indicate a CNF expression that allows exactly one of W, X, Y, or Z to be true

and at_most_one(W,X,Y,Z) to indicate a CNF expression that allows at most one of W, X, Y, or Z to be true

row constraints:

exactly_one(A,B,C,D)

exactly_one(E,F,G,H)

exactly_one(I,J,K,L)

exactly_one(M,N,O,P)

column constraints:

exactly_one(A,E,I,M)

exactly_one(B,F,J,N)

exactly_one(C,G,K,O)

exactly_one(D,H,L,P)

for the diagonal constraints, notice that the diagonals go in two different directions, range in size from 2 to 4, and at most one queen can appear on any diagonal:

at_most_one(C,H)

at_most_one(B,G,L)

at_most_one(A,F,K,P)

at_most_one(E,J,O)

at_most_one(I,N)

here is a CNF version of the constraints that can be input into minisat:

c 4-queens problem (sat)
p cnf 16 84
-1 -2 0
-1 -3 0
-1 -4 0
-2 -3 0
-2 -4 0
-3 -4 0
1 2 3 4 0
-5 -6 0
-5 -7 0
-5 -8 0
-6 -7 0
-6 -8 0
-7 -8 0
5 6 7 8 0
-9 -10 0
-9 -11 0
-9 -12 0
-10 -11 0
-10 -12 0
-11 -12 0
9 10 11 12 0
-13 -14 0
-13 -15 0
-13 -16 0
-14 -15 0
-14 -16 0
-15 -16 0
13 14 15 16 0
-1 -5 0
-1 -9 0
-1 -13 0
-5 -9 0
-5 -13 0
-9 -13 0
1 5 9 13 0
-2 -6 0
-2 -10 0
-2 -14 0
-6 -10 0
-6 -14 0
-10 -14 0
2 6 10 14 0
-3 -7 0
-3 -11 0
-3 -15 0
-7 -11 0
-7 -15 0
-11 -15 0
3 7 11 15 0
-4 -8 0
-4 -12 0
-4 -16 0
-8 -12 0
-8 -16 0
-12 -16 0
4 8 12 16 0
-3 -8 0
-2 -7 0
-2 -12 0
-7 -12 0
-1 -6 0
-1 -11 0
-1 -16 0
-6 -11 0
-6 -16 0
-11 -16 0
-5 -10 0
-5 -15 0
-10 -15 0
-9 -14 0
-2 -5 0
-3 -6 0
-3 -9 0
-6 -9 0
-4 -7 0
-4 -10 0
-4 -13 0
-7 -10 0
-7 -13 0
-10 -13 0
-8 -11 0
-8 -14 0
-11 -14 0
-12 -15 0

the 4-queens problem has solutions, and so this sentence is satisfiable, e.g. minisat returned this model:

-1 -2 3 -4 5 -6 -7 -8 -9 -10 -11 12 -13 14 -15 -16

a negative number means the variable is assigned false, and a positive number mean it’s assigned true

this model corresponds to this placement of queens:

. . Q .
Q . . .
. . . Q
. Q . .

N-queens in General

the previous examples of the N queens problem shows the general pattern you can follow to create a CNF expression that, when satisfied, is a solution to the N-queens problem

CSPs to SAT: One way of Encoding a CSP as a SAT Problem

any binary CSP (constraint satisfaction problem) can be converted into a SAT problem, and in some cases this can be a good way to solve the CSP

recall that a binary CSP consists of:

• \(n\) variables, \(X_1, \ldots , X_n\); a variable can be assigned or unassigned
• \(n\) domains, \(D_1, \ldots , D_n\), where variable \(X_i\) can only be assigned values from domain \(D_i\)
• a set of constraints on pair of variables, where a constraint specifies what values the two variables can be assigned at the same time

one way of converting this CSP into a SAT problem is as follows:

• use one true/false SAT variable for each of the domain values; this will result in \(|D_1| + |D_2| + \ldots + |D_n|\) SAT variables
• for each variable \(X_i\) in the CSP, add an “exactly one” constraint on the corresponding SAT variables for its domain values; this ensures that a solution to the SAT problem will assign exactly one value to the corresponding CSP variable
• convert the CSP constraint to constraints on the SAT variables; see the example below for how this can be done with good lists

for example, suppose you have a CSP with just two variables, \(X_1\) and \(X_2\), and they both have domains \({1,2,3}\)

the SAT variables are assigned to CSP values like this:

X_1    X_2
-----------
a  1   d  1
b  2   e  2
c  3   f  3

so, for example, if the SAT variable \(a\) is true and \(f\) is true (and all others are false), then \(X_1\) has the value 1 and \(X_2\) has the value 3

a CSP variable can only be assigned one value, so add the constraints exactly_one(a,b,c) and exactly_one(d,e,f)

now assume the constraint between \(X_1\) and \(X_2\) is specified by this good list:

X_1  X_2
--------     values that X_1 and X_2 can be assigned
1    2       at the same time
1    3
2    2
2    3

to convert this to a SAT constraint, we describe, in SAT, exactly what pairs of values are allowed at the same time

for example, \(X_1=1\) and \(X_2=2\) is permitted, and so for the corresponding SAT variables the sentence \(a \land e\) must be true

another permitted possibility is that \(X_1=1\) and \(X_2=3\), which means the sentence \(b \land f\) could be true as well

if these two possibilities are or-ed together we get the sentence \((a \land e) \lor (b \land f)\), which corresponds to \(X_1=1\) and \(X_2=2\) or \(X_1=1\) and \(X_2=3\)

if we do the same thing for all the pairs of values on the good list, we get this sentence

\[(a \land e) \lor (a \land f) \lor (b \land e) \lor (b \land f)\]

of course, this is not in CNF, so you need to convert this to CNF using rules of logic

also, this sentence allows for two, or more, different assignments to be true at the same time, which is not allowed for CSP solutions; however, the exactly-one constraints on the domain values above prevent this

in general, note that the size of the CSP search space is \(|D_1| \cdot |D_2| \cdot \ldots \cdot |D_n|\), and that the size of the corresponding SAT problem is \(2^{|D_1| + |D_2| + \ldots + |D_n|}\)

• for example, consider a 3-coloring problem with 10 variables each with a domain of size 3; the CSP search space has size \(3^{10}\), while the corresponding SAT search space is size \(2^{30}\)
  • \(3^{10} = 59049\)
  • \(2^{30} = 1 073 741 824\) (over 1 billion)
  • the SAT search space is 18,000 times bigger than the CSP search space!

this means the search space of the SAT problem is always bigger than search space of the CSP, which suggests that this is not a great encoding, i.e. it converts a CSP into a SAT problem with a bigger search space

for some problems, however, this may not be a problem seem since modern SAT solvers are extremely efficient, and they can solve some large SAT problems quite quickly

however, in general, this particular encoding of a CSP into SAT is not always the best, and there are other encodings that result in smaller search spaces

SAT Solvers

SAT solvers are a kind of CSP solver tuned specifically for solving SAT problems

they are efficient enough to actually be useful in some practical applications, and can sometimes efficiently solve problems with 1000s of variables and clauses

there are two main categories of SAT solvers:

• backtracking solvers (like minisat)
  • can be used to prove that a sentence is unsatisfiable
• local search solvers (like Walksat)
  • can’t be used to prove (with 100% certainty, at least) that a sentence is unsatisfiable

modern backtracking SAT solvers combine efficient data structures and SAT-specific heuristics to efficiently solve many large SAT problems

• they are often a practical choice for solving CSP-like problems, or problems that require backtracking
• the tricky part is usually coming up with an efficient CNF-encoding of all the constraints, and, as with the N-queen problem, this may involve writing a program to help generate the clauses

SAT: DPLL Algorithm

the DPLL algorithm (Davis, Putnam, Logemann, and Loveland); from early 1960s

the input to DPLL is a CNF (conjunctive normal form) sentence

• recall that a CNF sentence is a series of clauses and-ed together
• a clause is one, or more, literals or-ed together
• a literal is a variable, or the negation of a variable
• any propositional sentence can be converted to CNF

DPLL is essentially a depth-first backtracking algorithm, with a few improvements:

• early termination

  sometimes you don’t need to assign all variables to determine if a sentence is satisfied, e.g. (A | B) & (A | C) is true if A is true, no matter the values of B and C

  • so once A is assigned true in the backtracking search, we can see that the sentence is satisfied, and can stop immediately and return SAT

  similarly, if any clause is false, then the entire CNF sentence must be false (because the clauses are and-ed together), and backtracking can occur; this might happen after only a few variables have been assigned, e.g. (A | !B) & (C | !D) must be false if A=false and B=true — no need to check C and D

• pure symbol heuristic

  a “symbol” is pure if it occurs with the same “sign” in all clauses where it occurs, i.e. it always occurs negated, or always occurs un-negated

  e.g. (A | !B) & (!B | !C) & (C | A)

  • A is pure because it appears with the same sign in all its clauses
  • B is pure because it appears with the same sign in all its clauses
  • C is not pure because it appears with different signs, C in the 3rd clause, !C in the 2nd

  all pure symbols can be assigned a value that makes them true, since doing so can never make a clause false

  e.g. (A | !B) & (!B | !C) & (C | A)

  • A is pure, so setting A=True will never make the clauses it appears in false
  • B is also pure, so setting B=False will never make the clauses it appears in false
  • A=True, B=True, C=True (or C=False) is a satisfying assignment

  note that a symbol could become pure based on partial assignments, i.e. assigning values to some variables may make some clauses true, and true clauses can be ignored when determining a variable purity

• unit clause heuristic

  a unit clause is a clause with one literal, i.e. a clause that is just a variable, or the negation of a variable

  in the context of DPLL, a unit clause can also occur when all literals but one in a clause have a known value, e.g. if A=false and B=true in the current search, then (A | !B | !C) becomes a unit clause

  since a unit clause has only one literal and that must evaluate to true, we can immediately assign it the value that makes it true

  after assigning a unit clause the required value, other clauses may simplify to unit clauses, sometimes resulting in a cascade of assignments

  e.g. consider the sentence (A | !B) & (A | B | !C) & (B | C)

  • for the sake of this example, suppose we initially set A=False (and we ignore the fact that A is pure!)
  • the first clause is now a unit clause, and that means !B must be true, so B=False
  • the third clause is now a unit clause, so !C=True, meaning C=False
  • since B and C are both False, the clause (B | C) cannot be satisfied, so the entire expression is unsatisfiable if we start with A=false
  • suppose we re-start and set A=true initially, then the first two clauses are satisfied, meaning the expression reduces to (B | C); this is satisfiable if we set B, or C, or both, to true

  e.g. consider the sentence (A | !B) & (!A | B | C) & (B | !C)

  • suppose we set A=False
  • this forces !B=True, i.e. B=False
  • since !A=True, (!A | B | C) is true
  • since B=False, (B | !C) is a unit clause, so !C=True, i.e. C=False
  • therefore A=False, B=False, C=False is a satisfying assignment

the above heuristics have been part of the DPLL algorithm since its invention

modern SAT solvers based on DPLL typically implement many other clever tricks and heuristics that make them even faster, tricks such as:

• component analysis: SAT solvers may be able to recognize disjoint subsets of clauses and solve them independently
• Variable and value ordering: as with general CSPs, heuristics for choosing the next variable to assign and the value to assign it can be quite effective; e.g. the degree heuristic says you should choose the next variable to assign to be the one that appears in the most clauses
• Intelligent backtracking: SAT solvers can use clause learning to keep track of conflicts, i.e. they add new clauses to the sentence to avoid going down parts of the search tree that are known to be unfruitful
  • experiments show that this is probably the one single trick with the greatest performance impact in SAT solving
• Random restarts: if it seems progress is not being made, a solver can re-start the search, making difference random choices and preserving any learned conflicts
• Clever indexing: SAT solvers can use efficient customized data structures to quickly find things like all clauses in which a variable appears as a positive literal, or to determine in which clauses unit propagation will occur (2-watched literals)

overall, these sorts of improvements to the basic DPLL have resulted in extremely efficient SAT solvers that are good enough to solve some practical problems involving tens of thousands of variable and clauses

• both the theory of SAT and the practice of implementing efficient SAT solvers is still a well-studied area of computer science, with dozens of research papers being published every year

SAT: Walksat

just as some CSPs can be efficiently solved by local search (e.g using min-conflicts), the local search algorithm named Walksat can find satisfying assignments for some sentences even more quickly than DPLL solvers

• keep in mind that, like min-conflicts for CSPs, Walksat is a randomized algorithm and so cannot prove that a sentence is unsatisfiable
  • if Walksat can’t satisfy a sentence, then you might take that as good evidence that the sentence can’t be satisfied — but it’s not a proof that no satisfying assignment exists!

in Walksat, all variables in the sentence have a value (you could start with a random initial assignment)

then Walksat repeatedly does the following until the sentence is satisfied, or some max number of “flips” is reached:

• it chooses an unsatisfied clause at random
• it then “flips” the value of one of the variables in the clause by randomly choosing (with some probability \(p\)) one of the following:
  • pick a variable to flip at random
  • or, flip the variable that maximizes the number of satisfied clauses overall

this is a much simpler algorithm than DPLL!

it is perhaps surprising that it can work so well

it has undergone extensive testing, and it can efficiently satisfy many large sentences

• but keep in mind, Walksat can never prove unsatisfiability!