Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

Computational Thinking 2023/24

Logic Coursework

You should submit a single ZIP file containing (i) one PDF document containing your answers to all the theoretical/mathematical questions, and (ii) a single Python file with your code. Please name the Python file according to your username (e.g. mpll19.py).

The coding part of the coursework will be to write a SAT-solver in Python.  Note that you will be restricted in some of your choices for data structures and function names.  The data structure for a literal will be an integer, where a negative integer indicates the negation of the variable denoted by the corresponding positive integer.  The data structure for partial assignment should be a list of literals. The data structure for a clause set should be a list of lists of literals.

1. Answer the following questions about complete sets of logical connectives, in each case justify- ing your answer. [12 marks]

(i). Show {¬, ∧} is a complete set of connectives. [3 marks.]

(ii). Show {→ , XOR} is a complete set of connectives. [3 marks.]

(ii). Is {NOR, ∨} a complete set of connectives? [3 marks.]

(iv). Is {∧, ∨} a complete set of connectives? [3 marks.]

2. Convert ((p → q) → (r → s)) → t) to

(i). Conjunctive Normal Form (CNF) [4 marks.]

(ii). Disjunctive Normal Form (DNF) [4 marks.] [8 marks]

3. What is the purpose of Tseitin’s Algorithm? Apply Tseitin’s Algorithm to turn the propositional formula ((p → q) → (r → s)) → t) to CNF. [8 marks]

4. State with justification if each of the following sentences of predicate logic is logically valid. [8 marks]

(i).  (∀x ∃y∃zS(x, y, z)) → (∀x∀y∃zS(x, y, z)) [2 marks].

(ii).  (∀x ∃y∀zS(x, y, z)) → (∀u ∃v ∃wS(u, v, w)) [2 marks].

(iii).  (∀x∀y∃zS(x, y, z) → (∀x ∃y∀zS(x, y, z)) [2 marks].

(iv).  (∀x ∃z∀yS(x, y, z)) → (∀x∀y∃zS(x, y, z)) [2 marks].

5. Evaluate the given sentence on the respective relations S over domain {0, 1} [8 marks]

(i). ∀w ∃x∀y∃zR(w, x, y, z) on {(0, 1, 0, 1), (0, 1, 1, 0), (1, 0, 0, 0), (1, 0, 1, 1)} [2 marks]. (ii).  ∃w∀x ∃y∀zR(w, x, y, z) on {(1, 0, 0, 1), (1, 0, 0, 0), (1, 1, 0, 0), (1, 1, 0, 1)} [2 marks].

(iii). ∀x ∃y∀zR(x, y) ∨ R(y, z) on {(0, 1, 1), (0, 1, 0), (1, 1, 1)} [2 marks].

(iv). ∀x ∃y∀zR(x, y) ∨ R(y, z) on {(0, 1, 1), (0, 0, 1)} [2 marks].

6. Write a Python function load dimacs, that takes a file in DIMACS format as input and returns the clause set as a list of lists. For example the file containing the lines: ”pcnf 3 2”, ”1 -2 0” and ”-1 3 0” would become [[1, −2], [−1, 3]]. [6 marks]

7. Write a Python function simple sat solve, that takes a single argument clause set as a list of lists and solves the satisfiability of the clause set by running through all truth assignments. In case the clause set is satisfiable it should output a full satisfying assignment as a list of literals; in the case the clause setisunstatisfiable the function should output False.  For example on the input [[1, −2], [−1, 3]] the function might return [1, 3]. [10 marks]

8. Write a recursive Python function branching sat solve that takes two arguments clause set and partial assignment as input and returns either a full satisfying assignment, if the

clause set is satisfiable under the partial assignment, or False if it is not.  You should as- sume clause set is a list of lists representing the clause set and partial assignment is a list of literals. The function should solve the satisfiability of the clause set by branching on the two truth assignments for a given variable.  When the function is run with an empty partial assignment it should act as a SAT-solver. [10 marks]

9. Write a Python function unit propagate that takes a single argument clause set as input and which outputs a new clause set after iteratively applying unit propagation until it cannot be applied further. [10 marks]

10. Write a recursive Python function dpll sat solve that takes two arguments clause set and partial assignment as input and solves the satisfiability of the clause set under the par- tial assignment by applying unit propagation before branching on the two truth assignments for a given variable (this is the famous DPLL algorithm but without pure literal elimination). In case the clause set is satisfiable under the partial assignment it should output a full satisfying assignment; if it is not satisfiable the function should return False. When the function is run with an empty partial assignment it should act as a SAT-solver. [10 marks]

11. The final 10 marks of the coursework will be allocated according to the speed of your functions unit propagate and dpll sat solve running on some benchmark instances. If your code is faster than mine, you receive 10 marks; within a factor of 2, 8 marks; within a factor of 3, 6 marks; within a factor of 4, 4 marks; within a factor of 5, 2 marks. [10 marks]

Total marks: 100