In alttpr, for instance, small keys in a dungeon are all identical, or progressive objects (sword, glove). And we want to be able to express properties such as: to reach location X, I need at least that many items.
The basic plan is to
transform the pseudo-arithmetic clause so that the goal is a time n+1 first, so that this becomes a normal pseudo-arithmetic clause
use techniques from the minisat+ paper to transform such a pseudo-arithmetic clause into normal SAT clauses
In order to avoid silly combinatory explosion, we also need to make sure that the various copies of the same item that this will produce (I think) are ordered, and locations are ordered too, and that we only affect a larger copy of an item to a larger location (otherwise, we would produce a problem with two equivalent configuration, and we don't want that!)
In alttpr, for instance, small keys in a dungeon are all identical, or progressive objects (sword, glove). And we want to be able to express properties such as: to reach location X, I need at least that many items.
The basic plan is to
n+1first, so that this becomes a normal pseudo-arithmetic clauseIn order to avoid silly combinatory explosion, we also need to make sure that the various copies of the same item that this will produce (I think) are ordered, and locations are ordered too, and that we only affect a larger copy of an item to a larger location (otherwise, we would produce a problem with two equivalent configuration, and we don't want that!)