Boolean satisfiability

Logical methods for AI

Boolean satisfiability

Lecture 5

What you’ll be able to do

Read chapter 5 first; exercise sheet 5 comes after the lecture.

Automating the hard work

In chapter 4 we did it all by hand: list the models, calculate the values, hunt for a countermodel.

Let the machine do it.
SAT asks one question: can one valuation make all of these true?
Two reasoning problems reduce to it.

Reduce the problem to SAT, then run an algorithm on it.

Satisfiability

$SUN \land \negRAIN$ , with $v(SUN) = 1$ , $v(RAIN) = 0$ :

1 AND (NOT 0) = 1

Satisfiable: one valuation settles it.

$SUN \land \negSUN$ :

1 AND (NOT 1) = 0 0 AND (NOT 0) = 0

Unsatisfiable: every valuation must fail.

The SAT problem

$SUN \lor RAIN$ , $\negSUN$ : satisfiable, by $v(SUN) = 0$ , $v(RAIN) = 1$ .
Add $\negRAIN$ : unsatisfiable — though each can be satisfied on its own.

Reduction 1: circuit verification

What the circuit does:

C = \neg(INPUT₁ \land INPUT₂)

What it should do, excluding the row with output $0$ :

S = \negINPUT₁ \lor \negINPUT₂

Where do they disagree? SAT? $\neg(S \leftrightarrow C)$

Satisfiable: that valuation is an input where the circuit is wrong.
Unsatisfiable: the circuit implements the specification.

Reduction 2: deductive validity

$(SUN \lor RAIN) \land \negSUN \land \negRAIN$ : no countermodel, so valid.

$(SUN \lor RAIN) \land SUN \land \neg\negRAIN$ : $v(SUN) = v(RAIN) = 1$ is a countermodel, so invalid.

Truth-tables: brute force

$n$ variables: $2ⁿ$ assignments.
Count from $0$ in binary to list them all.
Evaluate the formula in each row.
No preparation: the formula goes in as it stands.

Evaluating a row

python

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


def evaluate(tree, v):
    if is_variable(tree):
        return v(variable(tree))

    if operator(tree) == "¬":
        return NOT(evaluate(child(tree), v))

    left_value = evaluate(left_child(tree), v)
    right_value = evaluate(right_child(tree), v)
    if operator(tree) == "∧":
        return AND(left_value, right_value)
    if operator(tree) == "∨":
        return OR(left_value, right_value)
    return XNOR(left_value, right_value)

Every call gets a smaller tree, so evaluation terminates.

Searching the table

Ex.

The interactive example is loading.

A decision procedure

Finitely many rows, so the search finishes.
A returned valuation makes the formula true.
“Unsatisfiable” means every valuation was checked.

So SAT is decidable. The finished table also shows a tautology (glossary, opens in a new tab) (all $1$ s) or a contradiction (glossary, opens in a new tab) (all $0$ s).

The cost of brute force

For $n$ variables and $m$ operators, worst-case time complexity (glossary, opens in a new tab) :

O(2ⁿ(m + 1))

Variables	Rows
$3$	$8$
$10$	$1 024$
$20$	$1 048 576$
$40$	over a trillion

Combinatorial explosion (glossary, opens in a new tab) : one more variable doubles the work.

Normal forms

A literal (glossary, opens in a new tab) is a propositional variable or the negation of a propositional variable.

Formula	DNF?	CNF?
$SUN \lor \negRAIN$	yes	yes
$SUN \land \negRAIN$	yes	yes
$SUN \lor (RAIN \land WIND)$	yes	no
$(SUN \lor RAIN) \land WIND$	no	yes
$\neg(SUN \land RAIN)$	no	no

A DNF lists alternatives; a CNF lists requirements. Resolution needs CNF.

Rewriting into normal form

Each rule replaces a subformula by an equivalent one. First remove every $\leftrightarrow$ :

(A \leftrightarrow B) ⟹ ((\negA \lor B) \land (\negB \lor A))

Push negations inward:

r₁: \neg\negA ⟹ A r₂: \neg(A \land B) ⟹ \negA \lor \negB r₃: \neg(A \lor B) ⟹ \negA \land \negB

The result is in negation normal form (glossary, opens in a new tab) .

For CNF, distribute $\lor$ over $\land$ :

r₄: A \lor (B \land C) ⟹ (A \lor B) \land (A \lor C) r₅: (A \land B) \lor C ⟹ (A \lor C) \land (B \lor C)

For DNF, distribute $\land$ over $\lor$ :

r₆: A \land (B \lor C) ⟹ (A \land B) \lor (A \land C) r₇: (A \lor B) \land C ⟹ (A \land C) \lor (B \land C)

The rewriting algorithm

Remove $\leftrightarrow$ , push negations inward, then distribute — one rule at a time.

Ex.

The interactive example is loading.

Preprocessing is the expensive part

Distribution copies subformulas: a compact input can produce exponentially many clauses.

(SUN \land WARM) \lor (RAIN \land WIND)

becomes

(SUN \lor RAIN) \land (SUN \lor WIND) \land (WARM \lor RAIN) \land (WARM \lor WIND)

Each further pair doubles the clauses: $n$ pairs give $2ⁿ$ .

Truth-tables pay at search time; resolution pays before the search starts.

The resolution rule

Remove only one complementary pair at a time.

The empty clause (glossary, opens in a new tab) $⊥$ is false under every valuation.

Refutation search

Ex.

The interactive example is loading.

Tseytin: cheap preprocessing

Give each subformula a fresh name and constrain its value, instead of copying it. Name $SUN \land RAIN$ by a fresh $u$ :

(\negu \lor SUN) \land (\negu \lor RAIN) \land (u \lor \negSUN \lor \negRAIN)

One fresh variable and a few clauses per connective: the CNF grows linearly.

Worked-out example: the NAND circuit

Ex.

The interactive example is loading.