Applied Logic for Computer Science Assignment 3

Department of Computer Science
CS 2209A — Applied Logic for Computer Science
Assignment 3

1. With the First Order Logic sentences given by Γ show Γ ` ∃xHate(x, Caesar) using resolution.
Your answer must include each of the required steps to accomplish this proof. In the sentences
below, predicates and constants start with an upper case letter and variables are lower case
letters.
Γ =



Man(Marcus)
Roman(Marcus)
∀x(Man(x) → Person(x))
Ruler(Caesar)
∀x(Roman(x) → (Loyal(x, Caesar) ∨ Hate(x, Caesar)))
∀x∃yLoyal(x, y)
∀x∀y((Person(x) ∧ Ruler(y) ∧ Tryassasin(x, y)) → ¬Loyal(x, y))
Tryassasin(Marcus, Caesar)



When performing the resolution step, use the following demonstration format:
1. clause Given
.
.
.
k. clause Given
k+1. clause line number, line number, unifier (+ standardize variables apart)
.
.
.
n. empty line number, line number, unifier (+ standardize variables apart)
2. Given the following set of clauses, the implication graph that is generated by the DPLL
algorithm with unit propagation, and the cut provided, give the learned clause generated by
Conflict Directed Clause Learning and the backjump by stating the variable to backjump to.
The notation in the graph is slightly different than what was used in the notes: w1 . . . w6 label
the clauses below and on the graph, x1 . . . x9 are the propositional variables, each node in the
implication graph has the following format: “propositional variable = truth value @ decision
level in the tree”. The truth values are 0 for False, 1 for True. Any variables that have been
given truth values because they are unit variables will have the same “decision level” as the
variable that is a decision node.
w1 = (x1 ∨ x2)
w2 = (x1 ∨ x3 ∨ x7)
w3 = (¬x2 ∨ ¬x3 ∨ x4)
w4 = (¬x4 ∨ x5 ∨ x8)
w5 = (¬x4 ∨ x6 ∨ x9)
w6 = (¬x5 ∨ ¬x6)
Once the cut is decided upon the question of how to derive the conflict
clause from the bipartioned I-Graph remains to be answered.
Deriving the Conflict Clause The conflict clause consists of all nodes,
belonging to the reason side, that have edges leading into the conflict side.
The variables represented by these nodes, in our example x4, x8, x9 have to
be negated in the conflict clause according to their current assignment, since
the conflict clause should be made false by, and thus exclude, an assignment
leading to the conflict. Therefore in our example above the derived conflict
clause C would be:
Conflict Clause: C = (¬ x4 ∨ x8 ∨ x9)
The updated database of clauses would be:
w1 = (x1 ∨ x2)
w2 = (x1 ∨ x3 ∨ x7)
w3 = (¬ x2 ∨ ¬ x3 ∨ x4)
w4 = (¬ x4 ∨ x5 ∨ x8)
7
3. Given the representation of the 2-Queens problem given in class (and reproduced below in
a slightly different form), produce the search tree produced by DPLL with unit propagation
to show whether the propositional formula is satisfiable or unsatisfiable. You must provide
enough annotation to show how this tree is produced. Suggested annotation: (follow the
annotation style in the lecture slides): show in the tree the valuation given for each decision
node (give the valuation on the left and right branch); provide the unit propagation values for
unit variables beside the tree branch; show whether the tree can be expanded on the branch
or whether it leads to a conflict (i.e., a failure, mark it with an X); list the clauses in the
CNF form of the original formula and indicate which clauses are made true by the current
valuation or made false by the current valuation (annotate appropriately, you will probably
need two columns for each decision node, one for the left branch and one for the right branch).
(a ∨ b)
(¬a ∨ ¬b)
(c ∨ d)
(¬c ∨ ¬d)
(a ∨ d)
(¬a ∨ ¬d)
(b ∨ c)
(¬b ∨ ¬c)
(¬a ∨ ¬c)
(¬b ∨ ¬d)
4. Give the propositional formula that models the 3-Queens problem. Take this propositional
formula, convert it to CNF (provide this a part of your answer) and give it as input to the
SAT solver that you have installed on your computer. (If you don’t have a computer tell me.)
What is the answer given by the SAT solver? In addition to the items above, also submit
the file containing the CNF version of the propositional formula and a screen shot of your
Python run.
2