COMP4418 – Assignment 2

COMP4418 – Assignment 2

Worth: 15 %
This assignment consists of seven questions.
1. [15 Marks] (Answer Set Programming)
A clique of a graph is a set of vertices C that are pairwise adjacent. That is, for a graph with vertex
set V and set of undirected edges E ⊆ {{x, y} | x, y ∈ V }, a clique is a set C ⊆ V such that for all
x ∈ C and y ∈ C, if x 6= y, then {x, y} ∈ E. A k-clique is a clique C of size k, that is, |C| = k.
(a) Write an ASP program that decides the k-Clique problem:
Input: a graph with vertices V and edges E ⊆ V × V , and a natural number k ≥ 0.
Problem: decide if there is a k-clique.
Assume the input parameters V , E, k are encoded in ASP in the form of a unary predicate
v, a binary predicate e, and a constant symbol k, respectively. Use a unary predicate c to
represent the clique C. Your program should have no more than two rules.
(b) Use an ASP solver1
to determine how many k-cliques the following graph has for every k ∈
{3, 4, 5, 6}.
Hint: the number of 2-cliques is 11.
1 2
3
4
5
6
2. [15 Marks] (Answer Set Programming)
Consider the following logic program P.
a ← not b, not c.
b ← not a, not c.
c ← not a, not b.
d ← a.
d ← b.
d ← c.
Determine stable models of this program. For every candidate interpretation S, specify the reduct
P
S. Give your solution in a table of exactly (!) the following form and order:
1For instance, you can download the Clingo ASP solver from https://potassco.org/ and run your program with clingo
--const k=k -n 0 clique.lp or ./clingo --const k=k -n 0 clique.lp where k ∈ N is the size of the clique.
1
S Reduct P
S Stable model?
{a, b, c, d} d ← a. d ← b. d ← c. ✗
{a, b, c}
{a, b, d}
{a, c, d}
{b, c, d}
{a, b}
{a, c}
{a, d}
{b, c}
{b, d}
{c, d}
{a}
{b}
{c}
{d}
{}
2
3. [5 Marks] (Satisfiability)
Download the following material from the course website:
• Lectures → Week 6 & 7 → sat-naive.cc (implements Algorithm 1)
• Lectures → Week 6 & 7 → sat-up.cc (implements Algorithm 2)
• Lectures → Week 6 & 7 → sat-cdcl.cc (implements Algorithm 3)
• Assignments → sudoku.cnf (CNF encoding of a Sudoku game)
On the CSE machines, you can compile the files by running the following commands:
$ c++ -std=c++11 -O3 -DNDEBUG -o sat-naive sat-naive.cc
$ c++ -std=c++11 -O3 -DNDEBUG -o sat-up sat-up.cc
$ c++ -std=c++11 -O3 -DNDEBUG -o sat-cdcl sat-cdcl.cc
This will create three executable files: sat-naive, sat-up, sat-cdcl. Use them to solve the Sudoku
instance sudoku.cnf:
$ ./sat-naive sudoku.cnf
$ ./sat-up sudoku.cnf
$ ./sat-cdcl sudoku.cnf
(If the solver does not report a result after 5 minutes, you can terminate the process.)
(a) What are the run times reported by the individual solvers?
(b) Briefly explain why the run times differ (two or three sentences).
4. [18 Marks] (Satisfiability)
State for each of the following statements whether it is true. Briefly explain your answer in one or
two sentences.
(a) Converting a propositional formula into an equisatisfiable CNF formula in the worst case
requires exponential time (under the assumption P 6= NP).
(b) There are decision problems that cannot be reduced to SAT (if so, name a concrete problem).
(c) If I is closed under unit propagation relative to φ, then in order to close I ∪ {x} under unit
propagation relative to φ it suffices to inspect the clauses c ∈ φ that watch ¯x.
5. [15 Marks] (Satisfiability)
Consider the CNF formula φ
(p ∨ q ∨ r ∨ s) ∧ (p ∨ q¯∨ t¯) ∧ (p ∨ t)
and the partial interpretation I = {p¯}. Close I under unit propagation relative to φ using the
watched-literal scheme. Initially, the clauses shall be watching the following literals:
• p ∨ q ∨ r ∨ s watches p and q,
• p ∨ q¯∨ t¯ watches p and ¯q,
• p ∨ t watches p and t.
Use a table of the following form to show how I and the watched literals evolve. In each row, use
the cell below a clause to list the literals currently watched by the clause, and when a new literal
is derived by unit propagation, add it to the next free cell in the first column.
3
I
Clauses and Watched Literals
p ∨ q ∨ r ∨ s p ∨ q¯∨ t p ¯ ∨ t
p, q p, q p, t ¯
p¯
Hint: the closure of {p¯} under unit propagation relative to φ is {p, ¯ q, t ¯ }, so a table with three rows
like the one below should suffice.
6. [12 Marks] (Reasoning about Knowledge)
For each of the the following statements, prove whether it is valid, or not valid but satisfiable, or
unsatisfiable. That is, to prove that φ is valid, you need to show that all interpretations e, w satisfy
φ; to prove that φ is satisfiable, you need to show that some interpretation e, w satisfies φ; to prove
that φ is unsatisfiable, you need to prove that no interpretation e, w satisfies φ.
For instance, one way to prove validity of (Kφ ∧ K(φ → ψ)) → Kψ is as follows: Let e, w be an
arbitrary interpretation. Suppose e, w |= Kφ ∧ K(φ → ψ); we need to show e, w |= Kψ. Then for
all e, w |= Kφ and e, w |= K(φ → ψ). The former means that for all w
0 ∈ e, e, w0
|= φ; the latter
means that for all w
0 ∈ e, e, w0
|= (φ → ψ). Therefore for all w
0 ∈ e, e, w0
|= φ and e, w0
|= (φ → ψ),
and therefore e, w0
|= ψ. Thus for all w
0 ∈ e, e, w0
|= ψ. Hence e, w |= Kψ.
(a) KHappy ∧ K¬Happy
(b) K(Happy ∨ Sad) → ¬KHappy
You may abbreviate the propositions by their first letters.
7. [20 Marks] (Reasoning about Action & Change)
In the blocks world a robot is stacking blocks on a table. We formalised this scenario using STRIPS
in the lecture. Here, your task is to represent the actions and their effects from the blocks world
using the Logic of Actions. For this purpose you should familiarise yourself with the actions and
propositions in the STRIPS model first.
The limitations of STRIPS required us to introduce some redundancies in the STRIPS model.
When translating the STRIPS model to the Logic of Actions, some of these redundancies can be
avoided. For example, we can simplify the actions in the following way.
• The action pickUp(x) replaces the STRIPS action pickUp(x, y) because we can figure out in
the successor-state axiom on which table or block y the block x is.
• The action putOn(y) replaces the STRIPS action putOn(x, y) because we can figure out in
the successor-state axiom which block x the robot is holding.
• The action putOnTable replaces the STRIPS action putOnTable(x) because we can figure out
in the successor-state axiom which x the robot is holding.
4
With these simplified actions, we can capture the behaviour of the predicate On(x, y) with the
following successor-state axiom:
∀a∀x∀y

