Project 4

CSU 670 Fall 2007
Out: September 30, 2007
Due October 5, 2007
This subproject consists of 2 parts: Product Finishing and Transition System for SDG.

Product Finishing

Product Finishing Part 1

To play the Specker Derivative Game well, we need to solve the following sub problem:
Input: CNF F with weighted clauses
Output: Assignment M
Postcondition: The more weighted clauses M satisfies in F, the better.
Ideally we would like to have an M that maximizes the fraction 
of satisfied clauses.

This is a generalization of the famous Satisfiability problem (SAT) and is called the MAXSAT problem (MaxSat and MAX-SAT are also used as abbreviations). Over the last 30 years researchers, including your professor, have developed practically useful algorithms called SAT and MAXSAT solvers.

The importance of SAT and MAXSAT solvers is documented by several websites and conferences, e.g., http://www.satlive.org/. Application domains are: program verification, electronic design automation, optimal planning, Bayesian network inference, computational biology and chemistry, etc. For us in CSU 670, the most important application of MAXSAT solvers is to play the Specker Derivative Game well to win the SDG competition.

There are two options to solve MAXSAT: 1. to use one of the existing solvers, such as Toolbar and Yices from SRI that both have won international competitions. 2. to implement our own MAXSAT solver.

We choose the second option in this project. The behavior of a large class of SAT and MAXSAT solvers can be explained in terms of state transition systems. You have seen simple forms of state transition systems in your Theory of Computation class: Automata are a simple form of a state transition system. See:

http://en.wikipedia.org/wiki/Labelled_transition_system

The transition rules below describe at a high level the basic capabilities that your algorithms must have but it is left to you 1. how to implement those basic capabilities; 2. how to sequence those basic capabilities.

View this document as a requirements document written by a user who wants to influence at a high level of abstraction the algorithms that are used. In principle, the requirement document could just say: Implement a MAXSAT Solver which takes input according to class dictionary In and produces output according to class dictionary Out.

The state of the transition system has 4 components: M: a partial assignment, F: the CNF formula, N: the currently best complete assignment (a finished product) and a coin bias b that we use to generate random flips of the assignments to variables in N.

M | F | N | b

unsat(M,F) is the fraction of clauses in F that are unsatisfied under partial assignment M.

The initial state and the rules are as follows:

Initial State:
{} | F | N | b
where b is a coin bias and
where N is the all 0 assignment (could be any other assignment).

Decide:
D: M | F | N | b -> Mk | F | N | b
if literal k is not in M and v(k) occurs in some constraint in F.
k=!N(v(k)) with probability b.
k=N(v(k)) with probability 1-b.

N(v(k)) is the literal that represents the assignment by N to v(k).

v(k) is the variable corresponding to the literal k.
Explanation: Mk stands for the assignment M (a set of literals) to which literal k has been added. b is the probability for flipping the assignment for v(k). We flip it with probability p.
Update:
M | F | N | b -> M | F | M | b
if M is complete (all variables assigned) and unsat(M,F) < unsat(N,F).

Finale: (final transition)
M | F | N | b -> M | F | N | b
if unsat(N,F) = 0 or Restart was repeated enough times with the same bias b.

Restart:
M | F | N | b -> {} | F | N | b_new
where b_new is a new bias.

Informal:
With restart we can forget the partial assignment we have tried
and start from scratch.

Transition sequence:

(Restart Decide* [Update])* Finale

Let c = 40.
The plan is to try bias b = 0 0.1 0.2 0.3 0.4 0.5 0.6 0.7 0.8 0.9 1.0.
For bias b <= 0.5 we make (b*c)+1 Restarts.
For bias b >  0.5 we make ((1-b)*c)+1 Restarts.

This approach will guarantee, with high probability, that you find an assignment that does not make you lose money if you have bought the derivative at the right price.

Example:
CNF F (all weights are one):
1+2,3+4,5+6,!1+!3,!1+!5,!3+!5,!2+!4,!2+!6,!4+!6
N = all false, b=0.2
The type of the CNF is: (2,2) (2,0).

Initial state:

{} | F | N | 0.2 
unsat(N,F) = 3/9

6 Decide:

