
Project 3  Boolean Formulae and SAT
Due 11:59pm Wed, October 20th, 2010
Introduction
For this project you will develop code for constructing
collections of boolean formulae, and determine whether
they can be solved (satisfied). You will then use your
code to model binary numbers and solve a 3x3 magic square.
Getting Started
Download the following archive file p3.zip
and extract its contents.
Along with files used to make direct submissions to the
submit server (submit.jar, .submit, submit.rb), you will
find the following project files:
Some notes on public tests:
 Lines in expected output beginning with % are comments and are ignored by the submit server tests. They typically display examples of boolean formulae where multipe answers are possible.
 The public tests provided sometimes use one project function to test
a different project function. For instance, in public_binary3.ml
we use subst and eval to test the eq function.
On the submit server the tests will be using our own functions
instead. So it may be possible for you to pass public_binary3.ml
on the submit server even if you have not yet implemented subst and eval.
 Make sure you produce an answer in the correct format.
Distinguish between bool true, a formula (True), and
a vector of formulae [True].
Project Goals
For this project, you will develop some functions for working with
boolean formulae, defined by the following OCaml data type:
type formula =
False
 True
 Var of char
 And of formula * formula
 Or of formula * formula
 Not of formula
 Forall of char * formula
 Exists of char * formula
Here False and True represent the obvious values.
Var c represents the boolean variable with name c
(notice that variable names can only be characters. The constructors
And, Or, and Not represent boolean
conjunction, disjunction, and negation, respectively. For example,
the mathematical formula (a or b) and c would be represented by
the OCaml value And(Or(Var 'a', Var 'b'), Var 'c'). (We'll
explain Forall and Exists in a moment.)
We will use associative lists, which are just lists of pairs,
to assign truth values to variables:
type assignment = (char * bool) list
Here if an assignment contains the pair (c,b), then
that assignment gives the variable represented by the character
c the value b. When working with the type
assignment, you will find the functions List.assoc,
List.mem_assoc, and related functions helpful. See the OCaml
library documentation for more details.
You may assume for purposes of this project that whenever you work
with an assignment for boolean expressions, all listed
variables are distinct (i.e., you don't need to worry about shadowing names).
The last two kinds of formula, Forall and
Exists, represent the similarly named quantifiers. The boolean
formula Forall(x, f) is true if f is true under all
assignments to x, i.e., if f is true when
x=true and when x=false. The boolean formula
Exists(x, f) is true if f is true either for
x=true or x=false. For example, the formula
Forall('x', Or(Var 'x', Var 'y')) is true under the
assignment [('y', true)] and false under the assignment
[('y', false)].
Part 1: Associative Lists
We begin with writing some additional functions for associative lists.
For this section the multiple associations (bindings) may exist
for the same key (symbol). E.g., [('a',true);('a',false)]
 count_assoc : assignment char > int. This function
counts the number of times an association appears for some
symbol x in the assignment.
For instance, count_assoc 'a' [('a',true);('a',false)] 'a' returns 2.
 remove_assoc_all: assignment char > assignment. This function
removes all associations for some symbol x in the assignment.
For instance, remove_assoc_all [('a',true);('b',true);('a',false)] 'a' returns [('b',true)].
 change_assoc_all: assignment char bool > assignment.
This function changes all associations for some symbol x in
the assignment to the specified boolean value.
For instance, change_assoc_all [('a',true);('a',false)] 'a' true returns [('a',true);('a',true)].
 assoc_last: assignment char > bool. This function
returns the value bound to the last association for some symbol x
in the assignment.
For instance, assoc_last [('a',true);('a',false)] 'a' returns
false.
Part 2: Boolean Formulae
Write the following functions that work with boolean formulae:
 eval : formula > assignment > bool. This function
evaluates the boolean formula on the given variable assignment and
returns the result as an OCaml bool. For example, given the
OCaml value And(Or(Var 'x', Var 'y'), Var 'z') and the
assignment [('x', true); ('y', false); ('z', true)], the
eval function should return true. Your function can
assume that all of the formula's free variables are
specified in the assignment.
 vars_of : formula > char list. This function takes a
formula and returns a list of the names of the free variables
of the formula. The free variables are those that are not bound by a
quantifier. For example, for Exists('x', Or(Var 'x', Var
'y')), you should return a list containing only 'y'.
The list should contain no duplicates. There is no requirement as to
the order that the variable names must appear in the list.
 sat : formula > assignment option. This function
returns Some a, where a is a satisfying assignment,
if the formula is satisfiable, or None otherwise. For
example, sat (Or(Var 'x', Var 'y')) could return three
things: Some ([('x', true); ('y', false)]), Some ([('x',
false); ('y', true)]), or Some ([('x', true); ('y',
true)]), whereas sat (And(Var 'x', Not (Var 'x'))) would
return None. If more than one assignment is possible, you
may return any assignment. You might find the vars_of
function handy here. Do not worry about the efficiency of this function.
Part 3: Binary Arithmetic with SAT
The sat function you wrote above is likely not very
efficient; given a formula with n free variables, it probably
always runs in O(2^n) time. That's fine for this project, and
that's the worst case bound, but there has been significant progress
in recent years in developing SAT solvers that can test for
satisfiability much more efficiently in the "common case." One of the
major applications of SAT solvers is in reasoning about the kinds of
arithmetic hardware does, which is all carried out by bit twiddling.
In this project, you will implement a model of hardware arithmetic,
and you can then use your (inefficient) sat function to
compute some interesting stuff.
The functions for this part will work with the following type:
type vec = formula list
A vec is a list of boolean formulae representing the bits of
a machine word, with the low order bit at the head of the list. For
example, we would represent the number 13 as x = [True; False;
True; True]. Zero could be represented at [], or as
[False], or as [False; False], etc.
We could represent an unknown 4bit number as y
= [Var 'a'; Var 'b'; Var 'c'; Var 'd']. (We'll see the use of
this just below.) Below when we refer to x and y,
we'll mean these two vecs. For this problem, we will only
work with nonnegative numbers.
Write the following functions for type vec. For the first
few problems, you can just think of vec's as lists of
Trues and Falses.
 int_of_vec : vec > int. This function takes a
vec composed solely of Trues and Falses and
returns the integer equivalent. For example, int_of_vec [False;
True] should return 2. You don't need to handle the case when
some element of vec is neither True nor
False.
 vec_of_int : int > vec. This function takes a nonnegative
integer and returns the corresponding vec. For example,
vec 13 should return x above. vec_of_int 0
should return []. Hint: You'll
probably want to use the infix operators mod and /.
 subst : assignment > vec > vec. This function
reduces the vec argument to a vec of all
Trues and Falses by replacing the variables in the
vec according to the assignment and then evaluating
each bit. For example, subst [('x', true); ('y', false)] [Var
'x'; True; And(Var 'y', True)] returns [True; True; False].
 eq : vec > vec > formula. This function returns a
formula representing whether the two bit vectors are equal. For
example, eq [Var 'a'] [True] could return Or(And(Var 'a',
True), And(Not (Var 'a'), Not True)). (In other words, the two
vectors are equal if either both a and True are
true, or if both are false.)
You can assume for this problem that the two bit vectors have
the same length.
 add : vec > vec > vec. This function returns a new
vec representing the sum of the two vectors. You may assume
the two bit vectors have the same length. Since there may
be a carry out of the last bit, the resulting vector will have one
more element than the input vectors. You'll have to figure out the
formula for addition yourself. Hint: You'll probably want to write
a recursive helper function that has an extra parameter for the carry
bit.
Note that for eq and add, function arguments
may contain free variables, causing the boolean formulae returned
to contain free variables as well. Fully evaluating the results
will require an assignment where those free variables are bound.
Part 4: Magic Squares
A magic square is an nbyn grid of the numbers 1 through n^2
such that every number appears exactly once and the sum of each row,
column, and diagonal is the same. For example, here is a 3x3 magic
square:
In this part, you will write a function that solves the magic squares
problem, using the machinery you developed in parts 1 and 2. In
particular, what we will do is "reduce" the problem of finding a
solution to the magic squares problem to a boolean formula. We can
then use the sat function to actually find a solution. Here
are the functions you should write:
 pad : vec > int > vec. The function pad v i
returns a new vec that is equal to v but whose
length is the greater of i and the length of v.
I.e., it pads v, if necessary, with extra Falses so
that it has i bits.
 add_three : vec > vec > vec > vec. This function
returns a new vector that represents the sum of the three input
vectors. You can assume the three vecs have the same length.
 is_digit : vec > formula. The input is a vec
of length 4 (i.e., exactly 4 boolean formulae). This function returns
a formula that is true if and only if the vec is greater than
or equal to 1 and less than or equal to 9.
 disjoint : vec list > formula. This function takes a
list of vecs and returns a formula representing whether all
the vecs are different from each other.
 is_magic : vec list > formula. This function takes a
list of exactly nine vecs and returns a formula representing
whether the list is a magic square. A list [v1; v2; v3; v4; v5;
v6; v7; v8; v9] represents the following square:
You can assume that the vecs in the list consist of exactly
four boolean formulae each, i.e., they are fourbit numbers.
You can try out your is_magic function by seeing if it can
decide that the square above is magic. You can also try replacing one
or two entries by variables, and then seeing if your code correctly
finds the right numbers to fill in. However, you'll have to wait a
long, long time if you try making a lot of the entries in the magic
square variables, since your sat function probably takes
exponential time.
What to Submit
Write your solutions to this project in a file boolean.ml.
You can get a (very minimal) skeleton for this project here.
Submit your boolean.ml file under Project 3 on the
submit sever.
Submission
You can submit your project in two ways:

Submit your boolean.ml file directly to the
submit server
by clicking on the submit link in the column "web submission".
Next, use the submit dialog to submit your boolean.ml file directly.
Select your file using the "Browse" button,
then press the "Submit project!" button.
You do not need to put it in a Jar or Zip file.
Some students have mentioned problems
with using Internet Explorer, because
submissions being extracted in directories
(e.g., "C:\My Documents\330\boolean.ml") where
the submit server could not find them. The
problems went away when switching to the
Mozilla Firefox browser.


Submit directly by executing a Java program on a computer
with Java and network access. Use the submit.jar file
from the archive p3.zip,
To submit, go to the directory containing your project, then either
execute submit.rb or type the following command directly:
java jar submit.jar
You will be asked to enter your class account and password, then
all files in the directory (and its subdirectories) will be
put in a jar file and submitted to the submit server.
If your submission is successful you will see the message:
Successful submission # received for project 3
Academic Integrity
The Campus Senate has adopted a policy asking students to include the
following statement on each assignment in every course: "I pledge on
my honor that I have not given or received any unauthorized assistance
on this assignment." Consequently your program is requested to
contain this pledge in a comment near the top.
Please carefully read the academic honesty section of the
course syllabus. Any evidence of impermissible cooperation on
projects, use of disallowed materials or resources, or unauthorized
use of computer accounts, will be submitted to the Student
Honor Council, which could result in an XF for the course, or
suspension or expulsion from the University. Be sure you understand
what you are and what you are not permitted to do in regards to
academic integrity when it comes to project assignments. These
policies apply to all students, and the Student Honor Council does not
consider lack of knowledge of the policies to be a defense for
violating them. Full information is found in the course
syllabusplease review it at this time.
