Project 2: SAT Solver Front-End

Due: October 4, 2018 11:59:59pm

Updates

• Project deadline extended until October 4th

• For consistency, we will use the instructor’s implementation of boolean.ml during grading. The submit server is already configured to test this way. For local testing, you can use this version of the test setup, which contains a pre-compiled boolean.cma for OCaml 4.03.0. Other versions of OCaml are not compatible. You can also continue using your own boolean.ml (from Project 1) for local testing.

• Added ^ to the list of left-associative operators in Part 1: Parsing

Introduction

In this project, you will implement a front-end for the Boolean constraint solver you 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 lexer and 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:

• &, |, +, and ^ 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, the operators & and ^ bind more tightly than +.

• A boolean literal can be either an integer (0, 1) or a keyword (true, false).

• 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, 1, false, or true), where : separates the identifier from its value. The assignment is delimited by [ and ]. Trailing commas are not allowed. For example, [], [a:1,b:0], and [a:true,b:false] 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.

• Conditional boolean expressions of the form ASST GUARD ? TEXPR : FEXPR; evaluate the boolean expression GUARD in the context of assignments ASST and, if true, returns the first (or "true") expression TEXPR. If GUARD evaluates to false, the second (or "false") expression FEXPR is returned.

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

  For example, bool x = forall x . x | y;; is valid.

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

    The above prints false.

  • bvec x = 0; bprint x;

    The above throws an exception in evaluating the bprint statement because x is not a boolean expression.

  • bprint x;

    The above 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;

    The above prints x followed by newline.

  • fv x & y;

    The above prints x, y followed by newline.

  • fv 1;

    The above 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;

    The above prints Unsat followed by a newline.

  • sat x & y;

    The above prints [x:1, y:1] followed by a newline.

• Statement int_of VEXPR; prints the integer corresponding to 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.)

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.

Web Accessibility