{1} | F | N | 0.2
{1 !2 } | F | N | 0.2
{1 !2 !3 } | F | N | 0.2
{1 !2 !3 !4 } | F | N | 0.2
{1 !2 !3 !4 !5 } | F | N | 0.2
{1 !2 !3 !4 !5 !6} | F | N | 0.2

Now update applies because fewer clauses are unsat.

Update:
{1 !2 !3 !4 !5 !6} | F | N | 0.2 ->
{1 !2 !3 !4 !5 !6} | F | {1 !2 !3 !4 !5 !6} | 0.2

So the new N is: {1 !2 !3 !4 !5 !6}

Restart:
M | F | N | 0.2 -> {} | F | N | 0.2
unsat(N,F) = 2/9

6 Decide:

{1} | F | N | 0.2
{1 !2 } | F | N | 0.2
{1 !2 !3 } | F | N | 0.2
{1 !2 !3 !4 } | F | N | 0.2
{1 !2 !3 !4 !5 } | F | N | 0.2
{1 !2 !3 !4 !5 6} | F | N | 0.2


Now update applies because fewer clauses are unsat.

Update:
{1 !2 !3 !4 !5 6} | F | N | 0.2 ->
{1 !2 !3 !4 !5 6} | F | {1 !2 !3 !4 !5 6} | 0.2

So the new N is: {1 !2 !3 !4 !5 6}

Restart:
M | F | N | 0.2 -> {} | F | N | 0.2
unsat(N,F) = 1/9

This turns out to be the maximum assignment but we don't need to provide a proof.
Choose another CNF and work it through the transition system. Turn in your transition sequence as a text file.

Product Finishing Part 2

Implement the Decide rule and apply it until it can no longer be applied. With this implementation you implement the generation of a random assignment with a coin of bias b.

Product Finishing Part 3

Implement the complete transition system and implement the desired transition sequence. With this implementation you implement the generation of several random assignments with a coin of bias b and you choose the best assignment.

Product Finishing Part 4

Iterate through different probabilities b, as described earlier. Keep the history of the transitions that your implementation makes. Turn in your program complete with test cases.

Transition System for SDG

SDG consists of a sequence of transitions. Is a transition system an appropriate formalism to describe the mechanics of SDG? Turn in your evaluation with at least 5 transition rules. Example: Consider the following transitions:
Borrow transition

P1*[account a1, credit a2] request_to_borrow(P1,a3)
->
P1*[account a1+a3, credit a2+a3]
Buying transition

P1*[account a1] P2[account a2] S[offer d1 P2 c] 
->
P1*[account a1-c] P2[account a2+c] S[buyer P1 offer d1 P2 c] 
provided a1-c >=0.
P1 buys derivative d1 from P2 at price c.
Raw material delivery transition

P1 P2* S[buyer P1 offer d1 P2 c] 
->
P1 P2* S[raw mat F buyer P1 offer d1 P2 c] 
Finished material delivery transition

P1*[account a1] P2[account a2] S[raw mat F buyer P1 offer d1 P2 c]
->
P1*[account a1+fsat(M,F)] P2[account a2-fsat(M,F)] S[finished M raw mat F buyer P1 offer d1 P2 c]
provided a2-fsat(M,F) >= 0.
In English: Player P1 has finished the raw material F resulting in M with quality fsat(M,F). P1's account is increased and P2's account is decreased.
Finished material delivery transition (variant)

Finish: d1
P1*[account a1] P2[account a2] S[raw mat F buyer P1 offer d1 P2 c]
->
let pay(d1,M,F) = fsat(M,F) > d1.c ? 1 : 0;
P1*[account a1+pay(d1,M,F)] P2[account a2-pay(d1,M,F)] S[finished M raw mat F buyer P1 offer d1 P2 c]
provided a2-pay(d1,M,F) >= 0.

Explanation of symbols:

P1, P2: Players, P1*: it is player P1's turn
S : Store containing information about the state of all derivatives
[ ] : defines relevant information
offer d1 P2 c: derivative d1 sold by P2 at price c
account a1-c: deduct c from account a1
fsat(M,F): fraction of clauses satisfied by M in F
General form of a state transition for an SDG move: MOVE(parameters) PlayerInfo1 PlayerInfo2 StoreState1 -> PlayerInfo3 PlayerInfo4 StoreState2 provided predicate Transition system can be used for testing a player.