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

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.

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.

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