Introduction to AI: Tutorial 3
SAT solving using DP and DLL algorithms
Alessandra Russo
(with thanks to Krysia Broda)
This tutorial includes questions on Satisfiability for you to practice using the DP and
the DLL algorithms to check whether given sets of clauses are satisfiable or not.
Question 1
Consider the following set of clauses:
S = {{x1, x2}, {x4,¬x2}, {¬x5,¬x4}, {x3,¬x4}, {x5,¬x3}, {¬x1, x4, x6}, {¬x6}}
• List which literals are pure literals (if any) in S and which are unit clauses
• Use resolution to show that S is unsatisfiable.
• Apply now the improved DP algorithm, given in slide 14 of Unit 5, making use
of pure literals and unit propagation where possible. Annotate each step of the
derivation.
Question 2
Consider the following set S of clauses
S = {{x3, x4,¬x1, x5}, {¬x3, x4, x5}, {x3,¬x4,¬x1}{x1, x2}{x1,¬x2}{¬x1,¬x5}, {¬x3,¬x4, x5}}
Use the DLL (from slide 20 of Unit5) to check whetherS is satisfiable or not. Select
branching literals in the order x1, x2, x3, ….
Question 3
Consider the following problem
I would like to organise a dinner reunion and I do not want any two of
my close friends (Tom, Sam, John and Bob) to be uninvited.
But I cannot invite both Sam and John, and
if I invite Tom I must invite John.
• Formalise the above problem in propositional logic.
• Use the DLL algorithm to see whether the above problem is satisfiable or not.
If it is provide a suggestion of people to invite.
Introduction to AI: Tutorial 3 2
Question 4
Consider the following set S of clauses:
S = {{A,B,¬D}, {D,B,A}, {C,E,¬A}, {¬E,F,¬A}, {F,¬C,E}}
• How many pure literals are in the set S of clauses?
• If the next atom chosen for splitting is A, how many clauses are left in the A
and in the ¬A branches, after applying subsumption?
• Use DLL to see whether S is Satisfiable. If it is, return a model that makes it
true.
Question 5
Use the DLL procedure to show the unsatisfiability of each of the following sets of
clauses
1. S = {{¬A,¬B,C}, {D,E}, {¬C,¬E,F}, {D,¬F}, {A}, {B}, {¬D}}
2. S = {{A,B,C}, {A,¬B,C}, {¬A,¬B,¬C}, {A,B,¬C}, {¬A,B,¬C},
{¬A,¬B,C}, {A,¬B,¬C}, {¬A,B,C}}
Alessandra Russo Tutorial 2: SAT: DP and DLL solvers