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).