首页 >
> 详细

Computational Thinking 2021/22

Logic Coursework

Barnaby Martin

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 as 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

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 justifying

your answer. [12 marks]

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

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

(iii). Is {¬, ↔} a complete set of connectives? [4 marks.]

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

2. Answer the following question about Conjunctive Normal Form (CNF), in each case justifying

your answer. [12 marks]

(i). Show that any formula may be rewritten to an equivalent formula in CNF. [3 marks.]

(ii). Is there a polynomial p so that a general formula of size n can be rewritten to an equivalent

formula in CNF of size at most p(n)? [2 marks.]

(iii). What if we change equivalent to equisatisfiable in the previous question? [1 mark.]

(iv). Use Tseitin’s algorithm to convert (p → (q → (r → (s → (t → u))))) to CNF. [6 marks.]

3. Write some Python code that loads a textual file in DIMACS format into an internal representation

of a clause set, for which we will use a list of lists. For example, (v1 ∨ ¬v2) ∧ (¬v1 ∨ v3)

would become [[1, −2], [−1, 3]]. [6 marks]

4. Write a Python function simple sat solve in a single argument clause set that solves

the satisfiability of the clause set by running through all truth assignments. In case the clause

set is satisfiable it should output a satisfying assignment. A full (truth) assignment should be

represented by a list of literals. For example v1 ∧ ¬v2 ∧ v3 would be [1, −2, 3]. [10 marks]

5. Write a recursive Python function branching sat solve in the two arguments clause set

and partial assignment that solves the satisfiability of the clause set by branching on the

two truth assignments for a given variable. In case the clause set is satisfiable under the partial

assignment it should output a satisfying assignment. When this is run with an empty partial

assignment it should act as a SAT-solver. A partial assignment should be represented by a list

of literals, as was a full assignment in the previous question. [10 marks]

1

6. Write a Python function unit propagate in a single argument clause set which outputs

a new clause set after iteratively applying unit propagation until it cannot be applied further.

[10 marks]

7. Write a Python function pure literal eliminate in a single argument clause set which

outputs a new clause set after iteratively applying the pure literal assignment scheme until it

cannot be applied further. [10 marks]

8. Write a recursive Python function dpll sat solve in the two arguments clause set and

partial assignment that solves the satisfiability of the clause set by applying unit propagation

and pure literal elimination before branching on the two truth assignments for a given

variable (this is the famous DPLL algorithm). In case the clause set is satisfiable under the

partial assignment it should output a satisfying assignment. When this is run with an empty

partial assignment it should act as a SAT-solver. [20 marks]

9. The final 10 marks of the coursework will be allocated according to the speed of your functions

unit propagate, pure literal eliminate and dpll sat solve run on some benchmark

instances. If your code is faster than mine, you receive 10 marks; within a factor of 2,

6 marks; within a factor of 3, 4 marks; within a factor of 4, 2 marks. [10 marks]

Total marks: 100

联系我们

- QQ：99515681
- 邮箱：99515681@qq.com
- 工作时间：8:00-21:00
- 微信：codinghelp

- Fit5217辅导、Python程序语言辅导 2022-05-31
- 辅导ecs 170 Introduction To Artificial... 2022-05-31
- 辅导ecs 170 Homework Assignment 5 2022-05-31
- Fit 5003 Software Security辅导 2022-05-30
- 辅导cse 101 Data Structures And Algori... 2022-05-30
- 辅导econ7150、辅导java，Python编程 2022-05-30
- Econ7150编程辅导 讲解 S1 2022 2022-05-29
- 讲解cse 101 程序 辅导 Data Structures 2022-05-29
- 辅导fit 5003 Software Security 2022-05-29
- Stat7055 Introductory Statistics For B... 2022-05-28
- Assignment 3 Description: Computer Sy... 2022-05-28
- 辅导laboratory 程序、辅导program编程 2022-05-28
- 讲解eece 1080C Programming For Ece 2022-05-28
- Comp10002 Foundations Of Algorithms辅导... 2022-05-28
- 辅导 Swen30006、辅导java/C++编程 2022-05-28
- Comp326讲解导、辅导python，Java程序 2022-05-28
- 辅导 Dungeon Crawler C++ - Assignment ... 2022-05-27
- 辅导mast30025 Linear Statistical Model... 2022-05-27
- Prog2002辅导、辅导sql语言编程 2022-05-26
- 辅导 Info411/911 Data Mining Knowledge... 2022-05-26