[a]On(x, y) ↔

Holding(x) ∧ (a = putOn(y) ∨ (y = T ∧ a = putOnTable))

∨

On(x, y) ∧ a 6= pickUp(x)



.
(a) Similarly to the successor-state axiom given above, provide a successor-state axiom for the
predicate Holding(x) that captures the meaning of Holding(x) from the STRIPS model. That
is, your successor-state axiom should capture the effects of actions like pickUp(y) and putOn(y)
on which x the robot is holding.
(b) Show that after picking up B and putting it on C, B is on C, using regression. That is, regress
the formula
[pickUp(B)][putOn(C)]On(B, C)
and prove that the resulting formual is valid.
Please make sure that your solution is readable. Show intermediate steps. To keep the presentation concise, you can abbreviate Holding(x) by H(x), pickUp(x) by pu(x), putOn(x)
by po(x), and putOnTable(x) by pot(x). Moreover, you may make simplifying steps when
subformulas are obviously false/true; for instance, for the formula
H(C) ∧ (po(C) = po(C) ∨ (C = T ∧ po(C) = pot))
it is immediate that C = T ∧ po(C) = pot is trivially false, whereas po(C) = po(C) is trivially
true, so the whole formula can be simplified to H(C).
(c) The STRIPS formalisation mentions the proposition schema Clear(x). Is such a predicate also
needed when using the Logic of Action to model the blocks world, or is it redundant? Explain
your answer. If Clear(x) is redundant, provide a formula that expresses its meaning using the
predicates On(x, y) and/or Holding(x).
Submission
You will need to answer the questions in a file named assn2.pdf Submit using the command:
give cs4418 assn2 assn2.pdf
The deadline for this submission is 14:59:59pm 01 October.
Late Submissions
In case of late submissions, the maximum available mark is reduced by 10 points for each day late.
No extensions will be given for the assignment (except in case of illness or misadventure).