IA008: Computational Logic
1. Propositional Logic
Achim Blumensath
blumens@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
Basic Concepts
Propositional Logic
Syntax
▸ Variables A, B, C, . . . , X, Y, Z, . . .
▸ Operators ∧, ∨, ¬, →, ↔
Semantics
J ⊧ φ J Variables → {true, false}
Examples
φ = A ∧ (A → B) → B ,
ψ = ¬(A ∧ B) ↔ (¬A ∨ ¬B) .
Terminology
▸ entailment φ ⊧ ψ (do not confuse with J ⊧ φ!)
▸ equivalence φ ≡ ψ (do not confuse with φ = ψ!)
▸ φ ≡ ψ iff φ ⊧ ψ and ψ ⊧ φ
Terminology
▸ entailment φ ⊧ ψ (do not confuse with J ⊧ φ!)
▸ equivalence φ ≡ ψ (do not confuse with φ = ψ!)
▸ φ ≡ ψ iff φ ⊧ ψ and ψ ⊧ φ
▸ satisfiability φ ≢ false
▸ validity φ ≡ true
▸ Every valid formula is satisfiable.
▸ φ is valid iff ¬φ is not satisfiable.
▸ φ ⊧ ψ iff φ → ψ is valid.
Examples
▸ A ∧ (A → B) → B is
Terminology
▸ entailment φ ⊧ ψ (do not confuse with J ⊧ φ!)
▸ equivalence φ ≡ ψ (do not confuse with φ = ψ!)
▸ φ ≡ ψ iff φ ⊧ ψ and ψ ⊧ φ
▸ satisfiability φ ≢ false
▸ validity φ ≡ true
▸ Every valid formula is satisfiable.
▸ φ is valid iff ¬φ is not satisfiable.
▸ φ ⊧ ψ iff φ → ψ is valid.
Examples
▸ A ∧ (A → B) → B is valid.
▸ A ∨ B is
Terminology
▸ entailment φ ⊧ ψ (do not confuse with J ⊧ φ!)
▸ equivalence φ ≡ ψ (do not confuse with φ = ψ!)
▸ φ ≡ ψ iff φ ⊧ ψ and ψ ⊧ φ
▸ satisfiability φ ≢ false
▸ validity φ ≡ true
▸ Every valid formula is satisfiable.
▸ φ is valid iff ¬φ is not satisfiable.
▸ φ ⊧ ψ iff φ → ψ is valid.
Examples
▸ A ∧ (A → B) → B is valid.
▸ A ∨ B is satisfiable but not valid.
▸ ¬A ∧ A is
Terminology
▸ entailment φ ⊧ ψ (do not confuse with J ⊧ φ!)
▸ equivalence φ ≡ ψ (do not confuse with φ = ψ!)
▸ φ ≡ ψ iff φ ⊧ ψ and ψ ⊧ φ
▸ satisfiability φ ≢ false
▸ validity φ ≡ true
▸ Every valid formula is satisfiable.
▸ φ is valid iff ¬φ is not satisfiable.
▸ φ ⊧ ψ iff φ → ψ is valid.
Examples
▸ A ∧ (A → B) → B is valid.
▸ A ∨ B is satisfiable but not valid.
▸ ¬A ∧ A is not satisfiable.
Equivalence Transformations
De Morgan’s laws
¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ
¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ
Equivalence Transformations
De Morgan’s laws
¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ
¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ
Distributive laws
φ ∧ (ψ ∨ ϑ) ≡ (φ ∧ ψ) ∨ (φ ∧ ϑ)
φ ∨ (ψ ∧ ϑ) ≡ (φ ∨ ψ) ∧ (φ ∨ ϑ)
Normal Forms
Conjunctive Normal Form (CNF)
(A ∨ ¬B) ∧ (¬A ∨ C) ∧ (A ∨ ¬B ∨ ¬C)
Disjunctive Normal Form (DNF)
(A ∧ C) ∨ (¬A ∧ ¬B) ∨ (A ∧ ¬B ∧ ¬C)
Clauses
Definitions
▸ literal A or ¬A
▸ clause set of literals {A, B, ¬C}
short-hand for disjunction A ∨ B ∨ ¬C
Clauses
Definitions
▸ literal A or ¬A
▸ clause set of literals {A, B, ¬C}
short-hand for disjunction A ∨ B ∨ ¬C
Example
CNF φ = (A ∨ ¬B ∨ C) ∧ (¬A ∨ C) ∧ B
clauses {A, ¬B, C}, {¬A, C}, {B}
Clauses
Definitions
▸ literal A or ¬A
▸ clause set of literals {A, B, ¬C}
short-hand for disjunction A ∨ B ∨ ¬C
Example
CNF φ = (A ∨ ¬B ∨ C) ∧ (¬A ∨ C) ∧ B
clauses {A, ¬B, C}, {¬A, C}, {B}
Notation
Φ[L = true] = {C ∖ {¬L} C ∈ Φ , L ∉ C } .
The Satisfiability Problem
Davis-Putnam-Logemann-Loveland (DPLL) Algorithm
Input: a set of clauses Φ
Output: true if Φ is satisfiable, false otherwise.
DPLL(Φ)
for every singleton {L} in Φ (* simplify Φ *)
Φ = Φ[L = true]
for every literal L whose negation does not occur in Φ
Φ = Φ[L = true]
if Φ contains the empty clause then (* are we done? *)
return false
if Φ is empty then
return true
choose some literal L in Φ (* try L = true and L = false *)
if DPLL(Φ[L = true]) then
return true
else
return DPLL(Φ[L = false])
Example
Φ = {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step 1: A = true
Example
Φ = {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step 1: A = true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Step 2: B = true
Example
Φ = {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step 1: A = true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Step 2: B = true
{C, D}, {¬D}, {¬C}, {¬C, ¬D}
Step 3: C = false and D = false
Example
Φ = {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step 1: A = true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Step 2: B = true
{C, D}, {¬D}, {¬C}, {¬C, ¬D}
Step 3: C = false and D = false
{D}, {¬D}
Example
Φ = {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step 1: A = true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Step 2: B = true
{C, D}, {¬D}, {¬C}, {¬C, ¬D}
Step 3: C = false and D = false
{D}, {¬D}
∅ failure
Example
Φ = {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step 1: A = true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Backtrack to step 2: B = false
Example
Φ = {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step 1: A = true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Backtrack to step 2: B = false
{C, D}, {¬C, ¬D}
Step 3: C = true
Example
Φ = {{A, B, ¬C}, {¬B, C, D}, {¬A, ¬B, ¬D}, {B, C, D},
{¬A, ¬B, ¬C}, {¬A, ¬C, ¬D}}
Step 1: A = true
{¬B, C, D}, {¬B, ¬D}, {B, C, D}, {¬B, ¬C}, {¬C, ¬D}
Backtrack to step 2: B = false
{C, D}, {¬C, ¬D}
Step 3: C = true
{¬D} satisfiable
Solution: A = true, B = false, C = true, D = false
Expressing graph problems
Vertex cover
Variables:
Cv vertex v belongs to the cover
Expressing graph problems
Vertex cover
Variables:
Cv vertex v belongs to the cover
Formulae:
Cu ∨ Cv for every edge ⟨u, v⟩ ∈ E
Size≤
k “At most k of the Cv are true.”
Expressing graph problems
Vertex cover
Variables:
Cv vertex v belongs to the cover
Formulae:
Cu ∨ Cv for every edge ⟨u, v⟩ ∈ E
Size≤
k “At most k of the Cv are true.”
Clique
Variables:
Cv vertex v belongs to the clique
Expressing graph problems
Vertex cover
Variables:
Cv vertex v belongs to the cover
Formulae:
Cu ∨ Cv for every edge ⟨u, v⟩ ∈ E
Size≤
k “At most k of the Cv are true.”
Clique
Variables:
Cv vertex v belongs to the clique
Formulae:
¬Cu ∨
¬Cv
for every non-edge ⟨u, v⟩ ∉ E
Size≥
k “At least k of the Cv are true.”
Expressing graph problems
The Size≥
k formulae
Fix an enumeration v0, . . . , vn−1 of V.
Variables:
Sk
m at least k variables Cvi with i < m are true
Expressing graph problems
The Size≥
k formulae
Fix an enumeration v0, . . . , vn−1 of V.
Variables:
Sk
m at least k variables Cvi with i < m are true
Formulae:
S0
m
¬Sk
0 for k > 0
Cvi → [Sk
i ↔ Sk+1
i+1 ]
¬Cvi → [Sk
i ↔ Sk
i+1]
Sk
n
Expressing graph problems
The Size≥
k formulae
Fix an enumeration v0, . . . , vn−1 of V.
Variables:
Sk
m at least k variables Cvi with i < m are true
Formulae:
S0
m
¬Sk
0 for k > 0
Cvi → [Sk
i ↔ Sk+1
i+1 ]
¬Cvi → [Sk
i ↔ Sk
i+1]
Sk
n
v0 v1 v2
Cvi 1 0 1
S0
i 1 1 1 1
S1
i 0 1 1 1
S2
i 0 0 0 1
S3
i 0 0 0 0
Expressing graph problems
The Size≥
k formulae
Fix an enumeration v0, . . . , vn−1 of V.
Variables:
Sk
m at least k variables Cvi with i < m are true
Formulae:
S0
m
¬Sk
0 for k > 0
Cvi → [Sk
i ↔ Sk+1
i+1 ]
¬Cvi → [Sk
i ↔ Sk
i+1]
Sk
n
v0 v1 v2
Cvi 1 0 1
S0
i 1 1 1 1
S1
i 0 1 1 1
S2
i 0 0 0 1
S3
i 0 0 0 0
A similar construction works for Size≤
k .
The Satisfiability Problem
Theorem
3-SAT (satisfiability for formulae in 3-CNF) is NP-complete.
The Satisfiability Problem
Theorem
3-SAT (satisfiability for formulae in 3-CNF) is NP-complete.
Proof
Given Turing machine M and input w, construct formula φ such that
M accepts w iff φ is satisfiable.
Proof
Turing machine M = ⟨Q, Σ, ∆, q0, F+, F−⟩
Q set of states
Σ tape alphabet
∆ set of transitions ⟨p, a, b, m, q⟩ ∈ Q × Σ × Σ × {−1, 0, 1} × Q
q0 initial state
F+ accepting states
F− rejecting states
nondeterministic, runtime bounded by the polynomial r(n)
Proof
Turing machine M = ⟨Q, Σ, ∆, q0, F+, F−⟩
Q set of states
Σ tape alphabet
∆ set of transitions ⟨p, a, b, m, q⟩ ∈ Q × Σ × Σ × {−1, 0, 1} × Q
q0 initial state
F+ accepting states
F− rejecting states
nondeterministic, runtime bounded by the polynomial r(n)
Encoding in PL
St,q state q at time t
Ht,k head in field k at time t
Wt,k,a letter a in field k at time t
φw = ⋀
t<r(n)
[ADMt ∧ INIT ∧ TRANSt ∧ ACC]
Proof
St,q state q at time t
Ht,k head in field k at time t
Wt,k,a letter a in field k at time t
Admissibility formula
ADMt = ⋀
p≠q
[¬St,p ∨ ¬St,q] unique state
∧ ⋀
k≠l
[¬Ht,k ∨ ¬Ht,l] unique head position
∧ ⋀
k
⋀
a≠b
[¬Wt,k,a ∨ ¬Wt,k,b] unique letter
Proof
St,q state q at time t
Ht,k head in field k at time t
Wt,k,a letter a in field k at time t
Initialisation formula for input: a0 . . . an−1
INIT = S0,q0 initial state
∧ H0,0 initial head position
∧ ⋀
k<n
W0,k,ak
∧ ⋀
n≤k≤r(n)
W0,k,◻ initial tape content
Acceptance formula
ACC = ⋁
q∈F+
⋁
t≤r(n)
St,q accepting state
Proof
St,q state q at time t
Ht,k head in field k at time t
Wt,k,a letter a in field k at time t
Transition formula
TRANSt = ⋁
⟨p,a,b,m,q⟩∈∆
⋁
k≤r(n)
[St,p ∧ Ht,k ∧ Wt,k,a ∧
St+1,q ∧ Ht+1,k+m ∧ Wt+1,k,b]
effect of transition
∧ ⋀
k≤r(n)
⋀
a∈Σ
[¬Ht,k ∧ Wt,k,a → Wt+1,k,a]
rest of tape remains unchanged
Proof
TRANSt = ⋁
⟨p,a,b,m,q⟩∈∆
⋁
k≤r(n)
[St,p ∧ Ht,k ∧ Wt,k,a ∧
St+1,q ∧ Ht+1,k+m ∧ Wt+1,k,b] ∧ . . .
Proof
TRANSt = ⋁
⟨p,a,b,m,q⟩∈∆
⋁
k≤r(n)
[St,p ∧ Ht,k ∧ Wt,k,a ∧
St+1,q ∧ Ht+1,k+m ∧ Wt+1,k,b] ∧ . . .
equivalently:
⋀
k≤r(n)
⋀
p∈Q
⋀
a∈Σ
[St,p ∧ Ht,k ∧ Wt,k,a → ⋁
q∈TS(p,a)
St+1,q]
TS(p, a) = {q ∈ Q ⟨p, a, b, m, q⟩ ∈ ∆ }
Proof
TRANSt = ⋁
⟨p,a,b,m,q⟩∈∆
⋁
k≤r(n)
[St,p ∧ Ht,k ∧ Wt,k,a ∧
St+1,q ∧ Ht+1,k+m ∧ Wt+1,k,b] ∧ . . .
equivalently:
⋀
k≤r(n)
⋀
p∈Q
⋀
a∈Σ
[St,p ∧ Ht,k ∧ Wt,k,a → ⋁
q∈TS(p,a)
St+1,q]
∧ ⋀
k≤r(n)
⋀
p,q∈Q
⋀
a∈Σ
[St,p ∧ Ht,k ∧ Wt,k,a ∧ St+1,q → ⋁
m∈TH(p,a,q)
Ht+1,k+m]
TH(p, a, q) = {m ⟨p, a, b, m, q⟩ ∈ ∆ }
Proof
TRANSt = ⋁
⟨p,a,b,m,q⟩∈∆
⋁
k≤r(n)
[St,p ∧ Ht,k ∧ Wt,k,a ∧
St+1,q ∧ Ht+1,k+m ∧ Wt+1,k,b] ∧ . . .
equivalently:
⋀
k≤r(n)
⋀
p∈Q
⋀
a∈Σ
[St,p ∧ Ht,k ∧ Wt,k,a → ⋁
q∈TS(p,a)
St+1,q]
∧ ⋀
k≤r(n)
⋀
p,q∈Q
⋀
a∈Σ
[St,p ∧ Ht,k ∧ Wt,k,a ∧ St+1,q → ⋁
m∈TH(p,a,q)
Ht+1,k+m]
∧ ⋀
k≤r(n)
⋀
p,q∈Q
⋀
a∈Σ
⋀
m∈{−1,0,1}
[St,p ∧ Ht,k ∧ Wt,k,a ∧ St+1,q ∧ Ht+1,k+m →
⋁
b∈TW(p,a,m,q)
Wt+1,k,b]
TW(p, a, m, q) = {b ∈ Q ⟨p, a, b, m, q⟩ ∈ ∆ }
Proof
Properties of φw
▸ It is in CNF.
▸ It has length ∼ r(n)3
.
▸ It is satisfiable if, and only if, the Turing machine accepts w.
Consequently, the satisfiability problem for PL-formulae in CNF is
NP-complete.
Proof
Properties of φw
▸ It is in CNF.
▸ It has length ∼ r(n)3
.
▸ It is satisfiable if, and only if, the Turing machine accepts w.
Consequently, the satisfiability problem for PL-formulae in CNF is
NP-complete.
Reduction to 3-CNF
{L0, L1, L2, . . . , Ln} ↦ {L0, L1, X}, {¬X, L2, . . . , Ln}
(X new variable)
Resolution
Resolution
Resolution Step
The resolvent of two clauses
C = {L, A0, . . . , Am} and C′
= {¬L, B0, . . . , Bn}
is the clause
{A0, . . . , Am, B0, . . . , Bn} .
Lemma
Let C be the resolvent of two clauses in Φ. Then
Φ ⊧ Φ ∪ {C} .
Resolution
Resolution Step
The resolvent of two clauses
C = {L, A0, . . . , Am} and C′
= {¬L, B0, . . . , Bn}
is the clause
{A0, . . . , Am, B0, . . . , Bn} .
(This is the inverse of the splitting trick from the last slide.)
Lemma
Let C be the resolvent of two clauses in Φ. Then
Φ ⊧ Φ ∪ {C} .
The Resolution Method
Observation
If Φ contains the empty clause ∅, then Φ is not satisfiable.
Resolution Method
Input: a set of clauses Φ
Output: true if Φ is satisfiable, false otherwise.
RM(Φ)
add to Φ all possible resolvents
repeat until no new clauses are generated
if ∅ ∈ Φ then
return false
else
return true
Theorem
The resolution method for propositional logic is sound and complete.
Example
{A, C} {B, ¬C} {¬A, B, C} {A, ¬B} {¬A, ¬B, ¬C} {¬B, C}
Example
{A, C} {B, ¬C} {¬A, B, C} {A, ¬B} {¬A, ¬B, ¬C} {¬B, C}
{A, B} {¬A, B} {¬B, ¬C}
{B} {¬B}
∅
Davis-Putnam Algorithm
Input: a set of clauses Φ
Output: true if Φ is satisfiable, false otherwise.
DP(Φ)
remove all tautological clauses from Φ
if Φ = ∅ then
return true
if Φ = {∅} then
return false
select a variable X
add to Φ all resolvents over X
remove all clauses containing X or ¬X from Φ
repeat
Example
{A, C} {B, ¬C} {¬A, B, C} {A, ¬B} {¬A, ¬B, ¬C} {¬B, C}
Example
{A, C} {B, ¬C} {¬A, B, C} {A, ¬B} {¬A, ¬B, ¬C} {¬B, C}
select A: {B, C} {¬B, C, ¬C} {B, ¬B, C} {¬B, ¬C}
Example
{A, C} {B, ¬C} {¬A, B, C} {A, ¬B} {¬A, ¬B, ¬C} {¬B, C}
select A: {B, C} {¬B, C, ¬C} {B, ¬B, C} {¬B, ¬C}
removals: {B, ¬C} {¬B, C} {B, C} {¬B, ¬C}
Example
{A, C} {B, ¬C} {¬A, B, C} {A, ¬B} {¬A, ¬B, ¬C} {¬B, C}
select A: {B, C} {¬B, C, ¬C} {B, ¬B, C} {¬B, ¬C}
removals: {B, ¬C} {¬B, C} {B, C} {¬B, ¬C}
select B: {C, ¬C} {¬C} {C} {C, ¬C}
Example
{A, C} {B, ¬C} {¬A, B, C} {A, ¬B} {¬A, ¬B, ¬C} {¬B, C}
select A: {B, C} {¬B, C, ¬C} {B, ¬B, C} {¬B, ¬C}
removals: {B, ¬C} {¬B, C} {B, C} {¬B, ¬C}
select B: {C, ¬C} {¬C} {C} {C, ¬C}
removals: {¬C} {C}
Example
{A, C} {B, ¬C} {¬A, B, C} {A, ¬B} {¬A, ¬B, ¬C} {¬B, C}
select A: {B, C} {¬B, C, ¬C} {B, ¬B, C} {¬B, ¬C}
removals: {B, ¬C} {¬B, C} {B, C} {¬B, ¬C}
select B: {C, ¬C} {¬C} {C} {C, ¬C}
removals: {¬C} {C}
select C: ∅
Horn formulae
Linear Resolution
A linear resolution is a sequence of resolution steps where in each
step the resolvent of the previous step is used.
{¬A, ¬B} {A, ¬C} {B, ¬C, ¬D} {C, ¬D} {D}
{¬B, ¬C}
{¬C, ¬D}
{¬D}
∅
Horn formulae and linear resolution
Horn formulae
A Horn clause is a clause C that contains at most one positive literal.
Example
A0 ∧ ⋅⋅⋅ ∧ An → B ≡ {¬A0, . . . , ¬An, B}
Horn formulae and linear resolution
Horn formulae
A Horn clause is a clause C that contains at most one positive literal.
Example
A0 ∧ ⋅⋅⋅ ∧ An → B ≡ {¬A0, . . . , ¬An, B}
Theorem
A set of Horn clauses is unsatisfiable if, and only if, one can use linear
resolution to derive the empty clause from it.
SLD Resolution
Linear resolution where the clauses are sequences instead of sets and
we always resolve the leftmost literal of the current clause.
Minimal models
Lemma
Every satisfiable set of Horn-formulae has a minimal model.
Minimal models
Lemma
Every satisfiable set of Horn-formulae has a minimal model.
Algorithm to compute it:
Input: Φ set of Horn-formulae
T = ∅
repeat
for all A0 ∧ ⋅⋅⋅ ∧ An−1 → B ∈ Φ do
if A0, . . . , An−1 ∈ T then
T = T ∪ {B}
until T does not change anymore
Minimal models
Lemma
Every satisfiable set of Horn-formulae has a minimal model.
Algorithm to compute it:
Input: Φ set of Horn-formulae
T = ∅
repeat
for all A0 ∧ ⋅⋅⋅ ∧ An−1 → B ∈ Φ do
if A0, . . . , An−1 ∈ T then
T = T ∪ {B}
until T does not change anymore
Theorem
Satisfiability for sets of Horn-formulae can be checked in linear time.
Example
B ∧ C → A A ∧ D → B F → C E → D
D ∧ E → A C ∧ F → B 1 → F
Example
B ∧ C → A A ∧ D → B F → C E → D
D ∧ E → A C ∧ F → B 1 → F
Example
B ∧ C → A A ∧ D → B F → C E → D
D ∧ E → A C ∧ F → B 1 → F
Example
B ∧ C → A A ∧ D → B F → C E → D
D ∧ E → A C ∧ F → B 1 → F
Example
B ∧ C → A A ∧ D → B F → C E → D
D ∧ E → A C ∧ F → B 1 → F
Finite Games G = ⟨V , V◻, E⟩
Players and ◻
◻
◻ ◻
◻ ◻
◻
Winning regions: W , W◻
Finite Games G = ⟨V , V◻, E⟩
Players and ◻
◻
◻ ◻
◻ ◻
◻
Winning regions: W , W◻
Reduction
positions
V = variables ⟨A⟩ and V◻ = formulae [A0 ∧ ⋅⋅⋅ ∧ An−1 → B]
edges
⟨B⟩ → [A0 ∧ ⋅⋅⋅ ∧ An−1 → B]
[A0 ∧ ⋅⋅⋅ ∧ An−1 → B] → ⟨Ai⟩
Lemma
A variable A belongs to W iff it is true in the minimal model.
B ∧ C → A A ∧ D → B F → C
D ∧ E → A C ∧ F → B 1 → F
⟨F⟩
[F → C]
[C ∧ F → B]
⟨C⟩
⟨B⟩
[B ∧ C → A]
[A ∧ D → B]
⟨A⟩
⟨D⟩
[D ∧ E → A] ⟨E⟩
[ → F]
Simple Algorithm
Win(v, σ)
if v ∈ Vσ then
if there is an edge v → u with Win(u, σ) then
return true
else
return false
if v ∈ Vσ then (* = ◻ ◻ = *)
if for every edge v → u we have Win(u, σ) then
return true
else
return false
Linear Algorithm
Input: game ⟨V , V◻, E⟩
forall v ∈ V do
win[v] = (* winner of the position *)
P[v] = ∅ (* set of predecessors of v *)
n[v] = 0 (* number of successors of v *)
end
forall ⟨u, v⟩ ∈ E do
P[v] = P[v] ∪ {u}
n[u] = n[u] + 1
end
forall v ∈ V do
if n[v] = 0 then Propagate(v, ◻)
forall v ∈ V◻ do
if n[v] = 0 then Propagate(v, )
return win
procedure Propagate(v, σ) =
if win[v] ≠ then return
win[v] = σ
forall u ∈ P[v] do
n[u] = n[u] − 1
if u ∈ Vσ or n[u] = 0 then Propagate(u, σ)
end
end