Oversimplified history

Logic formalizes reasoning.

• Since ancient Greek (until modern high school):
  • First subject taught to young people.
  • Logic rules are classified and named.
  • Goal: Reasoning and debating.
• 19c Mathematicians:
  • Formalization of logic.
  • Goal: Clarifying foundation of mathematics.
  • Subjects: Consistency, independence, soundness, completeness.
  • Hilbert’s program “ended” by Gödel.
• Modern days:
  • Applications of logic in computer sciences.
  • Propositional logic applied both in hardware and software.
  • First-order logic applied in automated theorem prover and logic programming.

Structure of the course

We will learn about propositional logic and first-order (predicate) logic. For each we will study

• Syntax : Which strings are allowed?
• Semantics : What does a string mean?
• Deduction : Rules of inference between formulas.
• Resolution : Algorithm for automated proving.
• Application : SAT & logic programming.

Beginning today: propositional logic.

Section 1
Syntax

Atoms and operators

Definition: An atomic proposition is a sentence that is

• declarative.
• either true or false.
• cannot be decomposed.

The symbols used in a formula in propositional logic are

• Atomic propositions (atoms).
• Boolean operators: $\neg$, $\land$, $\lor$, …

Example

• One plus one equals two.
• The earth is flat.
• Sweet soy milk is more delicious.
• …

Example (Non-examples)

• Shut up!
• How are you?
• bla bla bla …
• …

Formula

Definition: A formula in propositional logic is generated by the following context-free grammar:

• terminals are atoms and operators.
• a nonterminal symbol fml.
• production rules are:
  • fml$\rightarrow p$, $p$ is an atom.
  • fml$\rightarrow\neg$fml.
  • fml$\rightarrow$(fml op fml).
  • op$\rightarrow\land\mid\lor\mid\rightarrow\mid\leftrightarrow\mid\dots$

Any formula $F$ that occurs in another formula $G$ is called a subformula of $G$.

Example

Or we can define recursively as follows:

• An atom is a formula (atomic formula).
• For every formula $F$, $\neg F$ is a formula.
• For every two formulas $F$ and $G$, $(F \land G)$ and $(F \lor G)$ and … are formulas.

Abbreviations
$(F \rightarrow G)$ means $(\neg F \lor G)$, $(F \leftrightarrow G)$ means $((F \land G) \lor (\neg F \land \neg G))$

Remark: All binary operators can be defined in terms of $\neg$, $\land$, $\lor$.

Precedence to reduce (‘s and )‘s:

A formula can be represented as a tree

• The leaves are labeled by the atoms.
• The nodes are labeled by operators.
• The $\neg$ node has a single child.
• Other operator nodes each have two children.
• Subtrees are subformulas.

Example

Induction on formula

To show that a statement $\mathcal{S}$ holds for every formula $F$, we show

• $\mathcal{S}$ holds for every atomic formula $A$.
• Under the hypothesis that $\mathcal{S}$ holds for formulas $F$ and $G$, then $\mathcal{S}$ holds for $\neg F$, $F \land G$ and $F \lor G$.

Section 2
Semantics

Interpretation

Definition: Let $F$ be a formula, and $\mathcal{A}$ be the set of atoms appearing in $F$. An interpretation of $F$ is a function $\mathcal{I} : \mathcal{A} \rightarrow \{1,0\}$. In other words, an interpretation assigns a truth value (true for $1$ or false for $0$) to every atom in $F$.

Definition: Given an interpretation $\mathcal{I}$ of $F$, the truth value of $F$ under $\mathcal{I}$, denoted $\mathcal{I}(F)$ is defined inductively as follows:

• $\mathcal{I}(\neg A) = \begin{cases} 1 & \text{if } \mathcal{I}(A) = 0, \\ 0 & \text{if } \mathcal{I}(A) = 1. \end{cases}$
• $\mathcal{I}(A \land B) = \begin{cases} 1 & \text{if } \mathcal{I}(A) = \mathcal{I}(B) = 1, \\ 0 & \text{otherwise.} \end{cases}$
• $\mathcal{I}(A \lor B) = \begin{cases} 0 & \text{if } \mathcal{I}(A) = \mathcal{I}(B) = 0, \\ 1 & \text{otherwise.} \end{cases}$

