The New Sudoku Players' Forum

[Mathimagics]

Thanks blue, yes, it's correct now!

I did move the "p cnf …" header record back to the top of the file, it had mysteriously migrated to the end!

One final issue remains …

If I add up all the non-given cells' candidate counts, I get 2291. If I do a "singles" pass first, that identifies 8 singles (which agrees with dSolver16's figure), I get this down to 2144.

But you have reduced this considerably, since your variable count is just 1821. So, are we really starting from the same base? Isn't this an indicator that you are doing some something more, like Hidden/Naked pairs? something else?

Or am I missing something else in the "bleeding obvious" category (again!) ...

[EDIT] Oh dear, I messed up again, this is all wrong!

[Mathimagics]

Uh oh! Ignore that last post … I goofed again …

I was counting vars for a Samurai grid, not for a Sudoku16. Egad!

So, are we really starting from the same base?

Yes, exactly the same, of course ... 1045 is the correct candidate count …

[blue]

Hi Mathimagics,

I did move the "p cnf …" header record back to the top of the file, it had mysteriously migrated to the end!

Oops ... I messed up again
The attachment is fixed again (not that it matters now).

Also, I changed my code to start with the SAT problem for an empty grid, and add unit clauses for the clues, at the end of the list.
The times increased, but only by a factor of ~4.
With the 2nd solution and minimality testing included, the "per puzzle" times were still all under a second.

Adding the clauses for the clues, before (instead of after) the "empty grid" clauses helped.
That much was to be expected, at least.
The times were still up by a factor of ~3, though.

Cheers,
Blue.

[Mathimagics]

Oops ... I messed up again

Ha, I envy the quality of your mess-ups, and would gladly trade them for mine! The Mathimagics Mess-up is usually of the "gross logical blunder" variety.

Well, it was all down to encoding in the end, particularly MY encoding, which was quite OK as it turns out, but had a bug which caused it to generate far too many clauses (36K vs 14K)! Unfortunately for me, these were merely redundant, not inconsistent with the puzzle definition. So it was just like driving with the handbrake full on.

I would probably never have found it without you pointing out the time discrepancy!

In the end, "variable compaction" (reducing the SAT variables from 4096 to 1045 in this case) was a non-issue (although it is still rather elegant!), and binary-encoding of the "exactly 1 of" clauses also seems to make little difference here. But at these speeds this is an appearance that could be deceptive ...

For the 20 puzzles, I now get a total time (32-bit mode DLL) of 0.062s for "SolveU", 4.047s for "Check Minimal". That's with my original encoding method (with bug fix). I can't test Win64 mode just now, I have yet to make a C version of the CNF generator function.

That changes the SAT vs dSolver16 comparison completely, ie estimates for the full "Check Minimal" job on tarek's data. SAT might give close to 300 puzzles per minute if it keeps that up, while my best rate for dSolver16 is currently 250, and that with only 55% of the set actually resolved.

SAT could do the entire job in just 50-60 CPU hours it seems! Throwing 4 cores at it, this reduces to just 12-15 hours.

I have a prototype of an alternative NCS strategy that looks promising - dramatic reductions in time for minimality checking for some BGS cases (825s reduced to 22s, 2600s reduced to 160s). But the bar has been raised by SAT. Matching it will definitely be a challenge …

Cheers!

[Mathimagics]

.
Verified all minimal puzzles in tarek's collection, using MiniSAT via a DLL.

Used 4 core/threads, job took 15 hours. Minimality checks performed at rate of 294 puzzles/minute (per thread). Average time per puzzle was 205ms, maximum for any puzzle was 420ms.

That's remarkable in itself - the lack of any significant spread in the individual time for any puzzle …

[tarek]

Fantastic result in a quick time ... You have the super solver now

tarek

[Mathimagics]

Maybe so, but it's not the one I actually spent a month building ...

Hopefully dSolver16 will be faster than SAT for (nearly) singles-only 16x16 puzzles … no bad-guess syndrome worries there ... otherwise it is about as useful as an IBM 029 (a card punch!) ...

For SAT the next level, 25x25, that will be interesting …