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  We can encode n-bit numbers via an n-tuple of propositional variables An−, . . . , A.
(a) Write a formula φ(A, A, B, B, C, C, C) for the addition of -bit numbers ( ¯A + ¯B = ¯C).
(b) Write a formula φ(An−, . . . , A, Bn−, . . . , B, Cn, . . . , C) for the addition of n-bit numbers.

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  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.
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
