Scientific Community Game Playground Designer Guide

version 0.4

This guide is written for teachers, editors, research program managers, recruters, and software managers who want to use SCG and define new playgrounds and to call for games taking place in those playgrounds. The playground is to be used by students, researchers, potential employees and software developers with their avatars. The intent is to educate, innovate (through crowd sourcing of small intelligent crowds), or evaluate. SCG is parameterized by a domain D and a set of claims based on D.

The playground designs described are submitted to SCG Game Courts to define a new game to take place in the Game Courts. Students either register themselves or their avatars for the next tournament to determine who has the best skills.

The definition of a playground includes: (1) a domain definition that specifies the problem to be solved, (2) a claim set definition with a strengthen relation. The claims specify how well (niches of) instances of the problem are claimed to be solved, including a refutation protocol that precisiely defines successful refutation of a claim in the sense of Karl Popper. A strengthen predicate on pairs of claims defines an implication relationship on claims. Karl Popper's ideas a reasonably summarized here (from Carla Fehr's web page): http://www.ccs.neu.edu/home/lieber/evergreen/specker/scientific-method/Popper-Carla-Fehr.html

There are two kinds of SCG: SCG/Avatar (where avatars developed by humans play the role of scholar) and SCG/Board (where humans play the role of scholar). This document is written for SCG/Avatar but much of it also applies to SCG/Board.

Domain

A domain is a 4-tuple: (Instance, Solution, valid, quality) where Instance and Solution are sets. valid is a relation between Instance and Solution and quality is a function that assigns an element of Instance and Solution a number in [0,1].

Computational Problems and Instances

A computational problem can be viewed as an infinite collection of instances together with a solution for every instance. The input string for a computational problem is referred to as a problem instance (which we abbreviate to instance), and should not be confused with the problem itself. A problem refers to the abstract question to be solved. In contrast, an instance of this problem is a rather concrete utterance, which can serve as the input for a decision problem. For example, consider the problem of primality testing. The instance is a number and the solution is "yes" if the number is prime and "no" otherwise. Alternately, the instance is a particular input to the problem, and the solution is the output corresponding to the given input.

Example HSR

Playing in this playground enhances the following skills: Constructing decision trees, applying linear and binary search, generalizing information-theoretic lower-bound arguments, memoization, dynamic programming, storage minimization in dynamic programming, perspective change. Important concepts that are used: recurrence relation, binomial coefficients, Pascal's triangle (modified), induction, function optimization, calculus (asymptotic analysis).
Instance = (n,k)
Solution = binary decision tree
valid: 
  has n+1 leaves labeled 0, 1, ... n.
  ...
quality: depth of decision tree / n

Example Landau (O notation)

Learning asymptotic analysis.
Instance = (n0,C)
Solution = n 
valid(n0,n): n>n0
quality: irrelevant

Example Independent Set

Algorithms for independent set problem.
Instance = indirected graph G = (V,E)
Solution = subset S of V 
valid: S is independent set
quality: |S|/|V|

Domain for mathematical Claim: ForAll Exists

ForAll x in X Exists y in Y(x): predicate(x,y). It is known for a long time http://www.ccs.neu.edu/home/lieber/courses/algorithms/cs4800/f10/resources/quantifiers.pdf how quantifiers connect with games. The refutation protocol is determined directly by the quantifiers.
Instance = X
Solution = Y
valid: y in Y(x)?
quality: irrelevant

Example Boolean MAX CSP

Instance = CSP formula = set of integer weighted constraints using Boolean relations.
Solution = assignment to the variables in a CSP-formula.
valid: Every constraint in an instance must contain distinct variables. Assignment is total.
quality: fraction of satisfied weighted constraints.
There is more to be said about the domain definition. The playground designer must choose a representation for the relations. It could be a truth table defining a Boolean relation but truth tables are not concise. The playground designer could choose an encoding of Boolean relations into integers. Let's use this alternative.

The playground designer wants to provide the avatars with a convenient infrastructure which they need for solving the instances and which the playground designer needs anyway to implement the valid and quality functions. To implement the quality function, the playground designer needs to evaluate a constraint R(x1,x2,...) for a given Boolean assignment to the variables x1,x2,.... The playground designer decides that all relations must be of arity 3 and the playground designer decides to offer incremental evaluation of a relation. For example, the relation R(x1,x2,x3) simplifies to R1(x1,x2,x3) after setting x1=1 and to R2(x1,x2,x3) after setting x1=1 and x2=1 and to R3(x1,x2,x3) after setting x1=1 and x2=1 and x3=0.

The playground designer decides to use a class Relation with the method:

int reduce(int variablePosition, int value) 
This method can be conveniently used to evaluate a constraint. After all variables are reduced to 0 or 1 (false or true), we get either the relation "always true" or "always false".

The playground designer decides on a specific encoding of the relations of arity 3. There are 2^(2^3)= 256 such relations. An encoding of a relation is a natural to number between 0 and 255. 0 is "always false" and 255 is "always true".

x3 x2 x1  R(x1,x2,x3)
0  0  0   y0
0  0  1   y1
0  1  0   y2
0  1  1   y3
1  0  0   y4
1  0  1   y5
1  1  0   y6
1  1  1   y7

The integer for the relation R is:
y0 + 2*y1 + 4*y2 + 8*y3 + 16*y4 + 32*y5 + 64*y6 + 128*y7
For example, the relation 1-in-3 is represented by the number 22 = 16 + 4 + 2.

The implementation of the valid predicate is also easy: Every constraint must reduce to either 0 or 255 after the assignment (the solution) is applied. The playground designer decides to offer many more classes, interfaces and methods to simplify the life of the avatar implementors:

http://www.ccs.neu.edu/home/lieber/courses/software/IR-2.0/doc/

To summarize the MAX-CSP-secret playground experience: The playground designer must define suitable abstractions to implement the quality and valid functions. Along the way, the playground designer should provide a simple infrastructure for its own use as well for the use by the avatars.

Claim(Domain)

A claim set for a domain is defined by a protocol used to define a successful refutation. A claim in the set defines data that is used by the protocol and to define a subset of all instances in D.Instance. A claim in the claim set has the form: (i1,i2,...;p1,p2,...;q;r), where i1,i2,... are used to define a set of instances, called setOfInstances, p1,p2, are data for the protocol, q in [0,1] is a quality and r is a positive integer representing some resource. The intuition behind using setOfInstances is to make claims about a subset of the instances of a computational problem. It is often the case that in some application domains the instances have a special form, they are in a niche, and this niche can sometimes be exploited algorithmically.

It is important that claims don't have to be mathematical. Mathematical claims are expressed in predicate logic and potentially we can prove them to be either true or false. Because we need a more powerful notion of claim to make SCG interesting we define a claim using a general protocol to determine whether a refutation is successful, in the sense of Karl Popper.

A protocol consists of a data gathering algorithm involving Alice and Bob and a predicate that determines the outcome of the refutation protocol. The data gathering algorithm is of the form (Alice (data) Bob(data))+ or (Bob(data) Alice(data))+. The predicate gets all the data for evaluation. We distinguish between defense and refutation predicates. Alice always makes the claim and Bob tries to refute.

Strengthen Relation

Besides the domain and claim set definitions, a third important component is the strengthenP relation which is a relation between two claims. strengthenP(C1,C2) means that claim C2 is stronger than claim C1.

Example HSR: claims and strengthening

positive: HSR(n,k) <= q

setOfInstances = (n,k) (singleton)
q = number of questions needed / n
protocol:
  Bob((n,k)) Alice(decision tree DT for n,k)
  defense = valid((n,k),DT) and depth(DT) <= q/n
strengthenp(HSR(n,k)<=q0,HSR(n,k)<=q1) iff q0 > q1.

negative: HSR(n,k) > q

setOfInstances = (n,k) (singleton)
q = number of questions needed
r = irrelevant
protocol:
  Alice((n,k)) Bob(decision tree DT for n,k)
  refutation = valid((n,k),DT) and depth(DT)<= q/n
strengthenp(HSR(n,k)>q0,HSR(n,k)>q1) iff q0 < q1.

Example Landau (O notation)

positive: f(n) in O(g(n))

Math: Exists n0,C ForAll n>n0: f(n)<=C*g(n)
setOfInstances = {(n0,C)} 
q = irrelevant
protocol:
  Alice(n0,C)) Bob(n)
    defense = valid(n0,n) and f(n) <= C*g(n)
strengthenP(f(n) in O(g0(n)), f(n) in O(g1(n))) iff g1 grows asymptotically slower than g0. g1 grows asymptotically slower than g0 iff g1(n) in O(g0(n)) and g1(n) !in Theta(g0(n)).

negative: f(n) !in O(g(n))

Math: ForAll n0,C Exists n>n0: f(n) > C*g(n)
setOfInstances = {(n0,C)} 
q = irrelevant
protocol:
Bob (n0,C)) Alice(n)
refutation = n>n0 and f(n) <= C*g(n)

Exercises:
HSR(n,2) in O(n)
HSR(n,2) not in O(log(n))
HSR(n,2) in O(n^(1/2))
n^(1/2) not in O(log(n))

Example Independent Set

positive: Bob can efficiently approximate Alice' solution within 0.9.

Approximate secret solution.
setOfInstances = {G=(V,E)} 
q = 0.9 of secret solution
r = running-time <= |E|^2
protocol:
Alice (G=(V,E),secret sA = Alice' solution) Bob(sB = Bob's solution)
defense = |sB|/|sA| >= 0.9

Mathematical Claim: ForAll Exists

positive

ForAll x in X Exists y in Y(x): predicate(x,y).
setOfInstances = X 
q = irrelevant
r = time
protocol:
  Bob(x) Alice(y)
  defense = predicate(x,y)

negative

Exists x in X ForAll y in Y: !predicate(x,y).
setOfInstances = X 
q = irrelevant
r = time
protocol:
  Alice(x) Bob(y)
  refutation = predicate(x,y)
Both HSR and Landau are mathematical claims.

Example Boolean MAX CSP

The claim set consists of positive claims of the form MAX-CSP-secret-pos({R1,R2, ...}, quality0, resource0) and a claim has the intutive meaning: Alice claims that she can come within q of the quality that Bob can achieve. A stronger claim means that its quality is higher.

The claim set consists of negative claims of the form MAX-CSP-secret-neg({R1,R2, ...}, quality0, resource0) and a claim has the intutive meaning: Alice claims that Bob can't come within q of the quality that Alice can achieve. A stronger claim means that its quality is lower.

In both cases only instances that use the relations {R1,R2, ...} may be used.

The refutation protocol for MAX-CSP-secret-pos is: Alice offers. Bob decides to refute. Bob provides CSP-formula F using only [R1,R2,...]. Bob provides his secret solution SB. Alice provides her solution SA. Refutation is successful iff quality(F,SA) < quality0 * quality(F,SB) and valid(F,SA) and valid(F,SB) and Alice spends less than resource0. In summary:

Bob(CSP formula F, secret solution SA for F)
Alice(solution sB for F)
Refutation successful iff valid(f,SA) and valid(f,SB) and quality(f,SA) < quality0 * quality(f,SB) and Alice spends less than resource0.

The refutation protocol for MAX-CSP-secret-neg is: Alice offers. Bob decides to refute. Alice provides CSP-formula F using only [R1,R2,...]. Alice provides her secret solution SA. Bob provides his solution SB. Refutation is successful iff quality(F,SB) >= quality0 * quality(F,SA) and valid(F,SA) and valid(F,SB) and Bob spends less than resource0.

Protocol Negation and Complement of a Claim

The above examples illustrate how to negate claims in general, even non-mathematical claims. In many applications we want to have positive and negative claims to solve the instance from both directions, e.g., finding lower bounds and upper bounds.

Alice' claim C1-pos(setOfInstances, q, r) means that if Bob gives her an instance p in setOfInstances she will find a solution of quality q using resources r.

The complement of this claim is: C1-neg(setOfInstances,q,r) means that Alice can find an instance p in setOfInstances so that Bob cannot find a solution y of quality q within resource bound r. Note that such a solution y might exist but the calim says that it is "hard" to find.

protocol C1-pos:
  Bob(x) Alice(y)
  defense = predicate(x,y)
is translated into
protocol C1-neg:
  Alice(x) Bob(y)
  refutation = predicate(x,y)
The simple rule for claim negation is: the domain stays the same and, in the protocol, the roles of Alice and Bob are reversed and a defense is changed into a refutation.

Special case: Mathematical claims and accidental defenses and refutations

We say that Alice is perfect, if she is perfect at playing the game. She optimizes her chances to win. We use the notion of a perfect scholar to make statements about true and false claims.

Alice claims C, Bob tries to refute. Claim is of the form: Exists x in X ForAll y in Y(x): p(x,y). Refutation protocol: Alice provides x, Bob provides y.

If C true and Bob refutes, then Alice is careless. We call this accidental refutation.

If Alice defends C, and Bob is perfect then C is true.

If Bob refutes C, and Alice is perfect then C is false. Bob found a counterexample.

If C is false and Alice defends, then Bob is careless. We call this an accidental defense.

Alice claims C, Bob tries to refute. Claim is of the form: ForAll x in X Exists y in Y(x): q(x,y). Refutation protocol: Bob provides x, Alice provides y. The analysis is similar to the one above.

"If Bob perfect, we have a proof that C is true." can be replaced by: "the stronger Bob is, the more likely it is that the claim is true." A similar statement applies to Alice.

Baby Steps Towards Proofs

A successful defense is a baby step towards a proof of the defended claim. A successful refutation is a baby step towards a proof of the negation of the refuted claim.

For EA claims: a successful defense might be a big step towards a proof. For AE claims: a successful refutation might be a big step towards a proof of the negation.

Consider the following scenario: You and your partner play with claims C and !C. C always gets defended while !C always gets refuted. This is an indication that you should try to prove C. Example: n^(1/2) in O(n/log(n)).

Careless Scholars

The playground designer has to decide how to deal with careless scholars. Careless scholars cloud the picture of what is true and what is false and therefore we want to discourage careless scholars in the virtual world of SCG.

How can carelessness happen in HSR? Alice claims HSR(9,3)<=3 which is a wrong claim. Alice defends it because Bob does not find the bug in Alice decision tree. But the Admin will find the bug and kick Bob out of the game. It is a violation of SCG rules not to compute valid and quality correctly. Alice' reputation is reduced before Bob is kicked out.

Avoidable Accidental Defenses

There are two kinds of avoidable accidental defenses. Both are related to erroneous evaluation of the valid predicate or quality function.

Avoidable Accidental Defense of False Claim

Alice claims HSR(9,2)<=3. Bob tries to refute but is careless: Alice gives him the decision tree but he fails to check it carefully for validity or he miscalculates the depth to be 3. Therefore Alice defends her claim and this is an example of an avoidable accidental defense because HSR(9,2)<=3 is a wrong statement.

Avoidable Accidental Defense of True Claim

For an accidental defense of a true statement, consider the claim HSR(11,2)<=4 which is true. Alice provides her decision tree but she miscalculates the depth to be 4 when it is actually 5. Bob does not notice and Alice defends successfully. Bob will be kicked out of the game. Alice reputation is reduced (because she did not defend her claim) before Bob is kicked out.

In the SCG/Board, the TA or the SCG/Board tool deducts points for carelessness and in SCG/Avatar, it is the administrator that detects an SCG rule violation and kicks the avatar out of the game.

Skill-related Accidental Defense and Refutation

Defense of False Claim

Alice makes the false claim that in any 2-CNF she can satisfy 0.9 of the clauses. Bob refutes and gives Alice a cnf in which she satisfies 0.95 of the clauses. Alice defends her wrong claim. She could defend because Bob was not skillful in giving Alice a harder cnf. It might also be hard to find such cnfs. Bob should not refute if he does not have a hard cnf? Maybe his solver could not do better. This is not detected by the Admin and it is a problem for the scientific community. The game should be designed in such a way that the same claim may be refuted multiple times against distinct opponents so that accidental defenses and refutations will be uncovered. The reputation system is designed in such a way that Alice will make big reputation gains against a weak Bob. Some of this gain may come from defending false claims but it is more likely to come from defending true claims or refuting Bob's false claims.

Refutation of True Claim

Alice makes the true claim that in any 2-CNF she can satisfy 0.7 of the clauses. Bob refutes and gives Alice a cnf in which she satisfies only 0.6 of the clauses. So the true claim is refuted. The reason is that Alice was not skillful to find the assignment with the quality she predicted. This is not detected by the Admin.

Protocol Kinds

pi = problem instance, s = solution

