The Evergreen Game for Life Scientists

The Evergreen Game provides a gentle introduction to maximum satisfiability through construction and solution of problems. Maximum satisfiablity-based approaches are gaining prominence in analyzing biological pathways.

@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 needed for the Evergreen Game

For playing the game, an undergraduate course on Mathematics for Life Sciences is needed. Some concepts of discrete mathematics are needed to correctly execute the moves of the game. If you wish to win at the game, you need some basic calculus topics as well: analysis of functions (limiting behaviour, maxima and minima, locating zeros).

Concepts:
Boolean CSP formula
constraint
variable
Boolean relation
assignment
satisfaction fraction fsat
weighted CSP(G)-formula

A 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.

Examples of Concepts used in Evergreen

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.

Evergreen Game (r,s) Definition

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.

Thoughts about how to play the Evergreen game

The basic algorithm of game playing is minimax, in which each player chooses the move which minimises the maximum score the opponent can achieve. In her first move, Alice will minimize her loss assuming that Bob will play optimally. Alice's task is ``complex'' because her option includes the construction of a potentially large CSP formula for which it will be difficult for Bob to satisfy many constraints. The space of CSP formula's is a huge search space and Alice needs to think about what kind of MAX-CSP solver Bob might use and what kind of CSP formula she might get from Bob.

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.

Example for Evergreen(2,2)

As an example, the protocol P1 chooses the following set G={R1, R2} of relations (we could choose any pair of relations): R1(a) = NOT(a) and R2(a,b) = OR(a,b). This is an Evergreen(2,2) game.

Alice's first move: construct CSP formula

For G={R1,R2}, Alice constructs the CSP(G)-formula H1:

1: NOT(A)
1: NOT(B)
1: NOT(C)
1: OR(A,B)
2: OR(B,C)

and gives it to Bob.

Bob's first move: Bob solves

Bob finds the maximum assignment J1={A=0, B=1, C=0} which satisfies all but one constraint, i.e., the fsat(H1,J1) is 5/6 = 0.83... Bob gets paid 0.83 million by Alice.

Bob's second move: construct CSP formula

Bob constructs CSP(G)-formula H2:

100: NOT(A)
150: NOT(B)
200: OR(A,B)

and gives it to Alice.

Alice's second move: Alice solves

Alice finds the maximum assignment J2={A=1, B=0} which satisfies fsat(H2,J2) = (150+200)/450 = 0.78.. constraints. Alice gets paid 0.78 million.

Game outcome

Alice has lost 0.05 million.

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