I call Fill3 the following simple game: the input is a $n \times n$ grid;
- every cell of the grid has a type: OR, AND, CHOICE, FANOUT and FIXED and can be rotated 0, 90, 180 or 270 degrees;
- every cell (except the FIXED) contains three green squares that according to the cell's type can be placed in several different valid configurations (see figure);
The aim of the game is to choose a valid configuration for each cell (the type and the rotation cannot be changed) in such a way that no two green squares are adjacent (vertically or horizontally). The game is NP-complete (a quick reduction is from planar 3SAT).
Valid configurations for each type of cell.
But the cell types are obviously a direct transposition of the four gadgets used in the bounded planar Nondetermnistic Constraint Logic (NCL) and the valid configurations match the constraints of the corresponding vertices in a constraint graph (blue/red arrows in the figure).
I'm wondering if a direct quick reduction from NCL is possible. It is immediate to reduce a planar constraint graph to a Fill3 game (CHOICE cells with a "free" endpoint can be used to build straight links and 90° turns). But in a bounded planar NCL problem $P$ the edges are reversed dinamically (though an edge can be reversed at most once) and the aim is to reverse a single edge; on the contrary the game Fill3 is static. A possible approach is: build the corresponding Fill3 game from $P$; "break" the edge that must be reversed (eventually expanding the board) and force it in the final direction using FIXED cells. Then one way is easy: if $P$ is solvable, the corrisponding Fill3 game has a solution (represented by the final configuration of the constraint graph); but the other way is more problematic:
If Fill3 has a (static) solution $s$, can we say that a (dynamic) solution for the corresponding planar bounded NCL problem $P$ always exist (i.e. a sequence of valid edge reversals)? And how to prove it formally?
