辅导program编程、讲解Python程序设计
- 首页 >> Java编程 Computational Thinking 2020/21
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]
2
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]
2