Project 4 - Boolean Formulae and SAT

Introduction

Getting Started

Along with files used to make direct submissions to the submit server (submit.jar, .submit, submit.rb), you will find the following project files:

• Your OCaml program - boolean.ml
• Utility code - testUtils.ml
• Public tests
  • public_boolean1.ml
  • public_boolean2.ml
  • public_binary1.ml
  • public_binary2.ml
  • public_binary3.ml
  • public_binary4.ml
  • public_magic1.ml
  • public_magic2.ml
• Expected outputs for public tests
  • public_boolean1.out
  • public_boolean2.out
  • public_binary1.out
  • public_binary2.out
  • public_binary3.out
  • public_binary4.out
  • public_magic1.out
  • public_magic2.out
• Test Script - goTest.rb
• New Test Cases - myTest.ml

• 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 bitadd and eq functions. 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, 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: 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 2: 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 4-bit 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 non-negative 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.

• double : vec -> vec. This function returns a vec representing twice its argument. For example, double [False; True] (which is 2) should return [False; False; True] (which is 4). (Yes, this is really easy.)
  
  
• 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 non-negative integer and returns the corresponding vec. For example, vec 13 should return x above. 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].
  
  
• zero : vec -> formula. This function returns a boolean formula representing whether vec represents zero, i.e., is composed solely of False or formulae that are false. For example, if y is the four-bit number defined above, zero y could return And(Not Var 'a', And(Not Var 'b', And(Not Var 'c', Not Var 'd'))). This is really cool: Once we have this, we can ask a question like sat (zero y), and the sat function will tell us, yes, there are choices for Var 'a', Var 'b', Var 'c', and Var 'd' that make the formula true. When you're testing your code, you can use the functions subst and int_of_vec above to look at your answers more easily.
  
  
• bitand : vec -> vec -> vec. This function returns a new vec representing the bitwise and of the two vectors. For example, if x and y are as defined above, then bitand x y should return [And(True, Var 'a'); And(False, Var 'b'); And(True, Var 'c'); And(True, Var 'd')]. Now we can do an even cooler thing: we can ask a question like sat (zero (bitand x y)), i.e., are there choices for variables a..d such that if you and x with y, you get zero. You can assume for this problem that the two bit vectors have the same length.
  
  
• 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.) Now we can ask questions like, sat (eq y (bitand x y)), i.e., is there a 4-bit number such that if you bitwise and it with x, you get itself. 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.
  
  
• 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.
  
  
• mul : vec -> int -> vec. This function mul a i returns a new vec representing the product of the a and i. Assume i is non-negative. Hint: For an efficient algorithm, use the following idea. If i is divisible by two, then a*i is the same as (a*2)*(i/2). Otherwise, i is odd. If i is one, the product is a. Otherwise, the product is a*(i-1) + a.

Part 3: Magic Squares

A magic square is an n-by-n 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:

• 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:

  v1	v2	v3
  v4	v5	v6
  v7	v8	v9

  You can assume that the vecs in the list consist of exactly four boolean formulae each, i.e., they are four-bit 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 4 on the submit sever.

Submission

• 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 p4.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 4

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 syllabus---please review it at this time.