Project 4

CSU 670 Fall 2007
Out: September 30, 2007
Due October 5, 2007

Product Finishing

Product Finishing Part 1

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.

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.

Product Finishing Part 2

Product Finishing Part 3

Product Finishing Part 4

Transition System for SDG

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.

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.

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