This guide is not yet synchronized with the implemented system. For example, strengthening is only done through the quality.
This guide is written for teachers, editors, research program managers, employee recruiters, and software managers who want to use SCG to 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 are 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.
Instance = (n,k) Solution = binary decision tree valid: has n+1 leaves labeled 0, 1, ... n. ... quality: depth of decision tree / n
Instance = (n0,C) Solution = n valid(n0,n): n>n0 quality: irrelevant
Instance = indirected graph G = (V,E) Solution = subset S of V valid: S is independent set quality: |S|/|V|
Instance = X Solution = Y valid: y in Y(x)? quality: irrelevant
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*y7For 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.
Instance = (set of trees. Set M which is a subset of
the nodes of the Graph Cartesian Product (GCP) of the trees)
Solution = (Boolean: all leaves are covered/not all leaves are covered).
If not all leaves are covered an uncovered leaf must be provided
as witness.
valid = if witness is given, the witness must not be covered by (reachable from)
a node in M.
quality = 0 (all solutions have quality 0). Quality is irrelevant.
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.
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.
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/nstrengthenp(HSR(n,k)<=q0,HSR(n,k)<=q1) iff q0 > q1.
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/nstrengthenp(HSR(n,k)>q0,HSR(n,k)>q1) iff q0 < q1.
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)).
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))
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
setOfInstances = X q = irrelevant r = time protocol: Bob(x) Alice(y) defense = 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.
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.
The use of the Landau notation in this context requires some thought. The C and the n0 must be provided as part of the claim. This information could be used for strengthening so that a claim with a smaller constant would be stronger. But for now, the strengthening relation is always false.
Domain
Instance = raw material = (adult skin cells, 4 cancer causing genes, "standard" biochemistry lab.) Solution = beating heart cells valid = the heart cells are healthy and beat properly. quality = fraction of skin cells transformed, duration of using cancer causing genes.The claims are of the form: AdultSkinCellToHeartCellTransformation(Organism,transformed: 25%,use of cancer causing genes: 5 days, overall duration: 11 days) valid = the procedure does not produce pluripotent stem cells as an intermediary.
If the biochemical procedures can be simulated in silico, scholars may be avatars, otherwise scholars are humans. The refutation protocol consists of having the scholars perform the procedure they claim and to check the achieved quality and the resources consumed.
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.
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.
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)).
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.
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.
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.
What kind of generalization of predicate logic do we get with protocols with secrets?
The transition from ALL to SECRET in the MAX-CSP case is interesting. In the SECRET case, a refuter may be lucky and find the secret. What is the connection between PC and NC where NC is the negation of PC? Both might be refuted or defended. But one of them will be refuted more frequently? PC below the P-optimal threshold can be easily defended. Above the P-optimal threshold, it is not clear.