Exercise � Consider the following formulae.
(a) (A ↔ B) → (¬A∧ C)
(b) (A → B) → C
(c) A ↔ B
(d) (A → B) ↔ (A → C)
(e) (A∧ B) ∨ (A∧ C)
(f) [A → (B∨ ¬A)] → (B → A)
(g) [(A∨ B) → (C → A)] ↔ (A∨ B∨ C)
For each of them
(�) use a truth table to determine if the formula is valid and/or satisfiable;
(�) convert the formula into CNF using the truth table;
(�) convert the formula into CNF using equivalence transformations instead;
(�) write the formula as a set of clauses.
Exercise � Which of the following formulae imply each other?
(a) A∧ B
(b) A∨ B
(c) A → B
(d) A ↔ B
(e) ¬A∧ ¬B
(f) ¬A
(g) ¬(A → B)
Exercise � Encode the following problems as a satisfiability problem for propositional logic:
(a) the independent set problem: given a graph G and a number k, does the graph contain k
vertices which are pairwise not connected by an edge to each other?
(b) the domino tiling problem: given a finite set Dof square dominoes,two relations H,V ⊆ D×D
specifying which pairs of dominoes can be put horizontally/vertically next to each other, and
a number n, does there exist a tiling of the n× n grid, i.e., a function τ n× n → D such that
(τ(i,j),τ(i + 1,j)) ∈ H and (τ(i,j),τ(i,j + 1)) ∈ V , for all i,j?
�
Exercise � We can encode n-bit numbers via an n-tuple of propositional variables An−1,...,A0.
(a) Write a formula φ(A1,A0, B1,B0, C2,C1,C0) for the addition of 2-bit numbers (A+B = C).
(b) Write a formula φ(An−1,...,A0, Bn−1,...,B0, Cn,...,C0) for the addition of n-bit num-
bers.
Exercise � Use the DPLL algorithm to determine whether the following formulae are satisfiable.
(a) ¬[(A → B) ↔ (A → C)]
(b) (A∨ B∨ C) ∧ (B∨ D) ∧ (A → D) ∧ (B → A)
(c) (A ↔ B) → (¬A∧ C)
(d) [A → (B∨ ¬A)] → (B → A)
(e) [(A∨ B) → (C → A)] ↔ (A∨ B∨ C)
Exercise � Use the resolution method to determine which of the following formulae are valid.
(a) (A∧ ¬B∧ C) ∨ (¬A∧ ¬B∧ ¬C) ∨ (B∧ C) ∨ (A∧ ¬C) ∨ (¬A∧ B∧ ¬C) ∨ (¬A∧ ¬B∧ C)
(b) (A∧ B) ∨ (B∧ C ∧ D) ∨ (¬A∧ B) ∨ (¬C ∧ ¬D)
(c) (¬A∧ B∧ ¬C) ∨ (¬B∧ ¬C ∧ D) ∨ (¬C ∧ ¬D) ∨ (A∧ B) ∨ (¬A∧ B∧ C) ∨ (¬A∧ C)
∨ (A∧ ¬B∧ C) ∨ (A∧ ¬B∧ D)
Exercise � Construct the game for the following set of Horn-formulae and determine the winning
regions.
B∧ C ∧ D → A C ∧ F → B A∧ F → C D → B A∧ B → F
E → A D ∧ E → B C D
Exercise � (optional) Given a finite automaton A and an input word w, write down a formula φA,w
that is satisfiable if, and only if, the automaton A accepts w.
