首页 >
> 详细

Computational Thinking 2020/21

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. [9 marks]

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

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

(iii). Is {∨, ∧} a complete set of connectives?

(iv). {→} is not a complete set of connectives. With which constant can it be made complete?

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

your answer. [11 marks]

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

(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)?

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

(iv). Use Tseitin’s algorithm to convert ((p ∨ (q ∧ r)) → ((x ∧ y) ∨ (u ∧ v))) to CNF.

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). [5 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. [5 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. [10 marks]

6. Write a Python function unit propagate in the two arguments literal and clause set

which outputs a new clause set after iteratively applying unit propagation until it cannot be

applied further. [10 marks]

1

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. There are three people: Stihl, Moller and Einstein. It is known that exactly one of them is ¨

Russian, while the other two are Germans. Moreover, every Russian must be a spy. When

Stihl meets Moller in a corridor, he makes the following joke: “you know, M ¨ oller, you are as ¨

German as I am Russian”. It is known that Stihl always tells the truth when he is joking. We

aim to establish that Einstein is not a Russian spy by using your SAT-solver. Use propositional

variables from the Cartesian product of {Stihl, Moller, Einstein ¨ } and {Russian, German, Spy},

e.g. Einstein-Spy is true iff Einstein is a spy. Write out a propositional encoding for this problem

justifying your constructed clauses. Make a DIMACS format instance and run it through your

SAT-solver. [10 marks]

10. 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]

联系我们

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

- Cs2461-10实验程序代做、代写java，C/C++，Python编程设 2021-03-02
- 代写program程序语言、代做python，C++课程程序、代写java编 2021-03-02
- Programming课程代做、代写c++程序语言、Algorithms编程 2021-03-02
- 代写csc1-Ua程序、代做java编程设计、Java实验编程代做 代做留学 2021-03-02
- 代做program编程语言、代写python程序、代做python设计编程 2021-03-02
- 代写data编程设计、代做python语言程序、Python课程编程代写 代 2021-03-02
- Cse 13S程序实验代做、代写c++编程、C/C++程序语言调试 代写留学 2021-03-02
- Mat136h5编程代做、C/C++程序调试、Python，Java编程设计 2021-03-01
- 代写ee425x实验编程、代做python，C++，Java程序设计 帮做c 2021-03-01
- Cscc11程序课程代做、代写python程序设计、Python编程调试 代 2021-03-01
- 代写program编程、Python语言程序调试、Python编程设计代写 2021-03-01
- 代做r语言编程|代做database|代做留学生p... 2021-03-01
- Data Structures代写、代做r编程课程、代做r程序实验 帮做ha 2021-03-01
- 代做data留学生编程、C++，Python语言代写、Java程序代做 代写 2021-03-01
- 代写aps 105编程实验、C/C++程序语言代做 代写r语言程序|代写py 2021-03-01
- Fre6831 Computational Finance 2021-02-28
- Sta141b Assignment 5 Interactive Visu... 2021-02-28
- Eecs2011a-F20 2021-02-28
- Comp-251 Final Asssessment 2021-02-28
- 代写cs1027课程程序、代做java编程语言、代写java留学生编程帮做h 2021-02-28