Satisfiability of Boolean functions

Due Wednesday, 30 September, 2009

In the lab, we saw that linear search is extremely fast, so millions of entries can be searched in a short amount of time. Other kinds of searches take much longer. A Boolean formula is said to be satisfiable if its truth table has a "T" at the right of some row; in other words if some setting of the variables results in the formula taking on the value "true". This assignment is to write a program that does an exhaustive search (essentially computing each row of the truth table) to determine whether a given Boolean formula is satisfiable.

Your program should have an array of true-false values (represented by 1s and 0s) that represents the left-hand side of the current row of the truth table. To test that row, it should call a subroutine that evaluates the given Boolean function for that row of the truth table. For example, if the function is (b0 AND b2) OR b3 the subroutine should return true (or 1) if passed the array (1, 0, 1, 0) (representing that b0 and b2 are true and b1 and b3 are false) or (0, 1, 0, 1), but return false (or 0) if passed the array (1, 1, 0, 0). If a satisfying assignment is found, the program should print a message including the assignment, and exit. If the program searches all possibilities and no satisfying assignment is found, it should print "unsatisfiable".

To search through all possible settings of the variables, you should think of the array of true-false values as a stack, and use Perl's push and pop operators to modify the values. Initially, all the values should be set to false (0, 0, 0, ..., 0). To generate a new setting, pop off the last value. If it was 0, push a 1 on in its place. If it was 1, pop the next value. If that was 0, push a 1 on to replace it, then push a 0 to replace the 1. In general, pop until you reach a 0, replace that with a 1, and push on enough 0s to replace the 1s that were popped. If there was no 0 in the array, you've reached (1, 1, 1, ..., 1) and you're done.

The size of the array should be determined by a variable near the top of the program. Initially set it to 4 or so, so that you can print all values while testing. Once you're convinced that your program works, try setting it to larger sizes. Put the answers to the following questions in a comment near the top of the program:

Submit your well-documented program online using the command

provide comp14 hw3 progname.pl

The documentation should contain your name near the top. The assignment is worth 100 points.