That's only half the battle of course - proof of uniqueness would seem to require that I add a clause that negates the solved cell values and feed it back in for another round?
That's what I did -- as unsatisfying as it was.
There's probably a way to modify thier source code, to do things like finding all solutions to a problem, using a new "resume()" function.
I never tried it, but maybe someone else has (?).
I spotted a paper where these researchers used a SAT system to find orthogonal Latin Squares with diagonals (like X-sudoku), they were only looking at size 10, and they chewed up years (yes) of cpu time, much of it on clusters.
Have just spent several frustrating hours with MiniSAT.
The binaries (2.2.0) I got hold of work fine - but neither the MinGW/gcc nor the MVS/C++ versions that came with it can come within a mile of being compilable ...
The MVS version was guaranteed to compile cleanly, the author assured us ...
I had forgotten about that battle.
Looking at some file dates, it was Feb. 2011, when I fought it -- for MSVC 6.0
My modified source code is attached below.
[ ".cc" files were renamed to ".cpp" (for some reason). "#if defined(WIN32)"/"#if !defined(WIN32)", mark the other changes ]
Many of the changes would have been unnecessary with MSVC 2005 or later, and/or with additional include directories specified in the project file.
Here's an outline of how to use it: