The Evergreen(r,s) Game for Life Scientists

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",
pages = "",
YEAR = 2007,
publisher = "Springer",
series = "LNCS",
}

This paper provides a translation of generic reaction networks to weighted maximum satisfiability. This page is about a game introducing life scientists to maximum satisfiability through our Evergreen game. To define the game, the following concepts are needed:

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

A weighted CSP formula is a set of weighted constraints. A weighted constraint is an integer weight, a Boolean relation of rank r and a set of r variables. A Boolean relation of rank r is defined by a Boolean formula involving r variables. An assignment for a weighted CSP formula H maps the variables of H to Boolean values. An assignment J defines a satisfaction fraction fsat(H,J) for a weighted CSP formula H: the weight of the satisfied constraints in H divided by the total weight 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 weighted CSP(G)-formula is a CSP formula that may only contain relations in G.

Examples:

Weighted CSP formula H:
100: NOT(x)
150:       NOT(y)
200: OR( x,    y)

Weighted constraint:
200 OR( x     y)

Variable
x

Boolean relation:
Or(x,)

Assignment J:
{x=1, y=0}

Satisfaction fraction:
fsat(H,J) = 350/450 = 0.78..

Weighted 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):

The game is named after our Evergreen Project.

Anna and Bob, the players, agree on a protocol P1 to 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. Anna chooses a CSP(G)-formula H with at most v_max=1000 variables. Bob solves H and gets paid by Anna the fraction times a million dollars that Bob satisfies in H. Anna will choose a formula that will minimize Bob's profit. Take turns. Bob will choose a formula and Anna solves it. The alternation of the game is: Anna: formula, Bob: solves, Bob: formula, Anna: 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.

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.

For G={R1,R2}, a formula H2 is:

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

and the maximum assignment is J2={A=0, B=1, C=0} which satisfies all but one constraint, i.e., the fsat(H2,J2) is 5/6.

What H should Anna choose for the G above? Should she use the full set CSP(G)-formula or should she limit herself to a subset?

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