In this assignment, you will use exception-based backtracking to solve a well-
known problem called SAT. SAT is short for “boolean satisfiability.” Simply put, if
you have a boolean formula with variables, SAT asks if there is any way to assign
true and false to each variable so that the value of the formula is true. In this
assignment, we write & for boolean AND, I for boolean OR, and ~ for boolean
For example, the formula x & ~y is satisfiable, by assigning x to true and y to
false. The formula x &
~x is not satisfiable, because no matter what value we
give to x, x &
~x will be false.
Boolean Formulae
In HW2, you worked with expression trees of float s. In this assignment, you will
witterenice s cinderent. was the tree had the ah cam ex wession-iT’ha biffss the trees
can have many named variables.
The Conjunction and Disjunction constructors represent boolean AND and
boolean OR, respectively.
expressions, you will have to use a dictionary from variable names to boolean
values. These dictionaries are called truth assignments. You will also want to know
all of the variables which appear in an expression, which is a set of names.
In the Prelude for this assignment, we’ve given you a function parse_formula
string -> formula. You can use it however you want, including to write tests. It
parses expressions like those shown above, including “(a | ~b) & c”
and “al | a2 I
• Try playing with it in the toplevel! Note that LearnOCaml
compiles your tests in your browser and does not always optimize, so larger input
strings may cause the parser to run out of memory. We tested it successfully, but
your mileage may vary.
You are not required to understand how the parser works, but feel free to look
around the implementation if you are interested.
Variable_set and Variable_map
In order to make sets of variables and dictionaries of variables, we have defined the
Variable_set and Variable_map modules for you. The interface is very similar
to simplified one you saw in class. These modules are defined using OCaml’s
standard Set .Make and Map.Make functors. The links in the previous sentence will
take you to their documentation.
For example, we could define the set of variables {x, y, z} as
let xyz : Variable_set.t
Variable_set.singleton
I> Variable set.add
|> Variable_set.add “z
We could also define the truth assignment that maps x to true, and y and z to
let xyz_truth_asgn : truth_assignment
Variable_map.singleton
> Variable_map.add
|> Variable_map.add
You are encouraged to define some constant variable sets and truth assignments to
use in your tests.
Question 1 (10 points)
Implement the function collect_variables : formula -> Variable_set.t.
This function takes a formula and returns the set of variable names which appear
anywhere in the formula. You may use any functions you want and whichever
recursive style you prefer.
Question 2 (15 points)
Implement the function eval : truth_assignment -> formula -> bool.
This function is very similar to the eval function from HW2. However, now you
are evaluating boolean formulae instead of float arithmetic. You also need to use
the correct boolean value for each variable. We recommend using
Variable_map. find_opt to perform lookups in the truth assignment. If a variable
is needed but does not appear in the truth assignment, you must raise an
Unassigned_variable x exception, where x is the unassigned variable.
Once again, you may use any functions you want and whichever recursive style
you prefer.
The test cases you must implement for this problem are split into two lists.
eval_success_tests is a list of tests for when eval does not raise an exception
and yields a bool, and eval_failure_tests is a list of tests for when eval
raises an exception.
Note: “f x && g y ” is not the same as “let fx
x in let gy = g y in fx
Question 3 (25 points)
Implement the function find_satisfying_assignment : formula ->
truth_assignment.
This function takes a formula and produces a truth_assignment which makes
the formu a evaluate to true
• If no such assignment exists, you must raise an Unsatisfiable_formula
exception.
• The truth assignment you return must be sharp, which means it must have an
assignment for every variable in the expression and no others.
• You can (and should) use the functions from both previous problems.
” Yoicttont the aurogfaderwild hard check thisarch to implement this
The test cases you must implement for this problem use truth_assignment
option as output type. A None output corresponds to
find_satisfying_assignment raising an exception on an unsatisfiable formula
given as input. A Some t output corresponds to find_satisfying_assignment
succeeding with t as satisfying truth assignment.
Further Reading
SAT turns out to be a surprisingly hard problem. But it’s very useful – a huge variety
of practical problems can be encoded as SAT problems. Examples include the
longest path problem, register allocation, OCaml type inference, and many others.
If you’re interested in the SAT problem and how high-powered solvers tackle it, the
paper A survev of SAT solver [W. Gone. X. Zhou 20171 is a good starting point.
let collect_variables_tests: (formula * Variable_set.t) list
(* TODO: Implement the function. *)
let collect_variables (formula : formula) : Variable_set.t=
raise Not_implemented
(** Question 2 *)
(* TODO: Add test cases.
let eval_success_tests : ((truth_assignment * formula)
* bool) list = [7
(* TODO: Add test cases.
let eval failure tests :
((truth_assignment * formula)
* exn) list = []
(* TODO: Implement the function.
let eval (state : truth_assignment) (formula : formula) : bool =
raise Not_implemented
(** Question 3 *)
(* TODO: Add test cases.
let find_satisfying_assignment_tests : (formula * truth_assignment option) list
(* TODO: Implement the function.
let find_satisfying_assignment (formula : formula) : truth_assignment
raise Not_implemented