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).
To specify the graph, enter one node per line; each node has an identifier (string with no spaces), and can either be:
  • 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 specify input/output gates, list the ids separated by space; same for the input values (0/1 for false/true). The iteration exponent should be equal to the number of input/output variables, but for the sake of avoiding a lengthy simulation you may choose smaller values. The output checked for truth is the first one.
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).