Your first practical / homework is to write a SAT-solver, i.e. a solver for mathematical problems expresses in propositional logic.
The SAT problem consists in deciding, given a formula in Conjunctive Normal Form, if it is satisfiable. We recall the basic definitions:
lis a variable
xor its negation
Cis a disjunction of literals
l1 ∨ ... ∨ ln
C1 ∧ ... ∧ Cm
⊥to each variable
Exercise.ml. We give examples of different difficulties to
In the Emacs+Tuareg+Merlin working environment, the keyboard shortcut ctr-x-e (also available via the menus Tuareg-Interactive Mode-Evaluate Phrase) will feed your current OCaml command to the OCaml interpreter.
The result of the run should appear in a new emacs buffer.
Exercise.opt, which can for instance be run from the command line.
For testing purposes, we provide a DIMACS parser (DIMACS is the standard format for SAT-soslving problems):
as well as a couple of tests
(but you can download other DIMACS files from the Internet).
It contains a file
dpllT.ml which is very similar
The main difference is that literals may be taken as literals from a particular theory T, for which we have a decision procedure (a function of type (Lit.t list -> bool) deciding whether a conjunction of literals is consistent (outputs true) or inconsistent (outputs false) with the theory T.
This decision procedure is passed as an extra argument to
You need to complete the function solve, which now takes the decision procedure as an extra argument, and which is now of type (solutionType -> bool) -> cnfType -> solutionType
In order to test your algorithm, we have included, in the subdirectory LRA of the archive
LRALitof the module type
LitType, implementing the literals of Linear Rational Arithmetic (LRA); a decision procedure for Linear Rational Arithmetic (function
Note: When reaching the test code, the simple OCaml interpreter available from emacs may not be able to fetch the code in subdirectory LRA.
A more robust approach is to use
ocamlbuild from the command line, to compile a multi-file project:
In the directory with files
_tags, run the command
ocamlbuild dpllT.native (compiling to native code) or
ocamlbuild dpllT.byte (compiling to bytecode). If no error occurs, it will produce a file
dpllT.byte which you can run on your OS.
Among the tests, we have modelled the 2016 American elections and expressed as a CNF (built on LRA literals) the question "There is a tie between Clinton and Trump". Determining whether this CNF is SAT answers the question of whether a tie is possible. We added a piece of code to count the number of solutions (if any). For this particular question, there should be 5 solutions.
all_form.ml. Some explanations about the provided code: Implementing
∀x p(x)as we write it by hand is not convenient because we have to manipulate formulae as equivalence classes of trees, the equivalence being that generated by the renaming of bound variables. This is not impossible, e.g. working on canonical representatives in the classes, but is quite complicated, error-prone and actually slightly inefficient. Most implementations use the solution proposed in the file: A term
tis not considered independently from the context in which it is being used. If it is considered as a term occurring in a formula, in such a way that one of its variables "
x" is bound by a quantifier
∃xfurther up in that formula, then in the implementation, the quantifier
∃xis simply encoded as
∃, forgetting the name of the bound variable; at the same time, every occurrence of
xin the term
tis encoded as
(Bound i), where
iis an integer: the number of quantifiers that one has to cross when going from
xto the quantifier that binds
xin the formula tree. For instance,
∀x (x=x)is implemented as
∀(Bound 0 = Bound 0), because there are no quantifiers to cross when going from an occurrence of
∀x. On the other hand
∀x ∃y (x=y)is implemented as
∀∃(Bound 1 = Bound 0)because from
yto its binder, there are no quantifiers to cross, but from
xto its binder, there is 1 quantifier to cross (that which binds
y). Note that sometimes, not all occurrences of
xgets the same
i, e.g. in
∀x ((x=x) ∧ ∃y (x=y)), which is implemented as
∀((Bound 0 = Bound 0) ∧ ∃(Bound 1 = Bound 0)). Now if the term
tis considered in a context that does not bind
xis really a free variable, not just in the term
t, but also free in the context in which
tis being used, then
xis implemented as
(Free "x"). Note that the manipulation of bound variables, managing the integers i of the
(Bound i)constructs, is not something you should worry about, because the only point of a variable
∃xis at some point to be substituted by a term
t', and we give you the substitution function: If you see the formula
∀x A(x), and you want get into
Aitself, you need to say with which
xyou are doing this, i.e. with which term
t'you want to substitute
x. In that case you call
(subst t' 0 A)to have what you would write on paper as
A(t'). In case you don't want to substitute it by any interesting term and really want to work on
xis really a free variable, you can just call
(subst (Free "x") 0 A).