Truth table

• $\neg$ is intended to model the word “not”.
• $\land$ is intended to model the word “and”.
• $\lor$ is intended to model the word “or”, but is inclusive or, not exclusive or.
• $P \rightarrow Q$ is defined as $\neg P \lor Q$.
• $\rightarrow$ is read “implies” but does not claim causation.

Model and satisfiability

Definition: Given an interpretation $\mathcal{I}$ of a formula $F$, if $\mathcal{I}(F) = 1$, we say that $F$ holds under $\mathcal{I}$, and $\mathcal{I}$ is a model of $F$, and write $\mathcal{I} \models F$.

Definition

• A formula $F$ is satisfiable if $F$ has a model.
• Otherwise $F$ is unsatisfiable.
• A formula $F$ is valid or a tautology if every interpretation is a model, and we write $\models F$.

Theorem: A formula $F$ is a tautology iff $\neg F$ is unsatisfiable.

Decision procedure

• We want an algorithm that decides satisfiability.
• That is: given an arbitrary formula $F$, it terminates and returns yes if $F$ is satisfiable, and no otherwise.
• Such an algorithm, when applied to $\neg F$, can decide validity.

Example: The truth table is such an algorithm, but very inefficient.
Is there a better algorithm?

Logical equivalence

Definition: Let $F_1$ and $F_2$ be two formulas (on the same set of atoms). If $\mathcal{I}(F_1) = \mathcal{I}(F_2)$ for all interpretations $\mathcal{I}$, then $F_1$ and $F_2$ are logically equivalent, denoted by $F_1 \equiv F_2$.

Theorem (material equivalence vs logic equivalence)$F_1 \equiv F_2$ iff $F_1 \leftrightarrow F_2$ is true in every interpretation.

Theorem: Let $F$ be a subformula of $G$ and $F’ \equiv F$. Then $G \equiv G\{F \leftarrow F’\}$, the latter denotes the formula obtained by replacing all occurrences of $F$ by $F’$.

• Absorption of constants
  $A \lor 1 \equiv 1$, $A \land 1 \equiv A$, $0 \rightarrow A \equiv 1$, …
• Identical operands
  $A \equiv \neg\neg A$, $A \land \neg A \equiv 0$, $A \rightarrow A \equiv 1$, …
• Commutativity, Associativity, Distributivity
  $A \lor B \equiv B \lor A$, $A \land (B \land C) \equiv (A \land B) \land C$, $\neg(A \lor B) \equiv \neg A \land \neg B$, $A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)$, …
• Defining operators
  $A \rightarrow B \equiv \neg A \lor B$, …

Set of formulas

Definition: Let $\mathcal{F} = \{F_1, F_2, \dots, F_n\}$ be a set of formulas, and $\mathcal{A}$ be the set of all atoms appearing in some formulas in $\mathcal{F}$. An interpretation of $\mathcal{F}$ is a function $\mathcal{I} : \mathcal{A} \rightarrow \{1,0\}$. The truth value of $F_i$ under $\mathcal{I}$ is defined similarly as above.

Definition: A set of formulas $\mathcal{F} = \{F_1, F_2, \dots, F_n\}$ is (simultaneously) satisfiable if there is an interpretation $\mathcal{I}$ such that $\mathcal{I}(F_i) = 1$ for all $i$. If this is the case, we say that $\mathcal{I}$ is a model of $\mathcal{F}$. If this is not the case, we say that $\mathcal{F}$ is unsatisfiable.

Logical consequence

Definition: Let $\mathcal{F} = \{F_1, F_2, \dots, F_n\}$ be a set of formulas and $G$ be a formula. $G$ is a logical consequence of $\mathcal{F}$, denoted $\mathcal{F} \models G$, iff every model of $\mathcal{F}$ is a model of .$G$

Theorem (material implication vs logmical consequence)$\mathcal{F} \models G$ iff $\models \land_{i=1}^n F_i \rightarrow G$.

Literals

