Project 2

CSU 670 Fall 2007
Out: September 14, 2007
Due September 21, 2007

For this project we fill in the unspecified concepts from project 1. What was left unspecified was the concept of a type T of a derivative, the concept of raw material of type T and the concept of finishing the raw material with a certain quality.

Our raw material are Boolean formulas in conjunctive normal form (CNF). A CNF consists of a list of clauses. The same clause may appear several times: so our CNFs are a bag of clauses. Each clause consists of a list of literals. A literal is either a positive or a negative variable.

raw material = CNF = bag of clauses

The concept of finishing the raw material amounts to finding an assignment that satisfies many clauses (ideally it maximizes the number of satisfied clauses over all possible assignments). An assignment assigns true or false to each variable of a CNF. An assignment is represented by a clause: a positive literal means the variable is set to true, a negative literal means the variable is set to false. A clause is satisfied by an assignment if at least one literal in the clause is satisfied. A positive literal is satisfied if its variable is assigned true and a negative literal is satisfied if its variable is assigned false. The quality of an assignment is the fraction of satisfied clauses among the total number of clauses.

finished product = CNF plus assignment

We need to define the concept of type of a CNF. The type of a CNF says what types of clauses the CNF contains. The type of a clause is a pair: the first element is the length of the clause (the number of literals) and the second element the number of positive literals. The clause (a !b !c) is of type (3,1) and the clause (!a !b !c !d) is of type (4,0). The type of a CNF is the union of the clause types. For example the CNF ((a) (b) (c) (!a !b) (!b !c)) is of type ((1,1) (2,0)).

Note that when you buy a derivative you buy it based on its type and its price. So you will need to figure out whether a price for a given type is fair. The uncertainty you have is different than with the weather, or exchange rates.

uncertainty
-----------

weather:  how nice will the weather be?
knowledge to reduce uncertainty: model of weather behavior.

interest rates:  how high will the rate be?
knowledge to reduce uncertainty: model of economy behavior.

Specker Derivative Game: how much can I satisfy in the CNF I get?
knowledge to reduce uncertainty: model of CNF  

type of raw material = list of relations. Each relation is given by a pair of numbers.

Complete the object-oriented design from project 1 with the new information.

Write a program that checks that the fraction of satisfied clauses (the quality of the finished product) is stated correctly. To check this, you need to write a program that determines how many clauses are satisfied by a given assignment.

What to turn in: Your extended object-oriented design drawn by a tool. In addition your program that takes as input a game object and that computes the fraction of clauses satisfied by each CNF that appears in a finished derivative and that compares this number to the quality given in the input object.

Here is a good way to think of a finished product:

(
let a in 
  let !b in 
    cnf (
       (a !b)
       (!a b))

    cnf (
       (a !b)
       (!a b))

Step 1:
  let !b in 
    cnf (
      (b)
      sat) 

Step 2:
    cnf (
    ()
    sat) 
)