@inproceedings{TTKLL07:AB, author = "{A.~Tiwari and C. Talcott and M. Knapp and P. Lincoln and K. Laderoute}", title = "{Analyzing Pathways using SAT-based Approaches}", booktitle = "Proc. 2nd Intl. Conf. on Algebraic Biology, AB 2007", YEAR = 2007, publisher = "Springer", series = "LNCS" }The paper "Analyzing Pathways using SAT-based Approaches" is available from SRI.

This paper provides a translation of generic reaction networks to weighted maximum satisfiability. To define the game, the following concepts are needed:

Concepts: Boolean CSP formula constraint variable Boolean relation assignment satisfaction fraction fsat weighted CSP(G)-formulaA Boolean CSP formula is a non-empty bag of constraints. From now on, we simply use CSP formula instead of Boolean CSP formula. A constraint consists of an integer multiplicity, a Boolean relation of some rank r and a set of r variables. The multiplicity indicates how often the constraint appears in the bag. A Boolean relation of rank r is defined by a Boolean formula involving r Boolean variables. An assignment for a CSP formula H maps the variables of H to Boolean values. An assignment J defines a satisfaction fraction fsat(H,J) for a CSP formula H: the number of the satisfied constraints in H divided by the total number of all constraints H. A constraint is satisfied under asssignment J if the Boolean formula evaluates to true under assignment J. Let G be a set of relations. A CSP(G)-formula is a CSP formula that must only contain relations in G.

CSP formula H: 100: NOT(x) 150: NOT(y) 200: OR( x, y) The first constraint has multiplicity 100. Constraint: 200 OR( x y) The multiplicity is 200, OR is the relation and x and y are the variables. Variable x Only assumes Boolean values, represented by 1 and 0. Boolean relation: OR(x,y) Assignment J: {x=1, y=0} Satisfaction fraction: fsat(H,J) = 350/450 = 0.78.. CSP(G)-formula H is such a formula for G = {OR(x,y), NOT(x)}. G uses a relation OR of rank 2 and a relation NOT of rank 1.

The game is named after our Evergreen Project.

The Evergreen game is played by two players, Alice and Bob, that take turns creating and solving CSP formulae and paying each other a percentage of a wager based on the fraction of constraints they can satisfy. Let's the stake be 1 million dollars.

The players choose a set G of s Boolean relations of at most rank r. For example, they choose two relations of rank r randomly, except the all true and all false relations. Alice chooses a CSP(G)-formula H with at most v_max=1000 variables. Bob solves H and gets paid by Alice the fraction times a million dollars that Bob satisfies in H. Alice will try to choose a formula that will minimize Bob's profit. Take turns. Bob will choose a formula and Alice solves it. The alternation of the game is: Alice: formula, Bob: solves, Bob: formula, Alice: solves, for one round of the game. Then a new set of relations is chosen and Bob generates a formula, etc.

The variables used in a constraint must all be distinct, i.e., R(x,x,y) is not allowed.

Each player has a fixed amount of time for each move, say 2 minutes. If the player fails to move in that time, the cost is $ 1 million and the game starts with a new set of relations.

For larger games, such as Evergreen, the evaluation must be cut off after some limit. The states at the limit are then evaluated by estimating the score to be achieved by the relevant player, and these scores are propagated back up the search tree to provide an estimate of the value of each move. The cut-off and the evaluation need to take into account the horizon effect (are there unavoidable moves which will affect the score but are not being factored in because they have been pushed beyond the cut-off horizon?).

For the Evergreen game it is sufficient to look only a few moves ahead: Alice constructs, Bob solves, Bob constructs, Alice solves. With this horizon in mind, Alice should find a CSP formula that is hard for Bob and at the same time it will not be possible for Bob to find a CSP formula in which Alice can only satisfy a much smaller fraction of constraints than Bob could for Alice's formula.

Each player always tries to choose a formula that has the smallest "fractional payoff". If Bob thinks that Alice gave him the formula with the smallest "fractional payoff", he may give the same formula back to Anna. This results in a tie if Bob found a maximum assignment.

1: NOT(A) 1: NOT(B) 1: NOT(C) 1: OR(A,B) 2: OR(B,C)and gives it to Bob.

100: NOT(A) 150: NOT(B) 200: OR(A,B)and gives it to Alice.

Could Alice or Bob have played better? Should she use the full set of CSP(G)-formulas or should she limit herself to a subset?

Now choose a partner, and play the game yourself. It is a good experiential learning experience and you will run into some basic calculus exercises involving polynomials if you learn to play the game well.

You may use Nature as Alice and let Nature give you a CSP formula based on a biological pathway. When you give a CSP formula to Nature it might execute a pathway behind the formula to find a good assignment.

If you need help with playing the game well, the following paper The Evergreen Game contains the answers. However, this paper is not written at a level so that it can be understood with a basic mathematics for life sciences course.

Karl J. Lieberherr, CCIS, Northeastern University, March 2007