IA085: Satisfiability and Automated Reasoning
Seminar 1
Exercise 1 Which of the following formulas are satisfiable? If the formula is
satisfiable, find its model, if it is unsatisfiable, explain why.
1. (A → B) ∧ (B ∧ C → ¬A) ∧ (¬C ↔ A)
2. (A ∨ B) ∧ (¬A ∨ C) ∧ (¬C ∨ ¬A) ∧ (¬C ∨ ¬B) ∧ (¬B ∨ C)
3. (A ∧ B ∧ ¬C ∧ ¬D) ∨ (¬A ∧ B ∧ ¬C ∧ D) ∨ (¬A ∧ ¬B ∧ ¬C ∧ D) ∨
(¬A ∧ B ∧ C ∧ ¬D) ∨ (A ∧ ¬B ∧ ¬C ∧ ¬D)
Exercise 2 Which of the following logical entailments hold? If the entailment
holds, explain why, if it does not, find a counterexample.
1. (A → B) ∧ ¬B |= ¬A
2. (A → B) ∧ A ∧ ¬B |= C ∧ ¬C
3. (A ∨ ¬B ∨ C) ∧ (¬A ∨ ¬B ∨ C) ∧ (¬A ∨ B ∨ C) ∧ (¬A ∨ ¬B ∨ ¬C) |=
¬(A ∧ B)
4. (A → (B ∨ C)) ∧ (A ∨ B) ∧ (¬B → C) |= B
Exercise 3 Convert the following formulas to the conjunctive normal form
using Tseitin transformation.
1. ¬(A ∧ B) ∨ (B ∧ C ∧ D) ∨ ¬A
2. ¬(A ∨ (B → C)) ∧ (A ↔ (B → C))
Exercise 4 Let a0,a1,a2, b0,b1,b2 be Boolean variables that represent bits of
three-bit numbers a = a2a1a0 and b = b2b1b0. Consider the standard addition
operation + on binary numbers that throws away the potential overflow
bit (i.e., + is addition modulo 23). Write a formula that is satisfiable if and
only if the sum of the two numbers is five, i.e.,
a2a1a0 + b2b1b0 = 101.
Hint: introduce new auxiliary variables.
Exercise 5 Install PySAT library and run the following Python script.
from pysat.solvers import Solver
with Solver() as s:
s.add_clause([-1, 2])
s.add_clause([-2, 3])
print(s.solve())
print(s.get_model())
ia085: satisfiability and automated reasoning 2
Exercise 6 Using PySAT, write a program that gets a number n as a command
line argument and solves the n queens problem. Text output of the
positions in the solution is fine, but if you are feeling fancy, draw the resulting
chess board in the terminal.
Bonus: If you have spare time, you can try out and compare different
encodings of the at-most-one constraint1. 1
https://
manuscriptlink-society-file.
s3-ap-northeast-1.amazonaws.
com/kism/conference/sma2020/
presentation/SMA-2020_paper_77.pdf
Exercise 7 Modify the script from Exercise 5 so that the input formula
is a CNF encoding of the formula you designed in Exercise 4. Modify the
script so that it prints out not one model of the formula, but two different
models.
Modify the script so that it prints out all models of the formula.