COMP 360A: Introduction to Automated Reasoning Problem Set 6
Due: Tuesday, Oct 31
Submit, individually, a pdf file and the two edited ml files solvers.ml and test.ml to Classroom. OCaml functions must be accompanied by adequate tests to receive full credit. You may resubmit as much as you like before the end of the due date.
Problem 1. The goal of this problem is to implement a backtracking SAT solver based on the DPLL algorithm, which outputs a satisfying assignment if there is one.
1. (1 point ) Write tests for the following functions: apply empty, apply, assignment of literals, and choose var.
2. (2 points) Finish designing apply clause and apply sing.
3. (2 points) Finish designing naive sat. Use choose var and apply as helper functions.
4. (4 points) Finish designing find unit clauses, find pure, and dpll. Use the first two functions, choose var and apply as helper functions for dpll.
Problem 2. (3 points) Prove the following proposition. Let F be a CNF formula. If F is unsatis- fiable, then there exists a refutation R of F such that for all clauses Ci in R, Ci is not a tautology. (Hint: Use the resolution restriction and the resolution expansion lemmas from the textbook.)
Problem 3. The goal of this problem is to implement an UNSAT solver, which outputs a refutation if there is one. Note that because we are implementing resolution traces with lists, the ordering of the traces is reversed: in particular, resolvents precede their parents.
1. (1 point) Write tests for the following functions: proper sublist and subset.
2. (3 points) Finish designing is taut and resolve on. Use proper sublist and is taut as
helpers for resolve on.
3. (3 points) Finish designing resolve. Use resolve on as a helper.
4. (3 points) Finish designing resolve pairwise. Use resolve as a helper.
5. (3 points) Finish designing naive ref. Use subset and resolve pairwise as helpers.
6. (3 extra credit points) Improve naive ref so that the output refutations do not contain re- peated resolvents, and so that the resolvents in the output do not contain repeated literals.
Computer Science Tutoring