Homework 6

Due: Saturday, Feb 21st at 11:59pm

Replace each failwith "TODO" with your solution.
Be sure to test your solutions in utop or in tests alongside your submission. To load your file into utop, use #use "hw6.ml";;.
Submit your version of hw6.ml to the HW6 assignment on Gradescope. Only submit hw6.ml; NOT any other files or folders.
At the top of the template file, there is a comment for you to write in approximately how many hours you spent on the assignment. Filling this in is optional, but helpful feedback for the instructors.

Data representations and PBT

Recall from homework 1 that we introduced propositional logic to you, which can be naturally represented in OCaml as expressions of type bool:

let p1 a b c = a && (b || c)
let p2 a b c = (a && b) || (a && c)

We do not have an implication operation, but we can easily implement it either as a function, or even as an operator.

let impl a b = if a then b else true
let (==>) a b = not a || b

For this assignment we are providing a local Pbt module which includes helper functions that you can use when working with property-based testing. This will provide to you with forall as well as some combinators and simple generators which you can use when property based testing:

let test_equiv_p1_p2 () =
  forall (gen3 gen_bool gen_bool gen_bool) (fun (a, b, c) -> p1 a b c = p2 a b c)

let test_equiv_impl () =
  forall (gen2 gen_bool gen_bool) (fun (a, b) -> impl a b = a ==> b)

Just as we can define implication, we could have defined and if it did not already exist, so the choice of true and false, 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 abstract data type to create a common interface such that, in the end, you can use all inter-changably. First, though, we’ll define a non-trivial program that uses an abstract interface for our truth values.

Question 1

First, we will provide the TruthVal interface, for propositional truth values. This includes two base values, called tru and fls, three operations tand, tor, and tnot, and a way of asking if a value is "truthy" or "falsy" (so that, when we are done with dealing with abstract propositional values, we can move back to regular computation).

module type TruthVal = sig
  type t

  val tru : t
  val fls : t

  val tand : t -> t -> t
  val tor : t -> t -> t
  val tnot : t -> t
  val tif : t -> 'a -> 'a -> 'a
end

Implement TruthVal using booleans, and fill in the GenTruthVal module to generate arbitrary TruthVal values (tru/fls) as well as all possible expressions in the signature (when generating tif, return type t for the polymorphic 'a). As this will be a recursive function, we allow for an optional argument maxdepth that indicates the deepest level of recursion before return a terminal expression of tru or fls.

module BoolTruthVal : TruthVal = struct ... end

module GenTruthVal (T : TruthVal) = struct
  let rec gen ?(maxdepth : int = 20) : unit -> T.t = failwith "TODO"
end

Note

4 points (autograded) for the implementatino of BoolTruthVal 1 point (manually graded) for the implementatino of GenTruthVal

Question 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 (called literals):

type variable = int

type literal = 
  | Var of variable
  | NotVar of variable

We’ll represent the variables as natural numbers (imagine they are x0, x1, x2, etc) and we'll define the formulas polymorphic of whether they have variables or a different value (here a clause is a formula of literals OR'd together):

type 'a clause = 'a list
type 'a cnf = ('a clause) list

We use lists and do not explicitly represent the AND's or the OR's because of the uniformity: the list of literals (variables/negated variables) in a clause are all OR'd together, and the list of clauses in the CNF are all AND'd together.

Our goal will be to find out if we can find mappings from variables to booleans which will make our formula reduce to a true value. If we can, we say that the formula is satisfiable, "is SAT," or "has a satisfying assignment."

an empty CNF is (trivially) satisfiable and an empty clause is trivially unsatisfiable

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.

let variable_upper_bound (cnf : variable_clause cnf) : variable = failwith "TODO"

As an example, variable_upper_bound [[Var 0, NotVar 4], [Var 1]] should return 4.

Note

5 points (autograded)

Question 3

Next, we need a way of evaluating CNF formulas, where we’ve already replaced all the variables with abstract truth values. So we want a function with the following signature / starter:

module Eval (T : TruthVal) = struct
  let eval (cnf : T.t cnf) = failwith "TODO"
end

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.

Note

5 points (autograded)

Question 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 code.

Note

that we still need the API, so we can do negation when we substitute for a negated variable.

Note

Assume that the mapping always contains all variables used in the given CNF and that there are no duplicated variables in the mapping. You may want to look at the assoc function of the List module.

type 'a mapping = (variable * 'a) list

module Subst(T : TruthVal) = struct
  let subst (vars : T.t mapping) (cnf : variable_clause cnf) : T.t cnf =
    failwith "TODO"
end

Note

5 points (autograded)

Question 5

Finally, now that we can substitute and evaluate formulas (i.e., see if it evaluates to true or false), 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_assignments 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.

let all_assignments (vals : 'a list) (bound : variable) : (variable * 'a) list list =
  let open List in
  let rec go n =
    if n <= 0 then [[]] else
      let xs = go (n - 1) in
      let prepend_permutations ys = map (fun v -> (n - 1, v) :: ys) vals in
      concat_map prepend_permutations xs
  in
  go bound

let () =
  test_assert "assignments for 3 variables of a or b value" (
    all_assignments ["a"; "b"] 3 =
    [[(2, "a"); (1, "a"); (0, "a")]; [(2, "b"); (1, "a"); (0, "a")];
     [(2, "a"); (1, "b"); (0, "a")]; [(2, "b"); (1, "b"); (0, "a")];
     [(2, "a"); (1, "a"); (0, "b")]; [(2, "b"); (1, "a"); (0, "b")];
     [(2, "a"); (1, "b"); (0, "b")]; [(2, "b"); (1, "b"); (0, "b")]]) 

module Sat (T : TruthVal) = struct
  module E = Eval(T)
  module S = Subst(T)

  let sat (cnf : variable_clause cnf) : T.t =
    failwith "TODO"
end

Note

10 points (autograded)

Question 6

Since we have written all our code abstractly, we can 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"), and one with custom structs (type t = { value : unit list }).

module IntTruthVal : TruthVal = struct
  type t = int
  ...
end

module StringTruthVal : TruthVal = struct
  type t = string
  ...
end

module RecordTruthVal : TruthVal = struct
  type t = { value : unit list }
  ...
end

Note

3 points (manually graded)

Question 7

Finally, given that we have many different implementations of TruthVal it is important to know that, not only are these implementing the same specification, but we have an equivalence of implementation, up to the notation of isomorphism.

An isomorphism signifies a structural similarity, where two types can be transformed into one another without loss of information. In our context, given two truth value implementations represented as modules A and B, Implement the conv function to take an element from A and "convert" it into an element of B, alonside an "inverse" function inv that maps elements back from B into A.

An isomorphism is defined by the left and right inverse properties:

prop_leftinv says \(\(\forall a : A.t, inv (conv a) = a\)\)
prop_rightinv says \(\(\forall b : B.t, conv (inv b) = b\)\)

Implement these properties and complete check_iso to ensure that your properties are correct.

module TruthValIso (A : TruthVal) (B : TruthVal) = struct
  let conv (a : A.t) : B.t = failwith "TODO"
  let inv (b : B.t) : A.t = failwith "TODO"

  let prop_leftinv (a : A.t) = failwith "TODO"
  let prop_rightinv (b : B.t) = failwith "TODO"

  module GA = GenTruthVal(A)
  module GB = GenTruthVal(B)

  let check_iso : (A.t * B.t) option = failwith "TODO"
end

Note

6 points (autograded)