IA085: Satisfiability and Automated Reasoning
Seminar 2
Exercise 1 Finish the exercises from the previous seminar.
Exercise 2 Using the resolution method, prove that the following sets of
clauses are not satisfiable.
1. {{A, B}, {¬A, B, C}, {C, ¬D, ¬E}, {A, D}, {¬B, D}, {¬C, D}, {¬D, E}, {¬D, ¬E}}
2. {{¬B, ¬C, D}, {¬B, C, D}, {B, E}, {B, ¬E}, {¬A, C, ¬D}, {¬C, ¬D}, {A, ¬D}}
Exercise 3 Using the resolution method, prove that the following propositional
entailments hold.
1. (A → C) ∧ (B → C) ∧ (A ∨ B) |= C
2. (A → B) ∧ (A → C) ∧ A |= B ∧ C
3. (A → (B ∨ C)) ∧ ¬B |= A → C
Exercise 4 Consider a cdcl-based sat solver in the following state:
• trail: [A, ¬B, C, D, E, ¬F, ¬H, I, J]
• decisions: [A, C, E]
• antecedent clauses:
– reason[¬B] = {¬A, ¬B}
– reason[D] = {B, ¬C, D}
– reason[¬F] = {¬D, ¬E, ¬F}
– reason[¬H] = {F, ¬H}
– reason[I] = {¬A, H, I}
– reason[J] = {B, H, J}
In this state, the clause {¬A, F, H, ¬J} was found to be conflicting. Perform
conflict analysis and compute the learnt conflict clause using the first uip
criterion. To what decision level should the solver backjump after learning
the clause?
Exercise 5 Consider the following list of requirements between packages:
• package X requires packages Y and Z1
• package Y requires package A or package B or package Z2
• package Z1 requires package A
• package A requires packages C and D
2
• package C requires package E or package F
• package D requires package F or package Z1
• packages Z1 and Z2 are not compatible
Use PySAT and write these constraints on installed packages as a formula.
Write a script that finds a model of the formula in which the package X is
installed.
Finally, implement a script that computes a model of the formula in which
the package X is installed and that is minimal with respect to inclusion of Hint: Call the solver multiple times with
added constraints. Try to find a smaller
model than the current one.
installed packages (i.e., a model from which no package can be removed).
Bonus: Find a model in which the package X is installed and that has
the minimal number of installed packages.