CS 228 : Logic in Computer Science
Krishna. S
1/14
Recap
I Completeness of Propositional Logic
I Normal forms
2/14
Satisfiability Checking : Horn
Formulae
I A Horn Formula is a particularly nice kind of CNF formula, which
can be quickly checked for satisfiability.
3/14
Satisfiability Checking : Horn
Formulae
I A Horn Formula is a particularly nice kind of CNF formula, which
can be quickly checked for satisfiability.
I A formula F is a Horn formula if it is in CNF and every disjunction
contains atmost one positive literal.
3/14
Satisfiability Checking : Horn
Formulae
I A Horn Formula is a particularly nice kind of CNF formula, which
can be quickly checked for satisfiability.
I A formula F is a Horn formula if it is in CNF and every disjunction
contains atmost one positive literal.
I p ∧ (¬p ∨ ¬q ∨ r ) ∧ (¬a ∨ ¬b) is Horn, but a ∨ b is not Horn.
3/14
Satisfiability Checking : Horn
Formulae
I A Horn Formula is a particularly nice kind of CNF formula, which
can be quickly checked for satisfiability.
I A formula F is a Horn formula if it is in CNF and every disjunction
contains atmost one positive literal.
I p ∧ (¬p ∨ ¬q ∨ r ) ∧ (¬a ∨ ¬b) is Horn, but a ∨ b is not Horn.
I A basic Horn formula is one which has no ∧. Every Horn formula
is a conjunction of basic Horn formulae.
3/14
Satisfiability Checking : Horn
Formulae
I Three types of basic Horn : no positive literals, no negative
literals, have both positive and negative literals.
4/14
Satisfiability Checking : Horn
Formulae
I Three types of basic Horn : no positive literals, no negative
literals, have both positive and negative literals.
I Basic Horn with both positive and negative literals are written as
an implication p ∧ q ∧ · · · ∧ r → s involving only positive literals.
4/14
Satisfiability Checking : Horn
Formulae
I Three types of basic Horn : no positive literals, no negative
literals, have both positive and negative literals.
I Basic Horn with both positive and negative literals are written as
an implication p ∧ q ∧ · · · ∧ r → s involving only positive literals.
I Basic Horn with no negative literals are of the form p and are
written as > → p.
4/14
Satisfiability Checking : Horn
Formulae
I Three types of basic Horn : no positive literals, no negative
literals, have both positive and negative literals.
I Basic Horn with both positive and negative literals are written as
an implication p ∧ q ∧ · · · ∧ r → s involving only positive literals.
I Basic Horn with no negative literals are of the form p and are
written as > → p.
I Basic Horn with no positive literals are written as
p ∧ q ∧ · · · ∧ r → ⊥.
4/14
Satisfiability Checking : Horn
Formulae
I Three types of basic Horn : no positive literals, no negative
literals, have both positive and negative literals.
I Basic Horn with both positive and negative literals are written as
an implication p ∧ q ∧ · · · ∧ r → s involving only positive literals.
I Basic Horn with no negative literals are of the form p and are
written as > → p.
I Basic Horn with no positive literals are written as
p ∧ q ∧ · · · ∧ r → ⊥.
I Thus, a Horn formula is written as a conjunction of implications.
4/14
The Horn Algorithm
Given a Horn formula H,
I Mark all occurrences of p, whenever > → p is a subformula.
5/14
The Horn Algorithm
Given a Horn formula H,
I Mark all occurrences of p, whenever > → p is a subformula.
I If there is a subformula of the form (p1 ∧ · · · ∧ pm ) → q, where
each pi is marked, and q is not marked, mark all occurrences of
q. Repeat this until there are no subformulae of this form and
proceed to the next step.
5/14
The Horn Algorithm
Given a Horn formula H,
I Mark all occurrences of p, whenever > → p is a subformula.
I If there is a subformula of the form (p1 ∧ · · · ∧ pm ) → q, where
each pi is marked, and q is not marked, mark all occurrences of
q. Repeat this until there are no subformulae of this form and
proceed to the next step.
I Consider subformulae of the form (p1 ∧ · · · ∧ pm ) → ⊥. If there is
one such subformula with all pi marked, then say Unsat,
otherwise say Sat.
5/14
An Example
(> → A) ∧ (C → D) ∧ ((A ∧ B) → C) ∧ ((C ∧ D) → ⊥) ∧ (> → B).
6/14
An Example
(> → A) ∧ (C → D) ∧ ((A ∧ B) → C) ∧ ((C ∧ D) → ⊥) ∧ (> → B).
I (> → A) ∧ (C → D) ∧ ((A ∧ B) → C) ∧ ((C ∧ D) → ⊥) ∧ (> → B).
6/14
An Example
(> → A) ∧ (C → D) ∧ ((A ∧ B) → C) ∧ ((C ∧ D) → ⊥) ∧ (> → B).
I (> → A) ∧ (C → D) ∧ ((A ∧ B) → C) ∧ ((C ∧ D) → ⊥) ∧ (> → B).
I (> → A) ∧ (C → D) ∧ ((A ∧ B) → C) ∧ ((C ∧ D) → ⊥) ∧ (> → B).
6/14
An Example
(> → A) ∧ (C → D) ∧ ((A ∧ B) → C) ∧ ((C ∧ D) → ⊥) ∧ (> → B).
I (> → A) ∧ (C → D) ∧ ((A ∧ B) → C) ∧ ((C ∧ D) → ⊥) ∧ (> → B).
I (> → A) ∧ (C → D) ∧ ((A ∧ B) → C) ∧ ((C ∧ D) → ⊥) ∧ (> → B).
I (> → A) ∧ (C → D) ∧ ((A ∧ B) → C) ∧ ((C ∧ D) → ⊥) ∧ (> → B).
6/14
The Horn Algorithm
The Horn algorithm concludes Sat iff H is satisfiable.
7/14
The Horn Algorithm
The Horn algorithm concludes Sat iff H is satisfiable.
I Let S = {C1 , . . . , Cn } be the set of propositions occurring in H. At
the end of the algorithm, some of these are marked.
7/14
The Horn Algorithm
The Horn algorithm concludes Sat iff H is satisfiable.
I Let S = {C1 , . . . , Cn } be the set of propositions occurring in H. At
the end of the algorithm, some of these are marked.
I Assume H is satisfiable. Then there is an assignment α of S
such that α |= H. For each basic Horn formula B of H, α(B) = 1.
Also, α(⊥) = 0 and α(>) = 1.
7/14
The Horn Algorithm
The Horn algorithm concludes Sat iff H is satisfiable.
I Let S = {C1 , . . . , Cn } be the set of propositions occurring in H. At
the end of the algorithm, some of these are marked.
I Assume H is satisfiable. Then there is an assignment α of S
such that α |= H. For each basic Horn formula B of H, α(B) = 1.
Also, α(⊥) = 0 and α(>) = 1.
I If B has the form > → Ci , then α(Ci ) = 1.
7/14
The Horn Algorithm
The Horn algorithm concludes Sat iff H is satisfiable.
I Let S = {C1 , . . . , Cn } be the set of propositions occurring in H. At
the end of the algorithm, some of these are marked.
I Assume H is satisfiable. Then there is an assignment α of S
such that α |= H. For each basic Horn formula B of H, α(B) = 1.
Also, α(⊥) = 0 and α(>) = 1.
I If B has the form > → Ci , then α(Ci ) = 1.
I If B has the form (C1 ∧ · · · ∧ Cn ) → D, where each α(Ci ) = 1,
then α(D) = 1.
7/14
The Horn Algorithm
The Horn algorithm concludes Sat iff H is satisfiable.
I Let S = {C1 , . . . , Cn } be the set of propositions occurring in H. At
the end of the algorithm, some of these are marked.
I Assume H is satisfiable. Then there is an assignment α of S
such that α |= H. For each basic Horn formula B of H, α(B) = 1.
Also, α(⊥) = 0 and α(>) = 1.
I If B has the form > → Ci , then α(Ci ) = 1.
I If B has the form (C1 ∧ · · · ∧ Cn ) → D, where each α(Ci ) = 1,
then α(D) = 1.
I Hence, α(Ci ) agrees with the marking of the algo.
7/14
The Horn Algorithm
I Assume the algo says H is unsat. Then there is a subformula B
of the form (A1 ∧ · · · ∧ Am ) → ⊥, where each Ai is marked.
Hence, α(Ai ) = 1 for each Ai . By semantics, α(B) = 0, a
contradiction to our assumption that α(B) = 1 for each B.
8/14
The Horn Algorithm
I Assume the algo says H is unsat. Then there is a subformula B
of the form (A1 ∧ · · · ∧ Am ) → ⊥, where each Ai is marked.
Hence, α(Ai ) = 1 for each Ai . By semantics, α(B) = 0, a
contradiction to our assumption that α(B) = 1 for each B.
I Conversely, assume that the algo says Sat. Show that there
exists a satisfying assignment α, using the markings made by
the algo.
8/14
The Horn Algorithm
I Assume the algo says H is unsat. Then there is a subformula B
of the form (A1 ∧ · · · ∧ Am ) → ⊥, where each Ai is marked.
Hence, α(Ai ) = 1 for each Ai . By semantics, α(B) = 0, a
contradiction to our assumption that α(B) = 1 for each B.
I Conversely, assume that the algo says Sat. Show that there
exists a satisfying assignment α, using the markings made by
the algo. Let α be the assignment of S defined by α(Ci ) = 1 iff Ci
is marked. We claim that α |= H.
8/14
The Horn Algorithm
I Assume the algo says H is unsat. Then there is a subformula B
of the form (A1 ∧ · · · ∧ Am ) → ⊥, where each Ai is marked.
Hence, α(Ai ) = 1 for each Ai . By semantics, α(B) = 0, a
contradiction to our assumption that α(B) = 1 for each B.
I Conversely, assume that the algo says Sat. Show that there
exists a satisfying assignment α, using the markings made by
the algo. Let α be the assignment of S defined by α(Ci ) = 1 iff Ci
is marked. We claim that α |= H.
I Show that α |= B for each basic Horn formula B of H.
8/14
The Horn Algorithm
I If B has the form > → A, then A is marked in step 1 of the algo,
and so α(B) = 1.
9/14
The Horn Algorithm
I If B has the form > → A, then A is marked in step 1 of the algo,
and so α(B) = 1.
I If B has the form A1 ∧ . . . Am → G, then G is either ⊥ or an
atomic formula.
9/14
The Horn Algorithm
I If B has the form > → A, then A is marked in step 1 of the algo,
and so α(B) = 1.
I If B has the form A1 ∧ . . . Am → G, then G is either ⊥ or an
atomic formula.
I If some Ai was not marked, then α(Ai ) = 0, and hence α(B) = 1.
9/14
The Horn Algorithm
I If B has the form > → A, then A is marked in step 1 of the algo,
and so α(B) = 1.
I If B has the form A1 ∧ . . . Am → G, then G is either ⊥ or an
atomic formula.
I If some Ai was not marked, then α(Ai ) = 0, and hence α(B) = 1.
I Assume all the Ai ’s were marked. Then α(Ai ) = 1 for all i. Since
the algo said Sat, G 6= ⊥. Then G is also marked (step 2 of
algo). Hence, α(G) = 1, and we have α(B) = 1.
9/14
The Horn Algorithm
I If B has the form > → A, then A is marked in step 1 of the algo,
and so α(B) = 1.
I If B has the form A1 ∧ . . . Am → G, then G is either ⊥ or an
atomic formula.
I If some Ai was not marked, then α(Ai ) = 0, and hence α(B) = 1.
I Assume all the Ai ’s were marked. Then α(Ai ) = 1 for all i. Since
the algo said Sat, G 6= ⊥. Then G is also marked (step 2 of
algo). Hence, α(G) = 1, and we have α(B) = 1.
I Thus, the markings of the algorithm gives rise to a satisfying
assignment α if the algorithm said Sat.
9/14
Complexity of Horn
I Given a Horn formula ψ with n propositions, how many times do
you have to read ψ?
I Step 1: Read once
I Step 2: Read atmost n times
I Step 3: Read once
10/14
Resolution
I Resolution is a technique used to check if a formula in CNF is
satisfiable.
11/14
Resolution
I Resolution is a technique used to check if a formula in CNF is
satisfiable.
I Let C1 , C2 be two clauses. Assume A ∈ C1 and ¬A ∈ C2 for
some atomic formula A. Then the clause
R = (C1 − {A}) ∪ (C2 − {¬A}) is a resolvent of C1 and C2 .
11/14
Resolution
I Resolution is a technique used to check if a formula in CNF is
satisfiable.
I Let C1 , C2 be two clauses. Assume A ∈ C1 and ¬A ∈ C2 for
some atomic formula A. Then the clause
R = (C1 − {A}) ∪ (C2 − {¬A}) is a resolvent of C1 and C2 .
I Let C1 = {A1 , ¬A2 , A3 } and C2 = {A2 , ¬A3 , A4 }. As A3 ∈ C1 and
¬A3 ∈ C2 , we can find the resolvent. The resolvent is
{A1 , A2 , ¬A2 , A4 }.
11/14
Resolution
I Resolution is a technique used to check if a formula in CNF is
satisfiable.
I Let C1 , C2 be two clauses. Assume A ∈ C1 and ¬A ∈ C2 for
some atomic formula A. Then the clause
R = (C1 − {A}) ∪ (C2 − {¬A}) is a resolvent of C1 and C2 .
I Let C1 = {A1 , ¬A2 , A3 } and C2 = {A2 , ¬A3 , A4 }. As A3 ∈ C1 and
¬A3 ∈ C2 , we can find the resolvent. The resolvent is
{A1 , A2 , ¬A2 , A4 }.
I Resolvent not unique : {A1 , A3 , ¬A3 , A4 } is also a resolvent.
11/14
3 rules in Resolution
I Let G be any formula. Let F be the CNF formula resulting from
the CNF algorithm applied to G. Then G ` F (Prove!)
12/14
3 rules in Resolution
I Let G be any formula. Let F be the CNF formula resulting from
the CNF algorithm applied to G. Then G ` F (Prove!)
I Let F be a formula in CNF, and let C be a clause in F . Then
F ` C (Prove!)
12/14
3 rules in Resolution
I Let G be any formula. Let F be the CNF formula resulting from
the CNF algorithm applied to G. Then G ` F (Prove!)
I Let F be a formula in CNF, and let C be a clause in F . Then
F ` C (Prove!)
I Let F be a formula in CNF. Let R be a resolvent of two clauses of
F . Then F ` R (Prove!)
12/14
Completeness of Resolution
Show that resolution can be used to determine whether any given
formula is satisfiable.
I Given F in CNF, let Res0 (F ) = {C | C is a clause in F }.
13/14
Completeness of Resolution
Show that resolution can be used to determine whether any given
formula is satisfiable.
I Given F in CNF, let Res0 (F ) = {C | C is a clause in F }.
I Resn (F ) = Resn−1 (F ) ∪ {R | R is a resolvent of two clauses in
Resn−1 (F )}
13/14
Completeness of Resolution
Show that resolution can be used to determine whether any given
formula is satisfiable.
I Given F in CNF, let Res0 (F ) = {C | C is a clause in F }.
I Resn (F ) = Resn−1 (F ) ∪ {R | R is a resolvent of two clauses in
Resn−1 (F )}
I Res0 (F ) = F , there are finitely many clauses that can be derived
from F .
13/14
Completeness of Resolution
Show that resolution can be used to determine whether any given
formula is satisfiable.
I Given F in CNF, let Res0 (F ) = {C | C is a clause in F }.
I Resn (F ) = Resn−1 (F ) ∪ {R | R is a resolvent of two clauses in
Resn−1 (F )}
I Res0 (F ) = F , there are finitely many clauses that can be derived
from F .
I There is some m such that Resm (F ) = Resm+1 (F ). Denote it by
Res∗ (F ).
13/14
Example
Let F = {{A1 , A2 , ¬A3 }, {¬A2 , A3 }}.
I Res0 (F ) = F
14/14
Example
Let F = {{A1 , A2 , ¬A3 }, {¬A2 , A3 }}.
I Res0 (F ) = F
I Res1 (F ) = F ∪ {A1 , A2 , ¬A2 } ∪ {A1 , ¬A3 , A3 }.
14/14
Example
Let F = {{A1 , A2 , ¬A3 }, {¬A2 , A3 }}.
I Res0 (F ) = F
I Res1 (F ) = F ∪ {A1 , A2 , ¬A2 } ∪ {A1 , ¬A3 , A3 }.
I Res2 (F ) = Res1 (F ) ∪ {A1 , A2 , ¬A3 } ∪ {A1 , A3 , ¬A2 }
14/14
