∀I

Logical methods for AI

Lecture 5

Boolean satisfiability

This work is licensed under CC BY 4.0

https://forms.gle/JiXXM9eysAZaJMja9

Boolean satisfiability

Ideas

Problem: Find a valuation that makes a given (set of) formula(s) true.
Satisfiability: $\Gamma$ is satisfiable $\Leftrightarrow$ there's a $\nu$ with $\nu(A)=1$ for all $A\in\Gamma$

Validity and SAT

$$P_1,P_2,\dots\vDash C\Leftrightarrow \Set{P_1,P_2,\dots, \neg C}\text{ is \emph{un}satisfiable}$$

$$\mathsf{RAIN}\lor \mathsf{BIKE},\neg\mathsf{RAIN}\vDash\mathsf{BIKE}$$ $$SAT(\Set{\mathsf{RAIN}\lor \mathsf{BIKE},\neg\mathsf{RAIN},\neg \mathsf{BIKE}})?$$

Truth-tables

$$SAT(\Set{\mathsf{RAIN}\lor \mathsf{BIKE},\neg\mathsf{RAIN},\neg \mathsf{BIKE}})?$$

Go through all valuations:

$\nu_1(\mathsf{RAIN})=1$ and $\nu_1(\mathsf{BIKE})=1$
$\nu_2(\mathsf{RAIN})=1$ and $\nu_2(\mathsf{BIKE})=0$
$\nu_3(\mathsf{RAIN})=0$ and $\nu_3(\mathsf{BIKE})=1$
$\nu_4(\mathsf{RAIN})=0$ and $\nu_4(\mathsf{BIKE})=0$

Combinatorial explosion

#variables	#rows
1	2
2	4
3	8
4	16
5	32
6	64

Conjunctive Normal Form (CNF)

Idea

Normal form: "canonical" way to write formula
CNF: conjunction of disjunction of literals$\dagger$
$\dagger$: $p,\neg p$

Examples

$\mathsf{RAIN}$
$\mathsf{RAIN}\land\neg\mathsf{BIKE}$
$\mathsf{RAIN}\lor\neg\mathsf{BIKE}$
$(\mathsf{RAIN}\lor\neg\mathsf{BIKE})\land (\mathsf{SUN}\lor\mathsf{BIKE})$

Counter-examples

$\neg\neg\mathsf{RAIN}$
$\mathsf{RAIN}\lor \neg(\mathsf{SUN}\land \neg \mathsf{BIKE})$
$\neg(\mathsf{RAIN}\land\neg\mathsf{BIKE})$
$\neg(\mathsf{RAIN}\lor\neg\mathsf{BIKE})$
$(\mathsf{RAIN}\land\neg\mathsf{BIKE})\lor\mathsf{SUN}$

Rewriting

$\neg\neg A\leadsto A$
$\neg (A\lor B)\leadsto \neg A\land \neg B$
$\neg (A\land B)\leadsto \neg A\lor \neg B$
$A\lor(B\land C)\leadsto (A\lor B)\land (A\lor C)$
$(A\land B)\lor C\leadsto (A\lor C)\land (B\lor C)$

$$\mathsf{RAIN}\lor \neg(\mathsf{SUN}\lor \neg \mathsf{BIKE})$$ $$\leadsto\mathsf{RAIN}\lor (\neg\mathsf{SUN}\land \neg\neg \mathsf{BIKE})$$ $$\leadsto(\mathsf{RAIN}\lor \neg\mathsf{SUN})\land (\mathsf{RAIN}\lor \neg\neg \mathsf{BIKE})$$ $$\leadsto(\mathsf{RAIN}\lor \neg\mathsf{SUN})\land (\mathsf{RAIN}\lor \mathsf{BIKE})$$

CNF Theorem

Theorem. For each formula $A$, there exists a formula $A_{CNF}$ in CNF, such that for all $\nu$, $$\nu(A)=\nu(A_{CNF})$$

Davis-Putnam-Logemann-Loveland algorithm

Ideas

"Smart" shortcuts
CNF as a set $$(\mathsf{RAIN}\lor \neg\mathsf{SUN})\land (\mathsf{RAIN}\lor \mathsf{BIKE})$$ $$\leadsto$$ $$\Set{\Set{\mathsf{RAIN},\neg\mathsf{SUN}},\Set{\mathsf{RAIN},\mathsf{BIKE}}}$$

Pure literal elimination

$$\Set{\Set{\mathsf{RAIN},\neg\mathsf{SUN}},\Set{\mathsf{RAIN},\mathsf{BIKE}},\Set{\neg \mathsf{SUN},\mathsf{BIKE}},\Set{\neg\mathsf{SUN},\neg\mathsf{BIKE}}}$$ $$\leadsto$$ $$\Set{\Set{\neg \mathsf{SUN},\mathsf{BIKE}},\Set{\neg\mathsf{SUN},\neg\mathsf{BIKE}}}$$ $$\leadsto$$ $$\Set{\Set{}}$$

Pure literal elimination

Whenever a literal occurs only positively/negatively, set its truth-value accordingly & eliminate every clause containing the literal.

Unit propagation

$$\Set{\Set{\mathsf{RAIN},\neg\mathsf{SUN}},\Set{\mathsf{RAIN},\neg\mathsf{BIKE}}, \Set{\neg \mathsf{SUN}},\Set{\mathsf{BIKE}}}$$ $$\leadsto$$ $$\Set{\Set{\mathsf{RAIN},\neg\mathsf{SUN}},\Set{\mathsf{RAIN}}, \Set{\neg \mathsf{SUN}}}$$ $$\leadsto$$ $$\Set{\Set{\neg \mathsf{SUN}}}$$ $$\leadsto$$ $$\Set{}$$

Unit propagation

When there's a unit clause, set the truth-value accordingly, eliminate the clause, & eliminate the "complement" from every clause.

Warning

$$\Set{\Set{\mathsf{RAIN}},\Set{\neg\mathsf{RAIN}}}$$ $$\leadsto$$ $$\Set{\Set{}}$$

The set is unsatisfiable

Splitting

$$\Set{\Set{\mathsf{RAIN},\neg\mathsf{BIKE}},\Set{\neg\mathsf{RAIN},\neg\mathsf{BIKE}},\Set{\neg\mathsf{RAIN},\mathsf{BIKE}}}$$ $$\leadsto$$ $$a.) \Set{\Set{\neg\mathsf{BIKE}},\Set{\mathsf{BIKE}}}$$ $$\leadsto$$ $$\Set{\Set{}}$$ $$b.) \Set{\Set{\neg\mathsf{BIKE}}}$$ $$\leadsto$$ $$\Set{}$$