|
|
Post by Lars Ericson on Jul 10, 2015 6:17:54 GMT -8
A constraint of GDL is that games always terminate hence the space of possible moves is a DAG.
I guess it is obvious to say then that if mA, mB, and mC are markings and P is a propnet and m1 -P> m2 means P can transition from m1 to m2, then if mA -P> mC and mB -P> mC then ~(mC -P> mA) and ~(mB -P> mB).
So if I like DAGs then my DAG nodes are just markings instead of states, the DAG machinery carries over otherwise.
|
|
|
|
Post by Steve Draper on Jul 10, 2015 9:52:33 GMT -8
Yes, but whether you can come up with a useful representation for a propnet marking that is more compact than the state is another matter
|
|
|
|
Post by Lars Ericson on Jul 10, 2015 9:59:16 GMT -8
Steve, I'm assuming that at any point in the game the size of the StateMachine and size of the corresponding PropNet marking are same order. I'm looking at design choices. The text talks about using Answer Set Programming to do some simplifications. I could do GDL -> Logic Programming Simplifications -> propnet -> Propnet Simplifications -> Game DAG, or skip propnet step if Icould get ASP to do the factoring/latch-inhibitor detection/dead state removal in the logic space. Chapter 16 gives an example of latch detection in ASP: logic.stanford.edu/ggp/chapters/chapter_16.html. Is factoring in the propnet sense possible in ASP, or does it make more sense to do a pass of ASP simplifications and then move to propnets and do a pass of propnet simplification? Is it correct that the main reason to use propnet rather than state machine is that state machine expands to 2^m where propnet description stays linear? That seems to be a pretty good reason to stay, but is that really an issue? I have to find the piece of code in GGP that expands out the state machine from the GDL and see if that is really a big time/space sink for the games we have, or whether it is not really material for the games in the GGP base. |
|
|
|
Post by Steve Draper on Jul 10, 2015 10:08:53 GMT -8
I think the best approach is very much an open question. I will comment on a few of the observations/points you make though:
1) O[sizeof(state)] == O(sizeof(propnet)). This is entirely false. The propnet must be at LEAST O(sizeof(state)) but it can be (arbitrarily) bigger. A very simple example is provided by 'Guess Two Thirds (6 player)'. The full state here is just one number in the range 1-100 for each of the 6 players (plus a couple of control props). However the size of the propnet is O(100 ^ <num roles>) - so the state size is linear in role count, but the propnet size is exponential
2) The above is why actually provers (and ASP I would think) scale much better than propnets, essentially because they do not have to ground everything. It is **probably** possible to construct a propnet that grounds dynamically (creates new components as it reaches them - like a cartoon railway track with someone pulling up track behind it and laying ahead!), but that would only help if the state space were poorly connected (that is to say it exhibitted locality such that parts of the state space could not be reached in a single move from other parts, which in trun would limit the scale of what needed to be ground at any one time). This is NOT true for Guess Two Thirds.
It's very much an open question where to do your optimizations and analysis. Some are easier in logic space, some in propnet space. All I can say is that its a good area to explore!
|
|
|
|
Post by alandau on Jul 10, 2015 16:46:04 GMT -8
Funny, I was just thinking about "virtual"/on-the-fly-generated propnets the other day. I think "god"/Cell Puzzle/Game of Death is a good test case; it doesn't work with OPNF currently, and it looks like a problem where the domain of one sentence type looks much larger than it actually is. The tricky part is that you'd probably want to "fold in" constants as you go, so you'd need some sort of system of component IDs that can change meaning over time, and any code using it would have to deal with that until it's fully ground.
I've also started a little work on generating propnets in a way that mirrors how provers function (essentially breaking down the rules so they have at most two conjuncts). I'm interested in seeing if this creates a situation where GDL changes that are good for provers are good for propnets and vice versa.
|
|
