13 Homework 8A

Due:

Tuesday, 2/27 at 9PM

This assignment may be done with an approved PARTNER.

This assignment is entirely AUTOGRADED.

What to Download:

hw8a.rkt

Please start with this file, filling in where appropriate, and submit your homework to the HW8A assignment on Gradescope. This page has additional information, and allows us to format things nicely.

13.1 Test Suites

LSL has support for named test suites. These allow code organization, and changes how errors are reported. More importantly, they allow us to give you better feedback on your test suites in out autograders. For this assignment, and all subsequent ones, you must put your unit tests for functions into the named test-suite blocks that follow the functions (usually, the blocks are named after the function). If you rename the block or put tests outside of the block, they will not be counted! These exist in the template file you download above.

13.2 Data representation

On the third day of class, we introduced the idea of representing propositional true / false values as boolean #t/#f values in LSL. This decision was somewhat motivated by built-in support for boolean operators like and and or, but some important propositional operators do not already exist (like implication). Just as we can define implication, we could have defined and if it did not already exist, so the choice of #t and #f, while convenient, was in some sense arbitrary.

Indeed, we could have, and in this set of problems, you will, define propositional truth values using many different representations, all of which work. For each, we will define a common set of operations, and use an existential type to create a common interface such that, in the end, you can use all interchangably. First, though, we’ll define a non-trivial program that uses an abstract interface to our truth values.

13.3 Problem 1

We first define an interface, which we will call TruthVal, for our propositional truth values. This includes two base values, called T and F, three operations AND, OR, and NOT, and a way of asking if a variable is True (so that, when we are done with dealing with abstract propositional values, we can move back to regular computation).

This will form an API (application programming interface) to using propositional values, irrespective of the actual values that are used underneath. This is an important idea, sometimes called "representation independence" (and is related to the software engineering concept of "loose coupling").

In this problem, we’d like you to start out with the interface by defining an instance of TruthVal where A is Boolean:

13.4 Problem 2

Now, we want to use our TruthVal. In this sequence of problems, we will make a naive (i.e., brute force) SAT solver. We will take, as input, formulas in conjunctive normal form (CNF), i.e., it is a conjunction (AND) of formulas that are themselves disjunctions (OR) of either variables or negated variables. We’ll represent the variables as natural numbers (imagine they are x0, x1, x2, etc). We’ll define the formulas agnostic of whether they have variables (i.e., (CNF VariableClause) or (Formula VariableClause)) or have a different value (e.g., (CNF Boolean), or some abstract value A, as in (CNF A)).

We’ll thus represent the input to the solver as:

We do not explicitly represent either the ANDs or the ORs because of the uniformity: the list of variables/negated variables in a Formula are all ORd together, and the list of Formulas in the CNF are all ANDd together.

Note: an empty CNF is (trivially) satisfiable!

To see if a formula is satisfiable, we’ll do several things. First, we need to figure out the variables that occur in our CNF. We’ll do this by calculating a natural number that is greater or equal to all variables in the CNF. If the CNF is empty, this is 0, otherwise, it should be the largest variable you find.

13.5 Problem 3

Next, we need a way of evaluating CNF formulas, where we’ve already replaced all the variables with abstract truth values. You can (and should!) test this function using your BOOL-TV above, and provide a (CNF Boolean)

So we want a function with the following signature / starter:

When you’re thinking about how to do this, think how to evaluate the expression (what has to be combined with OR, what with AND). Then, to actually do it, extract the corresponding function that works on the abstract TruthVal that you are given from the api argument.

13.6 Problem 4

Now we need a way of substituting for variables into CNF formulas. We’ll do this before calling eval. So we want a function with the following starter. Note that we still need the api, so we can do negation when we substitute for a negated variable.

Note: it’s fine to assume that: A. all variables k that occur in the (CNF Variable) (as either k or (make-n k)) occur in the vars argument. B. The vars argument contains no duplicates.

13.7 Problem 5

Finally, now that we can substitute and evaluate formulas (i.e., see if it is satisfiable), we need to be able to enumerate all possible assignments and check if there exists one that results in truth: this is the sat problem.

We’re providing you, as a helper function, all-tvs, which, given an arbitrary T and F value, and a maximum Variable (a Natural number), enumerates all possible combinations of the values as a list of lists. These are essentially the rows of a truth table, that you can then use as arguments to your earlier functions.

13.8 Problem 6

Since we have written all our code abstractly, we can now implement several other implementations of TruthVal. We’d like you define one with 1 and 0 as T and F respectively, one with strings (use "true" and "false"), one with custom structs ((define-struct true ()) and (define-struct false ())), and lastly, one that uses the anonymous function (lambda (x y) x) as T and (lambda (x y) y) as F (these are "Church booleans", named after Alonzo Church, one of the founders of computer science).

For each one, write at least one test of sat that uses this TruthVal as the implementation that will be used to perform the solving (if it’s not an interesting one, you may have to write several, as we are testing your test suites!). For the last, you’ll have to apply the result to two values and use the result of that, as check-expect (or any equality test) cannot compare function values. e.g., if you want to know if an expression e, which you know is a Church boolean, you could apply it to 1 and 2 (as (e 1 2)) and see if you get 1 (then you had the Church bool representing truth) or 2 (that means you had the Church bool representing falsehood).

It’s fine if the CNF you use is the same across these tests.