Standard Positive

Bob(pi) Alice(s)

Standard Negative

Alice(pi) Bob(s)

Secret Positive

Bob(pi secret sB) Alice(sA)

Secret Negative

Alice(pi secret sA) Bob(sB)

Renaissance

Alice (pA) simultaneous Bob(pB)
Alice (spB) Bob(spA)
repeat 10 times
The one who has solved the most problems, wins.

Baby Avatar Generation

For generating a baby avatar out of a domain, claim set and strengthening predicate definition, a few more functions are requested from the playground designer. Those functions should make the baby avatar survive for a little while in the virtual scientific community without violating a rule. The baby avatar may lose reputation rapidly. The baby avatar needs a propose function to generate a new claim: Claim propose(List(Claim). It needs a "Boolean WantToRefute(Claim)" predicate to decide whether to refute a given claim (default = random). It needs a "Claim WantToStrengthen(Claim)" function to decide whether to strengthen a claim and how to strengthen it. It needs a "Boolean WantToAgree(Claim)" predicate to decide whether to agree with a claim (default = random). It needs a "Solution solveInstance(Instance)" function to solve a given instance. It must generate a solution that is valid but the quality may be bad. It needs a "Instance provideInstance(Claim)" function to provide a "hard" instance for a given claim.

Subsystems

Admin Generation

Input: Domain, Claim Set Definition, StrengthenP. Output: Administrator that can run multiple games in a tournament in parallel.

Baby Avatar Generation

Generates a working avatar that is likely to lose reputation quickly.

Protocol Management

We need a protocol interpreter that overlays the protocols between Alice and Bob to minimize communication.

Registration of Avatars

Reuse current registration system?

Checking Playground Designs

It is easy to make mistakes in playground designs which will produce unusable administrators and baby avatars. For example, the protocols must be well-defined, i.e., they correctly collect the data needed in the refutation predicate.

An Extensional Version of SCG with Dynamic Difficulty Adaptation

SCG/Avatar is symmetric: Avatars choose the claims they propose from an intensionally defined, potentially infinite set of claims. In some scenarios it is useful to limit the power of the avatars and only let them choose from a limited set of claims. In the simplest form, there is a positive claim PC and its negated negative claim NC. No strengthening is possible.

Lemma: Defending versus Refuting Complement

Defending a claim PC has the same difficulty as refuting its complement NC.

Proof:

Alice proposes PC. Alice defends claim PC against Bob, i.e. he tries to refute. Bob provides an instance IB and Alice solves it with SA. refute(IB,SA).

Bob proposes NC. Alice tries to refute. Bob provides instance IB and Alice solves it with SA. refute(IB,SA)

Alice: (propose PC) Bob must refute or agree. If Bob refutes: he provides instance and Alice solves it If he agrees: Bob must refute NC

Reputation:

Social welfare:
initially it is not known whether PC or NC is true. Over time, one will be preferred.

Win points: if refute: successful refutation; if agree: Bob loses points if he cannot refute the complement

if Bob agrees and he cannot refute the negation: or should he defend PC against Alice

still zero sum?

Example:
PC/NC pair.

Alice 100/Bob 100, the game is zero-sum.
Alice proposes PC because she thinks it is true. Bob tries to refute and succeeds. 
Alice -10% of Alice/Bob + from Alice
Bob proposes NC because he thinks it is true. Alice tries to refute and does not succeed.
Alice -10% of Alice/Bob + from Alice
Alice proposes NC because she thinks it is true. Bob tries to refute and does not succeed.
Alice + from Bob/Bob -10% of Bob
Bob proposes NC because he thinks it is true. Alice agrees. She must propose NC and Bob must refute. Alice defends NC.
Alice +0/Bob +0 (because proposing and refutation were forced)
if Alice would not have defended NC: Alice -10% of Alice/ Bob + from Alice

Bob made more reputation points because he zeroed in on the correct answer and a strategy to defend before Alice.

Note that it is conceivable that the refutations or defenses were accidental.

NC is the winner. Alice and Bob sit together and write down a winning strategy for defending NC. The winning strategy
is equivalent to a proof.

Generalization of predicate logic

Claims and protocols that come from alternating predicate calculus formulas are of course the usual mathematical claims. Having a defense strategies for those claims