The paper:
http://www.ccs.neu.edu/research/demeter/papers/evergreen/cp07-submission.pdf
contains useful information about how to implement the
algorithmic players.

On page 7 of

http://www.ccs.neu.edu/research/demeter/papers/evergreen/cp07-submission.pdf

is a general description how to compute 
appmean[F](x) = E(Z(F,x)).

The product finishing algorithm can be summarized as follows:

Our product finishing algorithm
starts with a formula F and turns it 
into an equally satisfiable formula F'
for which the maximum biased coin has probability 0.

We can prove:
max [0<=x<=1] E(Z(F,x)) <= E(Z(F',0))

An equally satisfiable formula is one where some of the 
variables x have been replaced by 1-x (complemented).