I have been playing this obsessively the last few weeks without knowing about the implementation. I thought it expresses the known facts about the board configuration as a system of linear equations and uses one of the classic algorithms for solving these. Anyone know if that would be infeasible for some reason?
I was thinking along the same lines when the systems of linear equations came up. The difficulty is that the variables are 0-1 while the equations are over the integers. So this is not quite as simple as solving a system over F_2, but is instead feasibility testing of an IP with 0-1 variables and a 0-1 matrix.
I wonder if solving the LP-relaxation might lead to a rounding based approach.