Definition: A literal is an atom or the negation of an atom. For an atom $p$, $p$ is called a positive literal, $\neg p$ is a negative literal, and the pair $\{p, \neg p\}$ is a complementary pair of literals.

Theorem: A set of literals is satisfiable iff it does not contain a complementary pair of literals.

Semantic tableau

Given a formula $F$, output a tree $\mathcal{T}$ all of whose leaves are marked closed$\times$ or open$\odot$.

• Initially, the tree has a single node labeled with $\{F\}$ (not marked!)
• Repeat: Choose an unmarked leaf $v$ labeled with a set of formulas $U(v)$ (understood with $\land$).
  • If $U(v)$ is a set of literals, mark $v$closed$\times$ if it contains a complementary pair, or open$\odot$ otherwise.
  • Otherwise, choose a formula $G$ in $U(v)$ which is not a literal in the following order of preference:
    • If $G$ has the form of $\neg\neg G’$, create a child $w$ of $v$ with label $(U(v) \setminus \{G\}) \cup \{G’\}$.
    • If $G \equiv G_1 \land G_2$, create a child $w$ of $v$ with label $(U(v) \setminus \{G\}) \cup \{G_1, G_2\}$.
    • If $G \equiv G_1 \lor G_2$, create two children $w_1, w_2$ of $v$ with label $(U(v) \setminus \{G\}) \cup \{G_i\}$ for $w_i$.

Example

Theorem

• The algorithm terminates. After termination, all leaves are marked closed or open.
• $F$ is unsatisfiable iff $\mathcal{T}$ is closed (meaning all leaves marked closed).
• $F$ is satisfiable iff is open (meaning not closed).

Much better than truth tables.
Is there a better algorithm?

Sketched proofs

Sketched proof for termination.
Design an integer valued function $W(v)$ related to the number of binary operators and the number of negations in $U(v)$. Prove that $W(v)$ is strictly decreasing, i.e. for a child $v’$ of $v$, $W(v’) < W(v)$.

Sketched proof for soundness.
Need to prove: If the tableau closes, then the formula is unsatisfiable. Induction on the height of the nodes.

Sketched proof for completeness.
Need to prove: If a tableau is open, then the formula is satisfiable. Let $\ell$ be an open leaf, the union $U$ of $U(v)$ for $v$ on the path from the root to $\ell$ is a Hintikka set:

• For all atom $p$ in a formula in $U$, either $p \notin U$ or $\neg p \notin U$.
• If $U \ni G \equiv G_1 \land G_2$, $G_1 \in U$ and $G_2 \in U$.
• If $U \ni G \equiv G_1 \lor G_2$, $G_1 \in U$ or $G_2 \in U$.

Such a set satisfiable.

Section 3
Deduction

Deductive system

Definition: A deductive system consists of a set of formulas called axioms and a set of rules of inference. A proof in a deductive system is a (finite) sequence of formulas $S = \{A_1, A_2, \dots, A_n\}$, where each $A_i$ is either a theorem or a formula that can be inferred from previous formulas in the sequence using a rule of inference. The last formula $A_n$ is called a theorem and the sequence $S$ is the proof of $A_n$. In this case, we say that $A_n$ is provable, denoted $\vdash A_n$.

A priori, no connection to semantics, purely syntactical.
In practice, hope to be semantically “meaningful”.

Gentzen system

• Axioms (only one type): set of literals (understood with $\lor$) containing a complementary pair.
• Rules of inference: infer a set of formulas $U$ from one or two sets of formulas $U_1$ and $U_2$.
• If $G_1 \in U_1$, $U = U_1 \setminus \{G_1\} \cup \{\neg\neg G_1\}$ can be inferred.
• If $G_1, G_2 \in U_1$, $U = U_1 \setminus \{G_1, G_2\} \cup \{G_1 \lor G_2\}$ can be inferred.
• If $G_1 \in U_1$ and $G_2 \in U_2$, $U = (U_1 \setminus \{G_1\}) \cup (U_2 \setminus \{G_2\}) \cup \{G_1 \land G_2\}$ can be inferred.

