Searching for wins as a constraint satisfaction problem I: Ruminations on a constraint language

I'm just now returning to some ideas that I had while in Indonesia at LPAR-17 about viewing the search for wins (which in this post, unless otherwise indicated, will be ambiguous between “winning play” and “winning strategy”). My question:

Can we profitably view the search for wins as constraint satisfaction problems?

The current code does implement a primitive kind of constraint satisfaction procedure as follows: the constraint variables are

• PLAYER, the player of the move,
• STATEMENT, the statement (i.e., formula or symbolic attack) to be asserted by PLAYER,
• STANCE, the stance (attack or defend) that PLAYER will take,
• REFERENCE
, the number of the move to which this move is a response.

The constraints are simply Lisp predicates in whose definitions PLAYER, STATEMENT, STANCE and REFERENCE are free (Lisp) variables. Testing whether a constraint is satisfied just means assigning the values specified by a candidate solution to the Lisp variables in the predicate, and then simply evaluating the predicate. Given some dialogue ruleset R and a sequence ⟨s₁,…s_n⟩ of moves, we then simply enumerate all possible values for PLAYER, STATEMENT, STANCE, and REFERENCE that satisfy all the constraints. The current approach is less than ideal for several reasons:

• the enumeration of possible values for the variables is brutish: we simply enumerate all possible values for each of the contsraint variables: STANCE ∈ {Attack,Defend}, PLAYER ∈ {P,O}, STATEMENT ∈ sub(φ) ∪ {?_L,?_R,?}, REFERENCE ∈ [0,…n], and check whether all constraints are satisfied. This obviously blows up, as the game proceeds (the domain of the variable REFERENCE grows).
• no techniques from constraint solving are used (there's no propagation, consistency checking, etc).

So as it stands, only in the most primitive sense can it be said that we use constraint solving techniques to search for wins, and that's being charitable. Let's stick with these constraint variables—PLAYER, STATEMENT, STANCE, and REFERENCE—and see what kinds of issues come up.

• The variable PLAYER has only two possible values. Actually, the only reason why I even consider this to be a variable that varies at all is because I was interested in exploring dialogue rulesets in general, including rulesets that permit, say, a player to take multiple moves. This perspective is interesting, but so far nothing has come of it in my research (I haven't taken any steps to see what happens when players can take multiple turns). In the interest of performance, then, one could limit the generality of my approach and consider only alternating games. In that case, the value of the PLAYER constraint variable is always determined by the number of the move we're at, and it could be deleted. (Note that doing this would cut down by one half the number of possible moves to consider, which is nothing to sneeze at.)
• The observation that PLAYER takes on only two possible values led me to wonder about encoding part of the constraint satisfaction problem as an instance of SAT. We could conceivably encode the entire search for wins as a SAT problem, but I digress.
• With these four variables (or three, if we ditch PLAYER), what are the constraints? What's a suitable representation of dialogue rules? Let's look at an example. Felscher's dialogue rule D10 says: “P may assert an atomic formula only after it has been asserted by O before”. We might naively represent this in a first-order way using our constraint variables thus:

  PLAYER = P ∧ atomic(STATEMENT) → [ ∃k (k < ⟨TURN⟩ ∧ player-at(k) = O ∧ statement-at(k) = STATEMENT) ]

  This is a bit of a mess. Evidently we'll need the predicate "atomic", which can be applied to the variable STATEMENT to require that STATEMENT is an atomic formula. “⟨TURN⟩” isn't really a constraint variable, but is a parameter whose value comes form outside, as part of the specfication of the CSP. player-at is a function of natural numbers; given k, it gives the player who played at turn k. statement-at is another function of natural numbers; given k, it gives the statement made at move k. This may or may not actually be the constraint. Since we know ⟨TURN⟩, we could expand the existential quantifier, so that the contraint would be something like

  PLAYER = P ∧ atomic(STATEMENT)

  →

  P = O ∧ statement0 = STATEMENT ∨ O = O ∧ statement1 = STATEMENT ∨ P = O ∧ statement2 = STATEMENT …

  That is, we make a big disjunction and compute player-at and statement-at for each one. Evidently, some of these disjuncts are unsatisfiable because they contain equations such as “P = O”. We could further expand this one constraint into even more constraints by using the equivalence between p→(q∨r) and (p→q)∨(p→r), so that this implicational constraint generates a disjunctive constraint. This gives us an opportnity for parallel processing.
• The only propositional signature used by the site right now is one that has 26 atoms, whose names are simply the letters of the alphabet (case doesn't matter). We could expand any mention of the predicate atomic(STATEMENT) into a disjunction with 26 disjuncts STATEMENT = A ∨ STATEMENT = B ∨ …. We can refine this even further (again, at a cost of restricting the generality of the tool) by looking only at the atoms that are mentioned in the initial formula. (The generality of the site is restricted by doing this because it makes sense only for those rulesets where subformulas of the initial formula [or possibly symbolic attacks] appear.)

These are just some initial thoughts. I've used Felscher's D10 as an example, but we of course need to treat the other dialogue rules as well. It would be nice if, like D10, these can be reduced to boolean combinations of equations between constraint variables and ‘constants’ (like ‘P’).