Project 2: SAT Solver Front-End

Due: March 7, 2017 11:59:59pm

Introduction

In this project, you will implement a front-end for the Boolean constraint solver your wrote in Project 1.

For example, after implementing this project, you’ll be able to run the following program:

Pretty soon you’ll be ready to enter the International SAT Competition! Here is the code skeleton for the project.

Input Language

The input language to your solver is given by the following grammar, where capitalized words indicate non-terminals or the tokens ID or INT.

Here identifiers ID are made up of upper- and lowercase letters, digits, and underscores. They must begin with a letter or underscore. INT is made up of digits. (Note INTs must therefore be non-negative.)

Part 1: Parsing

The first step in building your solver is to develop a parser for the input language with ocamllex and ocamlyacc. Your parser will accept strings produced from PROG in the grammar above. Your parser should obey the following conventions:

• &, |, + are left-associative

• In boolean expressions, ! binds more tightly than &, which binds more tightly than |. For example: a | !b & c should parse as a | ((!b) & c).

• In vectors, & binds more tightly than +.

• A literal vector is made up of a sequence of zero or more boolean expressions separated by commas, and is delimited by [ and ]. A trailing comma is not allowed. For example, [], [0, a, b & c], and [forall x . x | y;] are all valid literal vectors, but [a,b,] is not.

• An assignment contains zero or more comma-separated pairs of bindings of identifiers to boolean values 0 or 1, where : separates the identifier from its value. The assignment is delimited by [ and ]. Trailing commas are not allowed. For example, [] and [a:1,b:0] are valid assignments, but [a:2], [a:1,b:0,], [a:(0)], and [a:(0|1)] are not.

• Empty programs are allowed.

• Statements are terminated by semicolons. A semicolon by itself is not valid, nor can extra semicolons be added to the end of statements.

• forall, exists, eq, and zero and terminated by ;. This is non-standard but will make parsing a bit easier.

• Whitespace is not significant and should be ignored.

• Comments begin with # and extend to the end of the line.

Part 2: Evaluation

Your parser should run the program as it parses it, following these rules:

• In general, your solver should not print anything out except exactly what we tell you below. So be sure to remove any debugging print statements before you submit your code.

• However, you may add extra newlines before or after executing individual statements.

• Statements bprint and vprint should print out their corresponding expressions or vectors using the code we’ve given you in unparse.ml. Please do not modify that code as we might rely on the exact format it uses to print.

• Statements bool ID = BEXPR and bvec ID = VEXPR bind the given identifiers to a boolean expression or vector, respectively. (And these statements do not print anything.) Inside of a BEXPR, if an ID has previously been bound to a BEXPR, its binding should be substituted for the identifier. If ID has previously been bound to a VEXPR, your solver should raise an exception (any exception). If ID has not been bound, then it should be turned into an EVar node with that id string. For example:

  • bool x = 0; bprint x; prints false

  • bvec x = 0; bprint x; throws an exception in evaluating the bprint statement because x is not a boolean expression.

  • bprint x; prints x

  For a VEXPR, if ID has previously been bound to a VEXPR, the previous binding is substituted for the identifier. If ID has previously been bound to a BEXPR, or if ID is not bound, your parser should raise an exception.

• Statement eval ASST BEXPR; evaluates an expression under an assignment and prints the resulting truth value as either true or false followed by a newline.

• Statement fv BEXPR; prints out a comma-separated list of the free variables of a boolean expression. For example:

  • fv x; prints x followed by newline.

  • fv x & y; prints x, y followed by newline.

  • fv 1; prints a newline.

• Statement sat BEXPR; prints out either Unsat if there is no satisfying assignment, or it prints out the satisfying assignment in the same format as ASST. For example:

  • sat 0; prints Unsat followed by a newline.

  • sat x & y; prints [x:1, y:1] followed by a newline.

• Statement int_of VEXPR; prints the integer corresponding the the VEXPR followed by a newline. Your solver should raise an exception if VEXPR contains anything other than 0’s and 1’s.

• (Note there are no expressions, vectors, or statements corresponding to subst for bvec.)

Part 3: More Parsing!

Extend your parser to handle a larger fragment of linear arithmetic, including inequalities and multiplication.

Multiplication is left-associative, binds more tightly than +, and less tightly than & in vectors.

Note: your previous implementation did not handle these features. The project skeleton provides stubs for these functions. You will only be graded on whether your implementation can parse them; bonus points are available to anyone who can implement them.

What to turn in

Put all your code in the code skeleton we have supplied, and upload your solution to the submit server. You can either upload your solution via the web interface, or you can run java -jar submit.jar in the project directory. Your code can use any OCaml standard library functions that you like.

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 Integrity 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.