Prove $\vdash (p \lor q) \rightarrow (q \lor p)$ in Gentzen system.

Proof.

1. $\vdash \neg p, q, p$ (Axiom)
2. $\vdash \neg q, q, p$ (Axiom)
3. $\vdash \neg(p \lor q), q, p$ (from 1 and 2, $\neg p \land \neg q \equiv \neg(p \lor q)$)
4. $\vdash \neg(p \lor q), (q \lor p)$ (from 3)
5. $\vdash (p \lor q) \rightarrow (q \lor p)$ (from 4)

Prove $\vdash p \lor (q \land r) \rightarrow (p \lor q) \land (p \lor r)$ in Gentzen system.

Proof.

1. $\vdash \neg p, p, q$ (Axiom)
2. $\vdash \neg p, (p \lor q)$ (from 1)
3. $\vdash \neg p, p, r$ (Axiom)
4. $\vdash \neg p, (p \lor r)$ (from 3)
5. $\vdash \neg p, (p \lor q) \land (p \lor r)$ (from 2, 4)
6. $\vdash \neg q, \neg r, p, q$ (Axiom)
7. $\vdash \neg q, \neg r, (p \lor q)$ (from 6)
8. $\vdash \neg q, \neg r, p, r$ (Axiom)
9. $\vdash \neg q, \neg r, (p \lor r)$ (from 8)
10. $\vdash \neg q, \neg r, (p \lor q) \land (p \lor r)$ (from 7, 9)
11. $\vdash \neg(q \land r), (p \lor q) \land (p \lor r)$ (from 10)
12. $\vdash \neg(p \lor (q \land r)), (p \lor q) \land (p \lor r)$ (from 5, 11)
13. $\vdash p \lor (q \land r) \rightarrow (p \lor q) \land (p \lor r)$ (from 12)

Gentzen proof for $A$ corresponds to semantic tableau for $\neg A$ upside down.

Theorem
$\models A$ iff $\vdash A$ in Gentzen system iff there is a closed semantic tableau for $\neg A$.

Hilbert system

