Trainyard Verification is PSPACE-complete
This is an implementation of the reduction of PSPACE-completeness for the problem of verifying a solution to a Trainyard level. See the corresponding paper.
Trainyard is a grid-based logic puzzle game where the goal is to get each train from its initial station to a goal station. Every train starts out a certain colour, and most puzzles require the player to mix and merge trains together so that the correctly coloured trains end up at the right stations.
The reduction transform an instance of Iterated Monotone Boolean Circuit problem (It-Mon-BC) to Trainyard. In It-Mon-BC we have a monotone circuit (circuit with only AND and OR gates), with the n output nodes connected to the n input nodes (thus iterated), and we ask whether the h-th output assumes value true within t iterations.
In particular, we are interested in instances where we want to check if the first output assumes value true after 2n iterations, in a circuit such that when it gets true as value, it remain so for all the subsequent iterations (refer to the paper for the reduction from an It-Mon-BC instance to one with this property).
Trainyard is a grid-based logic puzzle game where the goal is to get each train from its initial station to a goal station. Every train starts out a certain colour, and most puzzles require the player to mix and merge trains together so that the correctly coloured trains end up at the right stations.
The reduction transform an instance of Iterated Monotone Boolean Circuit problem (It-Mon-BC) to Trainyard. In It-Mon-BC we have a monotone circuit (circuit with only AND and OR gates), with the n output nodes connected to the n input nodes (thus iterated), and we ask whether the h-th output assumes value true within t iterations.
In particular, we are interested in instances where we want to check if the first output assumes value true after 2n iterations, in a circuit such that when it gets true as value, it remain so for all the subsequent iterations (refer to the paper for the reduction from an It-Mon-BC instance to one with this property).
To specify the graph, enter one node per line; each node has an identifier (string with no spaces), and can either be:
To start the simulation use the panel in the lower-right corner.
The example instance is a circuit that propagates the truth values from right to left (till the first node, which keeps its value).
- A source node:
nodeId(e.g.1-1) - An identity node:
nodeId sourceId(e.g.4-1 2-1) - A gate node:
nodeId (or|and) inputLeftId inputRightId(e.g.2-1 OR 1-1 1-2)
To start the simulation use the panel in the lower-right corner.
The example instance is a circuit that propagates the truth values from right to left (till the first node, which keeps its value).
