Trainyard is NP-Hard
This is an implementation of the reduction of NP-hardness for Trainyard provided in our paper titled Trainyard is NP-hard (ArXiv version).
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.
We prove the NP-hardness by showing a polynomial reduction from (the decision version of) Minimum Monotone Boolean Satisfiability Problem (Min-Mon-SAT), where we are given a CNF formula φ of n variables and m clauses such that each clause contains only positive literals and an integer k.
The goal is to decide whether there exists a truth assignment for the variables that satisfies φ and sets at most k variables to true.
To use the builder you can enter a formula (separating clauses with spaces and literals with pipes, e.g.
If the variables you chose are a solution for the formula, the board generated will show a solution (placing the rails for you, no thanks needed!), otherwise the board will be defective in some parts.
In the lower right side of the page you can find the simulation controls. Click Play (or Fast) and if your solution was correct, you will see it! (if it wasn't, something (hopefully a train) will crash).
Can I edit the board and simulate it? Sorry but it's not possible at the moment.
'More options'? If you want to tweak details of the simulation.
It says 'Unable to sync paths in clause playground blah blah', so? Click More options and increase AND Buffer height.
Why should I provide the height? It's easy to prove that the height must be polynomial in the size of the input, but doesn't mean that will fit into your screen (or memory), so to keep things nice and clean the board uses a small (editable) height.
Images courtesy of Matt Rix.
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.
We prove the NP-hardness by showing a polynomial reduction from (the decision version of) Minimum Monotone Boolean Satisfiability Problem (Min-Mon-SAT), where we are given a CNF formula φ of n variables and m clauses such that each clause contains only positive literals and an integer k.
The goal is to decide whether there exists a truth assignment for the variables that satisfies φ and sets at most k variables to true.
To use the builder you can enter a formula (separating clauses with spaces and literals with pipes, e.g.
a|b b b|c for (a or b) and (b) and (b or c)), then click Next.
Now you can choose which variables to set to true, and finally click Generate!.If the variables you chose are a solution for the formula, the board generated will show a solution (placing the rails for you, no thanks needed!), otherwise the board will be defective in some parts.
In the lower right side of the page you can find the simulation controls. Click Play (or Fast) and if your solution was correct, you will see it! (if it wasn't, something (hopefully a train) will crash).
Can I edit the board and simulate it? Sorry but it's not possible at the moment.
'More options'? If you want to tweak details of the simulation.
It says 'Unable to sync paths in clause playground blah blah', so? Click More options and increase AND Buffer height.
Why should I provide the height? It's easy to prove that the height must be polynomial in the size of the input, but doesn't mean that will fit into your screen (or memory), so to keep things nice and clean the board uses a small (editable) height.
Images courtesy of Matt Rix.
Enter a MonotoneSAT formula with space separated clauses (eg: a|b b b|c for (a or b) and (b) and (b or c)):