• Axioms:
  1. $\vdash (A \rightarrow (B \rightarrow A))$
  2. $\vdash (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$
  3. $\vdash (\neg B \rightarrow \neg A) \rightarrow (A \rightarrow B)$
• Rule (only one): modus ponens, MP

Prove $\vdash A \rightarrow A$.

Proof.

1. $\vdash (A \rightarrow ((A \rightarrow A) \rightarrow A)) \rightarrow ((A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A))$ (Axiom 2)
2. $\vdash A \rightarrow ((A \rightarrow A) \rightarrow A)$ (Axiom 1)
3. $\vdash (A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)$ (MP 1, 2)
4. $\vdash A \rightarrow (A \rightarrow A)$ (Axiom 1)
5. $\vdash A \rightarrow A$ (MP 3, 4)

Definition: Let $U$ be a set of formulas and $A$ a formula. $U \vdash A$ means that the formulas in $U$ are assumptions in a proof of $A$. A proof under the assumptions $U$ is a sequence of lines $U_i \vdash \phi_i$ such that $U_i \subseteq U$ and $\phi_i$

• is an axiom,
• is a member of $U$ (assumption),
• is a previously proved theorem,
• can be inferred by MP from previous lines.

Derived rules in Hilbert system

• $\displaystyle\frac{U \cup \{A\} \vdash B}{U \vdash A \rightarrow B}$ (deduction rule).
• $\displaystyle\frac{U \vdash \neg B \rightarrow \neg A}{U \vdash A \rightarrow B},\ \frac{U \vdash A \rightarrow B}{U \vdash \neg B \rightarrow \neg A}$ (contraposition rule).
• $\displaystyle\frac{U \vdash A \rightarrow B\quad U \vdash B \rightarrow C}{U \vdash A \rightarrow C}$ (transitivity rule).
• $\displaystyle\frac{U \vdash A \rightarrow (B \rightarrow C)}{U \vdash B \rightarrow (A \rightarrow C)}$ (exchange of antecedents).
• $\displaystyle\frac{U \vdash \neg\neg A}{U \vdash A}$, $\displaystyle\frac{U \vdash A}{U \vdash \neg\neg A}$ (double negation).
• $\displaystyle\frac{U \vdash \neg A \rightarrow 0}{U \vdash A}$ (reductio ad absurdum).

Prove $\vdash (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$.

Proof.

1. $\{A \rightarrow B, B \rightarrow C, A\} \vdash A$ (Assumption)
2. $\{A \rightarrow B, B \rightarrow C, A\} \vdash A \rightarrow B$ (Assumption)
3. $\{A \rightarrow B, B \rightarrow C, A\} \vdash B$ (MP 1, 2)
4. $\{A \rightarrow B, B \rightarrow C, A\} \vdash B \rightarrow C$ (Assumption)
5. $\{A \rightarrow B, B \rightarrow C, A\} \vdash C$ (MP 3, 4)
6. $\{A \rightarrow B, B \rightarrow C\} \vdash A \rightarrow C$ (Deduction 5)
7. $\{A \rightarrow B\} \vdash (B \rightarrow C) \rightarrow (A \rightarrow C)$ (Deduction 6)
8. $\vdash (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$ (Deduction 7)

Prove $\vdash (A \rightarrow (B \rightarrow C)) \rightarrow (B \rightarrow (A \rightarrow C))$.

Proof.

1. $\{A \rightarrow (B \rightarrow C), B, A\} \vdash A$ (Assumption)
2. $\{A \rightarrow (B \rightarrow C), B, A\} \vdash A \rightarrow (B \rightarrow C)$ (Assumption)
3. $\{A \rightarrow (B \rightarrow C), B, A\} \vdash B \rightarrow C$ (MP 1, 2)
4. $\{A \rightarrow (B \rightarrow C), B, A\} \vdash B$ (Assumption)
5. $\{A \rightarrow (B \rightarrow C), B, A\} \vdash C$ (MP 3, 4)
6. $\{A \rightarrow (B \rightarrow C), B\} \vdash A \rightarrow C$ (Deduction 5)
7. $\{A \rightarrow (B \rightarrow C)\} \vdash B \rightarrow (A \rightarrow C)$ (Deduction 6)
8. $\vdash (A \rightarrow (B \rightarrow C)) \rightarrow (B \rightarrow (A \rightarrow C))$ (Deduction 7)

Prove $\vdash \neg\neg A \rightarrow A$.

Proof.

1. $\{\neg\neg A\} \vdash \neg\neg A \rightarrow (\neg\neg\neg A \rightarrow \neg\neg A)$ (Axiom 1)
2. $\{\neg\neg A\} \vdash \neg\neg A$ (Assumption)
3. $\{\neg\neg A\} \vdash \neg\neg\neg A \rightarrow \neg\neg A$ (MP 1, 2)
4. $\{\neg\neg A\} \vdash \neg A \rightarrow \neg\neg\neg A$ (Contrapositive 3)
5. $\{\neg\neg A\} \vdash \neg\neg A \rightarrow A$ (Contrapositive 4)
6. $\{\neg\neg A\} \vdash A$ (MP 2, 5)
7. $\vdash \neg\neg A \rightarrow A$ (Deduction 6)

Prove $\vdash (\neg A \rightarrow 0) \rightarrow A$.

Proof.

1. $\{\neg A \rightarrow 0\} \vdash \neg A \rightarrow 0$ (Assumption)
2. $\{\neg A \rightarrow 0\} \vdash \neg 0 \rightarrow \neg\neg A$ (Contrapositive)
3. $\{\neg A \rightarrow 0\} \vdash \neg 0$ ($0 := \neg(B \rightarrow B)$)
4. $\{\neg A \rightarrow 0\} \vdash \neg\neg A$ (MP 2, 3)
5. $\{\neg A \rightarrow 0\} \vdash A$ (Double negation)
6. $\vdash (\neg A \rightarrow 0) \rightarrow A$ (Deduction 5)

Theorem

• Sound: If $\vdash A$ then $\models A$.
• Complete: If $\models A$ then $\vdash A$.

Sketched proof for soundness and completeness.

• Soundness:
  Axioms are valid, and MP is sound. That is, if $A$ and $A \rightarrow B$ are valid, so is $B$.
• Completeness:
  For a set $U$ of formula, if $\vdash U$ in Gentzen system, then $\vdash \lor U$ in Hilbert system. Moreover, if $U’ \subseteq U$ and $\vdash \lor U’$ in Hilbert system, then $\vdash \lor U$ in Hilbert system. Finally, the rules of inference of Gentzen system can be simulated in Hilbert system.

formula $\rightarrow$ semantic tableau $\rightarrow$ Gentzen proof $\rightarrow$ Hilbert proof

Definition: A set $U$ of formula is inconsistent iff for some formula $A$, $U \vdash A$ and $U \vdash \neg A$. $U$ is consistent iff it is not inconsistent. A deduction system is inconsistent if it contains an inconsistent set of formula.

Theorem
In the Hilbert system,

• $U$ is inconsistent iff for all $A$, $U \vdash A$.
• $U$ is consistent iff for some $A$, $U \nvdash A$.
• $U \vdash A$ iff $U \cup \{\neg A\}$ is inconsistent.

Since the Hilbert system is sound and $\not\models 0$, we have $\not\vdash 0$ in the Hilbert system, so the Hilbert system is consistent.

Section 4
Resolution

Conjunctive normal form (CNF)

Definition: A formula is in conjunctive normal form (CNF) if it is a conjunction of disjunctions of literals.

Theorem: Every formula can be transformed into an equivalent formula in CNF.

1. Express all operators in terms of $\neg$, $\land$, $\lor$.
2. Push negations inward.
3. Delete double negations.
4. Distribute disjunctions.

Example

$(\neg p \rightarrow \neg q) \rightarrow (p \rightarrow q)$
$\equiv \neg(\neg\neg p \lor \neg q) \lor (\neg p \lor q)$
$\equiv (\neg\neg\neg p \land \neg\neg q) \lor (\neg p \lor q)$
$\equiv (\neg p \land q) \lor (\neg p \lor q)$
$\equiv (\neg p \lor \neg p \lor q) \land (q \lor \neg p \lor q)$

Clausal form

Definition

• A clause is a set of literals (seen as disjunction of the literals).
• A formula in clausal form is a set of clauses (seen as conjunction of the clauses).

A clausal form is just another way to write a formula in CNF.

• A clause with exactly one literal is a unit clause.
• A clause with no literal is an empty clause, denoted $\square$.
  An empty clause is unsatisfiable.
• A clause with a pair of clashing literals is trivial.
  A trivial clause is valid, and can be removed from a set of clauses.
• An empty set of clauses is denoted $\emptyset$.
  An empty set of clauses is valid.

Resolvent

Definition: Let $l$ be a literal and $C_1, C_2$ be clauses such that $l \in C_1$ and $l^c \in C_2$. We say that $C_1$ and $C_2$ are clashing clauses, and they clash on the complementary pair of literals $l$ and $l^c$. The resolvent of $C_1$ and $C_2$ is the clause

$C_1$ and $C_2$ are called parent clauses of $C$.

Theorem

• If two clauses clash on more than one complementary pair, their resolvent is trivial.
• The resolvent is satisfiable iff the parent clauses are both (simultaneously) satisfiable.

Resolution

• Input: A set of clauses $S$.
• Output: Satisfiability of $S$ (yes or no).
• Initially $S_0 = S$. Repeat the following to obtain $S_{i+1}$ from $S_i$.
  • Choose a new clashing pair of clauses $C_1, C_2 \in S_i$
  • Compute the resolvent $C$.
  • If $C$ is trivial, $S_{i+1} = S_i$.
  • If $C$ is not trivial, $S_{i+1} = S_i \cup \{C\}$.
• Terminates if
  • $C = \square$.
  • No clashing pair.

Example
$C = \{C_1, C_2, C_3, C_4\}$ where

1. $C_1 = p$
2. $C_2 = \bar{p}q$
3. $C_3 = \bar{r}$
4. $C_4 = \bar{p}\bar{q}r$, then
5. $C_5 = \bar{p}\bar{q}$ resolving $C_3$ and $C_4$
6. $C_6 = \bar{p}$ resolving $C_2$ and $C_5$
7. $C_7 = \square$ resolving $C_1$ and $C_6$

A derivation of $\square$ from $S$ is a refutation by resolution of $S$.

Theorem

• If there is a refutation by resolution of $S$, then $S$ is unsatisfiable.
• If $S$ is unsatisfiable, then $\square$ will be derived by resolution.

Section 5
Application: SAT

Clauses

We write $S \approx S’$ to denote that $S$ is satisfiable iff $S’$ is satisfiable.

Theorem (and definition) A pure literal in $S$ is a literal $l$ that appears in some clause but $l^c$ does not appear in any clause. If this is the case, let $S’$ be obtained from $S$ by deleting every clause containing $l$. Then $S \approx S’$.

Theorem (and definition) Let $\{l\} \in S$ be a unit clause and $S’$ be obtained from $S$ by deleting every clause containing $l$ and deleting $l^c$ from every remaining clause. Then $S \approx S’$.

Theorem (and definition) Let $C_1 \subseteq C_2$ be two clauses in $S$. We say that $C_1$ subsumes $C_2$. If this is the case, let $S’ = S \setminus \{C_2\}$. Then $S \approx S’$.

Theorem (and definition) Let $U$ be a set of atomic propositions. The renaming of $S$ by $U$, denoted $R_U(S)$, is obtained from $S$ by replacing each literal $l$ on an atom $p \in U$ by $l^c$. We have $S \approx R_U(S)$.

Davis-Putnam Algorithm

• Input: A formula $F$ in clausal form.
• Output: $F$ is satisfiable or unsatisfiable.
• Repeat the following:
  • If there is a unit clause $\{l\}$, delete all clauses containing $l$ and delete $l^c$ from all other clauses.
  • If there is a pure literal $l$, delete all clauses containing $l$.
  • Only when the previous two do not apply, choose an atom $p$ and perform all possible resolutions on clauses clashing on $p$. Add these resolvents and delete all clauses containing $p$ or $\neg p$.
• Terminate
  • If empty clause $\square$ is produced, report unsatisfiable.
  • If no more rules applicable, report satisfiable.

Repeating the step about unit clauses until no longer applicable is called unit propagation.

Davis-Putnam-Logemann-Loveland Algorithm

• Input: A formula $F$ in clausal form.
• Output: $F$ is unsatisfiable or satisfiable with a partial interpretation that satisfies $F$.
• Call the following recursive function $\operatorname{DPLL}(B, \mathcal{I})$, where $B$ is a set of clauses and $\mathcal{I}$ is a partial interpretation, initially with $B = F$ and $\mathcal{I}$ empty.
  • Obtain $B’$ from $B$ by unit propagation. Obtain $\mathcal{I}’$ from $\mathcal{I}$ by adding all assignments during the propagation.
  • Evaluate $B’$ under $\mathcal{I}’$.
    • If $B’$ satisfied, return satisfiable and $\mathcal{I}’$.
    • If $B’$ contains a clause $C$ such that $\mathcal{I}'(C) = 0$, return unsatisfiable.
    • Otherwise, continue
  • Choose an atom $p$ in $B’$, extend $\mathcal{I}’$ to $\mathcal{I}_0$ with $\mathcal{I}_0(p) = 0$. Call $\operatorname{DPLL}(B’, \mathcal{I}_0)$. If result is satisfiable, return it. Otherwise continue.
  • Choose an atom $p$ in $B’$, extend $\mathcal{I}’$ to $\mathcal{I}_1$ with $\mathcal{I}_1(p) = 1$. Call $\operatorname{DPLL}(B’, \mathcal{I}_1)$. Return the result.

Linear time cases

The 2-SAT problem (satisfiability when each clause contains at most two literals) can be solved in linear time.

Definition: A formula $F$ in CNF is a Horn formula if every disjunction contains at most one positive literal.

A Horn formula can also be written in the form of conjunctions of implications.
The satisfiability of a Horn formula can be decided only by unit propagation (in linear time).