Chapter XI 3-Satisfiability

WalkSAT in Clojure

A randomized local-search algorithm that solves random 3-SAT instances faster than complete solvers — and reads as one beautiful pipeline.

Represent literals as integers — positive for the variable, negative for its negation. A clause is a vector of literals; a formula is a vector of clauses. Persistent data structures throughout.

;; (x1 ∨ ¬x2 ∨ x3) ∧ (¬x1 ∨ x2 ∨ x3)
(def formula [[1 -2 3] [-1 2 3]])

(defn sat-lit? [lit assignment]
  (let [v (Math/abs (long lit))]
    (if (pos? lit) (assignment v) (not (assignment v)))))

(defn sat-clause? [clause assignment]
  (some #(sat-lit? % assignment) clause))

WalkSAT's core: pick a random unsatisfied clause, then in that clause flip either a random variable (with probability p, to escape local minima) or the variable that maximizes the new count of satisfied clauses.

(defn random-unsat-clause [formula assignment]
  (rand-nth (filterv #(not (sat-clause? % assignment)) formula)))

(defn flip-var [assignment v]
  (update assignment v not))

(defn best-flip-in-clause [clause formula assignment]
  (apply max-key
         #(count (filter (fn [c] (sat-clause? c (flip-var assignment %))) formula))
         (map #(Math/abs (long %)) clause)))

Loop: while unsatisfied clauses exist and we haven't hit max-flips, flip a variable. Clojure's loop/recur gives bounded recursion without stack growth.

(defn walksat [formula n-vars max-flips p]
  (loop [assignment (zipmap (range 1 (inc n-vars))
                            (repeatedly #(< (rand) 0.5)))
         flips 0]
    (cond
      (every? #(sat-clause? % assignment) formula) assignment
      (>= flips max-flips) nil
      :else
        (let [c (random-unsat-clause formula assignment)
              v (if (< (rand) p)
                  (Math/abs (long (rand-nth c)))
                  (best-flip-in-clause c formula assignment))]
          (recur (flip-var assignment v) (inc flips))))))

04

Run it. WalkSAT often beats DPLL on random 3-SAT near the satisfiability threshold (clause-to-variable ratio ≈ 4.267). It is incomplete — it can't prove UNSAT — but for SAT instances it is very fast.
```
user=> (walksat formula 3 1000 0.5)
{1 true, 2 true, 3 true}
```

Grammar — Clojure

Clojure is a Lisp on the JVM. Code is data: every program is built from nested forms, each a list, vector, map, or symbol. The reading style takes one afternoon; the immutability discipline pays off forever.

(f a b): function call: f applied to a and b. Function comes first, parens wrap the whole call.
(defn name [args] body): define a function named `name` taking the listed args.
[a b c]: a vector literal. Indexed, fast random access.
{:k1 v1 :k2 v2}: a map literal. Keys can be any value; keywords (starting with :) are idiomatic.
#{1 2 3}: a set literal — like a map without values.
(let [a 1 b 2] body): local bindings. Pairs of name/value in the bracket vector.
(if cond then else): conditional expression. There is no statement-vs-expression distinction; everything returns a value.
(loop [x init] (recur ...)): bounded recursion that doesn't blow the stack. recur jumps back to the loop with new bindings.
#(... %1 %2): anonymous-function shorthand. `%1` is the first arg, `%` works for single-arg.

Represent a CNF formula as a vector of clauses, where each clause is a vector of literals. Positive integers are positive literals, negatives are negations.

;; (x1 ∨ ¬x2 ∨ x3) ∧ (¬x1 ∨ x2)
(def formula [[1 -2 3] [-1 2]])

;; "is this clause satisfied under assignment?"
(defn sat-clause? [clause assignment]
  (some #(let [v (Math/abs (long %))]
           (if (pos? %)
             (assignment v)
             (not (assignment v))))
        clause))

(sat-clause? [1 -2 3] {1 false, 2 false, 3 false})
;; -> true (literal -2 is satisfied since variable 2 is false)

Try Clojure in your browser →