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.

`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*

_{1},…

*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).

`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:

This is a bit of a mess. Evidently we'll need the predicate "atomic", which can be applied to the variable`PLAYER`=**P**∧ atomic(`STATEMENT`) → [ ∃*k*(*k*< ⟨`TURN`⟩ ∧ player-at(*k*) =**O**∧ statement-at(*k*) =`STATEMENT`) ]`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

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 “`PLAYER`=**P**∧ atomic(`STATEMENT`)→ **P**=**O**∧ statement_{0}=`STATEMENT`∨ **O**=**O**∧ statement_{1}=`STATEMENT`∨ **P**=**O**∧ statement_{2}=`STATEMENT`… **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.)

**P**’).

## No comments:

## Post a Comment