Academic Year:
Class Test Period: Module Code:
Class Test Paper Title: Duration:
2020/2021
Spring
CMT215
Automated Reasoning 2 hours and 30 minutes
Do not turn this page over until instructed to do so by the Invigilation Supervisor
Please read the following information carefully: Structure of Class Test Paper:
• There are 5 pages including this page.
• There are 8 questions in total.
• There are no appendices.
• The maximum mark for the class test paper is 50 and the mark obtainable for a question or part of a question is shown in brackets alongside the question.
Instructions for completing the class test:
• Answer ALL questions.
CMT215
Q1. Let ↵ and KB be given as follows. ↵ = p^¬s
KB = {t_p_s,s_¬t,¬s_r_q,¬q,¬r_¬s}
Prove whether KB entails ↵, or not. The proof should be given by using unit resolution, full resolution, or both. Factoring (i.e., removing multiple copies of literals) may be used if necessary. [4]
Q2. The DPLL (Davis-Putnam-Logemann-Loveland) algorithm shown below im- plements three truth-assignment rules: pure literal (or symbol) heuristic, unit clause heuristic, and case analysis. Let clauses and symbols be given as fol- lows.
clauses = {q_¬r,¬p_¬r,p_s_¬r,¬s,p_¬s,¬p_s_r,q_¬p} symbols = [s, r, q, p]
Explain DPLL(clauses, symbols, ;). The explanation should include the pro- cess of which rule is adopted, and as a result, which truth value is assigned, for each propositional symbol.
function DPLL-SATISFIABLE?(s) returns true or false inputs: s, a sentence in propositional logic
clauses the set of clauses in the CNF representation of s symbols a list of the proposition symbols in s
return DPLL(clauses, symbols, 😉
function DPLL(clauses, symbols, model) returns true or false
if every clause in clauses is true in model then return true
if some clause in clauses is false in model then return false
P , value FIND-PURE-SYMBOL(symbols, clauses, model)
if P is non-null then return DPLL(clauses, symbols P , model[{P = value}) P, value FIND-UNIT-CLAUSE(clauses, model)
if P is non-null then return DPLL(clauses, symbols P , model[{P = value}) P FIRST(symbols); rest REST(symbols)
return DPLL(clauses, rest, model [ {P = true}) or
DPLL(clauses, rest, model [ {P = f alse})
2
[6]
Q3. Answer all of the following questions regarding CDCL (conflict-driven clause learning).
(a) What is clause learning? Explain your answer in one or two sentences.[1]
(b) What is backjumping? Explain your answer in one or two sentences. [1]
(c) Let clauses and symbols be given as follows.
clauses = {¬p_¬r_s,p_r_s,¬p_¬q,r_s,q_¬s_t,q_¬s_¬t} symbols = [p, q, r, s, t]
Draw the implication graph from the application of the DPLL algorithm. The implication graph should continue until it demonstrates a conflict. [3]
(d) Obtain the learnt clause from a cut of the implication graph. The cut should be expressed by drawing a line splitting the implication graph into a reason side and conflict side. [2]
(e) Obtain the learnt clause from another cut of the implication graph. Again, the cut should be expressed by drawing a line splitting the implication graph into a reason side and conflict side. [2]
Derive a sentence in a CNF (conjunctive normal form) by applying Tseitin transformation to the following propositional sentence.
(¬(p _ r)) $ (q ^ r)
[6]
(b) Let X be a propositional sentence and Y be a sentence in a CNF derived from X by Tseitin transformation. Which of the following statement is true?
(A) X and Y are logically equivalent.
(B) X is satisfiable if and only if Y is satisfiable.
(C) X entails Y .
(D) X and Y are not semantically related. [3]
Q5. Determine the stable models of the following normal logic programs (Justify your answers in terms of the reduct P X ):
(a)P1:a b,c. a ⇠b. b ⇠d. c a,b. d a,⇠c. [3] (b)P2:a d,⇠b. b a. b d,⇠c. c ⇠a,⇠b. d a,b. d ⇠c. [3]
Q4. (a)
3 PLEASE TURN OVER
CMT215
CMT215
Q6. A vertex cover of a graph is a set of vertices such that every edge of the graph has at least one endpoint in that set. We would like to find a vertex cover of size n, if it exists. The following rules represent the graph with 6 vertex, a, b, c, d, e, d and the 9 edges:
vertex(a; b; c; d; e; f).
edge(a,b; b,c; c,a; d,f; f,e; e,d; a,d; f,c; b,e).
And the following rule encodes that a cover is a subset of vertices of size n
{cover(X) : vertex(X)} = n.
Add rules and possible constraints to the logic program, such that the following is achieved
(a) covered/2 is the set of edges that have an endpoint in cover/1 [3] (b) Every edge of the graph is covered. [3]
Q7. (a) Transform the following first-order formula into a CNF.
8x [8y P roblem(y) ! Solves(x, y)] ! [8y Respects(y, x)]
(Everyone who solves all problems is respected by everyone.)
[3]
(b) Let KB be given as follows.
KB = {¬Loves(x,F(x))_Loves(G(x),x), ¬Animal(x) _ Loves(Jack, x),
Animal(F (x)) _ Loves(G(z), x)}
Prove by resolution whether KB entails Loves(y, Jack), or not. The proof should specify all the unifiers used in the resolution. Factoring (i.e., re- moving multiple copies of literals) and standardizing apart (i.e., renaming variables to avoid name clashes) may be used if necessary. [4]
4
Q8. Select all correct statement(s) from the choices given and write the letter(s) corresponding to this choice (A,B,C,D) as your answer in the answer book.
(A) Careless misuse of automated reasoning systems can result in biased de- cision making.
(B) There is no way to mitigate decision making biases caused by automated reasoning systems.
(C) Biases caused by automated reasoning systems are avoided if the knowl- edge fed into the systems is based on data collected from the real world.
(D) Automated reasoning systems should not be applied to domains involving ethical and moral issues such as political, medical and legal domains. [3]
5X END OF CLASS TEST
CMT215