The goal of this exercise is to solve the satisfiability problem for boolean formulas, which consists in determining whether a propositional formula is satisfiable, i.e. is true under some valuation.
Open a new file sat.ml
.
We define a type
type var = int
for variables. A propositional formula is either
Define a type formula
for formulas (the constructors
should be named Var
, And
, Or
,
Not
, True
and False
).
Define a substitution function subst
of type var > formula > formula > formula
which replaces a given variable \(X\)
by a formula \(B\) in a formula \(A\). In mathematical notation, the
resulting formula is often noted \(A[B/X]\). In order to test whether you have
a precise variable v
, in your
match you should not write
 Var v > ...
(which will match any variable) but
when x = v > ...  Var x
Define a function free_var
of
type formula > var
which
returns an arbitrary free variable of the formula (a variable
which occurs in the formula). In the case where there is no such
variable, the exception Not_found
will
be raised. [NB: if you would rather have a function of type formula > var option
instead of raising and exception, this is fine.]
Define a function eval
of type
formula > bool
which evaluates a closed formula (a formula without free
variables). What we mean here is that you can suppose that the formula
given in argument is closed, you don’t have to test this.
We admit that a formula \(A\) with a free variable \(X\) is satisfiable if and only if either \(A[\top/X]\) or \(A[\bot/X]\) is satisfiable: trying both cases is called splitting on \(X\).
Using the functions of previous questions, define a function sat
of type formula > bool
which determines whether a formula is satisfiable.
You can test it with
let () =
let x = Var 0 in
let x'= Not x in
let y = Var 1 in
let y'= Not y in
let a = And (And(Or (x,y), Or (x',y)), Or (x',y')) in
let b = And (And(Or (x,y), Or (x',y)), And(Or (x,y'), Or (x',y'))) in
assert (sat a);
assert (not (sat b))
and add your own tests! The assert
function
will raise an exception if its argument is false
(try to
assert false
).
In practice, the above procedure is very slow and could be improved. For instance, on the formula \[X\land\lnot X\land X_1\land\ldots\land X_n\] it will try all the possible valuations for \(X_1,\ldots,X_n\), whereas it is easy to see that it cannot be satisfied for \(X=\top\) and \(X=\bot\), independently of the values of the other variables.
We now implement the DPLL algorithm on which are based most modern SAT solvers. It works much faster in practice, although the problem is NPcomplete. We admit that every boolean formula can be put into a conjunctive normal form (or cnf):
and we aim at determining the satisfiability of such formulas. They can be represented by the following types:
type var = int
type literal = bool * var (* false means negated *)
type clause = literal list
type cnf = clause list
Note that the cnf []
corresponds to true whereas the
clause []
corresponds to false.
We will be using standard operations on lists. They are part of the List module of the standard library, but we shall recode them here as an exercise.
Define a function list_mem
of
type 'a > 'a list > bool
which determines whether an element is present in a list. Test it
with
let () =
assert (list_mem 2 [1;2;3]);
assert (not (list_mem 5 [1;2;3]));
assert (not (list_mem 1 []))
Define a function list_map
of
type ('a > 'b) > 'a list > 'b list
which applies a function to every element of a list. Test it with
let () =
assert (list_map (fun x > 2*x) [1;2;3] = [2;4;6]);
assert (list_map (fun _ > ()) [] = [])
Define a function list_filter
of type ('a > bool) > 'a list > 'a list
which, in a list, keeps only the elements satisfying a given
predicate.
let () =
let even x = x mod 2 = 0 in
assert (list_filter even [1;2;3;4;6] = [2;4;6])
Observe that, given a variable \(X\) and a formula in cnf \[A=C_1\land\ldots\land C_n\] where the \(C_i\) are the clauses, a cnf for the formula \(A[\top/X]\) can be obtained from \(A\) by
and similarly for \(A[\bot/X]\). Can you see why?
Using the functions on lists coded above, implement a
substitution function subst_cnf
of type var > bool > cnf > cnf
which replaces a variable \(X\) by
either \(\top\) or \(\bot\) in a formula in cnf.
Implement again the function dpll
of type cnf > bool
,
using splitting as in the first part, but noting that
[]
is true,[]
is false(in particular, a cnf without free variables is in one of those two
cases). This should allow to conclude that a formula is not satisfiable
without giving a value to every variable. You can use the function List.hd
of type
'a list > 'a
which returns the first element of a list (or raises
Failure "hd"
if the list is empty). We also recall that you
can extract the first and second components of a pair with the functions
fst
and
snd
.
Test your function with the same example as previously:
let () =
let x = true, 0 in
let x'= false,0 in
let y = true, 1 in
let y'= false,1 in
let a = [[x;y]; [x';y]; [x';y']] in
let b = [[x;y]; [x';y]; [x;y']; [x';y']] in
assert (dpll a);
assert (not (dpll b))
The algorithm can be further improved by carefully choosing the variables on which we split. In particular, we should eliminate first the variables for which we will easily be able to conclude (at least one branch of the splitting).
A clause \(C_i\) is unitary when it is reduced to a literal. If \(C_i=X\), we know that \(X\) must be true in order for the formula to be satisfied (the case \(X=\bot\) will immediately fail), and similarly in the case where \(C_i=\lnot X\).
Program a function unit
of type
cnf > literal
which finds a
unitary clause in a formula (or raises Not_found
if there
is none).
Test it with
let () =
let x = true, 0 in
let y = true, 1 in
let y'= false,1 in
assert (unit [[x;y]; [x]; [y;y']] = x)
A literal \(X\) (resp. \(\lnot X\)) is pure in a formula \(A\) if \(\lnot X\) (resp. \(X\)) does not occur in any clause of \(A\) (i.e. the variable always occurs with the same polarity). What can we say of the satisfiability of a formula which contains a pure literal?
Program a function pure
of type
cnf > literal
which finds a
pure literal in a formula (or raises Not_found
if there is
none).
Modify the function dpll
so
that it operates in the following way on a given cnf
true
,false
,In the last case, we can still (hope to) improve the algorithm by carefully choosing the variables on which we split. The MOM heuristics (for Maximum number of Occurences in the Minimum length) consists in choosing a variable which occurs most among clauses of minimal length.
Program a function mom
of type
cnf > var
which finds such a
variable (or raises Not_found
if the formula has no
variable), and use it in dpll
.
Given a clause \(C\), we write \(C\) for the number of literals in \(C\). Given a formula \(A\) and a literal \(L\), we write \(C\in_L A\) to indicate that \(C\) is a clause of \(A\) containing \(L\) and define \[\mathcal{J}(L)=\sum_{C\in_L A}\left(\frac12\right)^{C}\] The JeroslowWang heuristics consists in splitting on the variable corresponding to a literal which maximizes \(\mathcal{J}\).
Program a function jw
of type
cnf > literal > float
which computes the above quantity.
Program a function jw_var
of
type cnf > var
which finds a
variable according to the JeroslowWang heuristics, and use it in dpll
.
The CNF file format is a text format to encode SAT problems, of which you can find many examples on the net.
A parser for the CNF file format can be implemented as follows:
(** Parse a CNF file. *)
let parse f : cnf =
let load_file f =
let ic = open_in f in
let n = in_channel_length ic in
let s = Bytes.create n in
really_input ic s 0 n;
close_in ic;
Bytes.to_string s
in
let f = load_file f in
let f = String.map (function '\t' > ' '  c > c) f in
let f = String.split_on_char '\n' f in
let f = List.map (String.split_on_char ' ') f in
let f = List.filter (function "c"::_  "p"::_ > false  _ > true) f in
let f = List.flatten f in
let aux (a,c) = function
"" > (a,c)
 "0" > (c::a,[])

 n >let n = int_of_string n in
let x = if n < 0 then (false,n) else (true,n) in
(a,x::c)in
fst (List.fold_left aux ([],[]) f)
You can then test the file file.cnf
by something
like
let () = assert (dpll (parse "file.cnf"))
It is advised that you compile your program in native mode, so that it is faster, by typing on a console
ocamlopt sat.ml o sat
You can then run the program with
./sat
You can even pass a file name as argument by executing
./sat file.cnf
and the file name can be retrieved in OCaml with Sys.argv.(1)
(see the
documentation).
Here are some examples of satisfiable files:
and unsatisfiable ones:
Some of those files are quite complicated, it is normal if your program takes quite some times to check them (or even does not terminate in a reasonable amount of time for some of those).
A Sudoku can be
encoded as a 9×9 matrix cells
of integers such that
cells.(i).(j)
\(=9\) means
that the cell \((i,j)\) is empty and
\(0\leq\)cell.(i).(j)
\(<9\) means that the cell contains the
number cells.(i).(j)
\(+1\). For instance, the game
. . 8 6 5 . . 2 1 
. 9 3 4 . 2 . 8 . 
5 . . . . . 3 . . 
3 8 . . 7 . 1 . 9 
. 6 . . . . . 4 . 
2 . 9 . 1 . . 7 3 
. . 5 . . . . . 6 
. 1 . 3 . 9 8 2 . 
7 3 . . 2 6 1 . . 
is encoded as
let simple_sudoku =
9;9;7;9;8;2;4;9;9];
[[5;4;9;3;9;1;9;9;9];
[9;1;0;9;7;9;2;9;9];
[2;7;9;9;5;9;1;9;8];
[9;6;9;9;9;9;9;0;9];
[0;9;8;9;3;9;9;6;2];
[9;9;4;9;0;9;6;2;9];
[9;9;9;2;9;8;9;1;5];
[9;9;5;7;1;9;0;9;9]] [
Our aim is now to encode such a game as a SAT problem. We define
let var i j n : var =
let i = i mod 9 in
let j = j mod 9 in
9*(9*i+j)+n
the function which returns a variable depending on \(0\leq i<9\), \(0\leq j<9\) and \(0\leq n<9\). In a valuation, the value
of var i j n
is true means that the cell \((i,j)\) contains the value \(n\). We now want to generate formulas which
encode the fact that a valuation gives rise to a solution to a sudoku
game.
Define a function sudoku
of
type int array array > cnf
,
which takes a Sudoku game as above, and returns a cnf which is
satisfiable if and only if the Sudoku game is. The function must
generate formulas expressing that
It can be shown that these conditions suffice (e.g. they imply that there is at most one number in a cell).
Test it with
let () =
assert (dpll (sudoku simple_sudoku))
Here is also an example of a game of medium difficulty:
let medium_sudoku =
9;1;9;7;4;3;9;9;9];
[[9;9;9;5;9;9;9;9;7];
[9;0;9;9;9;9;9;9;8];
[1;9;9;9;9;9;9;8;2];
[9;6;4;2;9;7;5;1;9];
[7;8;9;9;9;9;9;9;6];
[3;9;9;9;9;9;9;5;9];
[2;9;9;9;9;1;9;9;9];
[9;9;9;6;5;0;9;3;9]] [
a hard one:
let hard_sudoku =
9;9;9;9;4;9;8;9;9];
[[8;7;9;9;9;9;9;4;9];
[9;3;4;6;9;9;2;9;9];
[9;9;3;1;9;9;7;6;9];
[9;9;9;0;9;3;9;9;9];
[9;6;5;9;9;8;0;9;9];
[9;9;7;9;9;0;5;2;9];
[9;1;9;9;9;9;9;7;0];
[9;9;6;9;2;9;9;9;9]] [
and an unsolvable one:
let unsolvable_sudoku =
1;9;9;8;9;9;9;9;9];
[[9;9;9;9;9;9;9;5;9];
[9;9;9;9;9;0;9;9;9];
[4;9;1;5;9;9;3;9;6];
[9;9;9;9;9;3;0;9;9];
[9;9;9;9;8;7;9;1;2];
[9;9;9;9;9;2;9;7;9];
[9;9;4;9;0;9;9;9;9];
[9;9;6;9;9;9;9;9;9]] [
As usual, you can test those with
let () =
assert (dpll (sudoku medium_sudoku))
let () =
assert (dpll (sudoku hard_sudoku))
let () =
assert (not (dpll (sudoku unsolvable_sudoku)))
As before, the medium and hard problem might take quite some time to check.
Define a procedure cnf
of type
formula > cnf
which puts a
formula into conjunctive normal form. It might be a good idea to first
define a function of type bool > formula > cnf
which puts a formula, or its negation (depending on the boolean
argument), in cnf.