Sudoku16 - Minimal Puzzles

For fans of Killer Sudoku, Samurai Sudoku and other variants

16x16 Mega List

Postby tarek » Sun Mar 10, 2019 2:45 pm

I'm glad you're having fun. It looks that it will hopefully lead to further improving your super solver/generator.

As it is a very big nearly random list, It will cover most interests & it will have some rare special qualities puzzles that may be of interest too.

Presented in this raw fashion. The list hasn't been sorted nor has it been checked for isomorphisms. This will allow for further operations that may be of interest as well.

tarek
User avatar
tarek
 
Posts: 2971
Joined: 05 January 2006

Re: Sudoku16 - Minimal Puzzles

Postby hkociemba1 » Mon Mar 11, 2019 4:44 pm

I adopted my code to batch solve Tarek's list of 2000 minimal puzzles. For 1823 of them the SAT solver took less than 0.1 s, for 176 of them the SAT solver took between 0.1 and 0.2 s and for one (Nr. 1302, see below) the SAT solver was not invoked at all because the preprocessing with the standard methods already solved it.

9.1..5.8.....74F........9.....D5...D.....FAE0.1..0.E2.......B..32FE7..3......05.36..7......4.......A0...69...2C.....AF....1.8..E...6...90.F.5..7...F..0D.........3..46C1A..5......90.....2.3A....7.CB...4E...DA.....1A.52.D..B.....89...1...E....B5.F..03...1.2.

Checking if the puzzles all are minimal also would take rather long (about 80 s per puzzle).
Last edited by hkociemba1 on Mon Mar 11, 2019 7:01 pm, edited 1 time in total.
User avatar
hkociemba1
 
Posts: 60
Joined: 08 August 2018

Re: Sudoku16 - Minimal Puzzles

Postby Mathimagics » Mon Mar 11, 2019 6:53 pm

hkociemba1 wrote:I adopted my code to batch solve Tarek's list of 2000 minimal puzzles.

That puzzle is one of mine, actually! 8-)

My testing indicates that SAT time for verifying a minimal puzzle is roughly (# of clues) x (time to solve the puzzle itself).

So for a typical minimal 16x16 it will take perhaps 90 times as long to verify it, as it does to solve …

… now consider the task of confirming that tarek's actual list of 1,000,000+ minimal 16x16's really are all minimal. :?


Cheers
MM
User avatar
Mathimagics
2017 Supporter
 
Posts: 1264
Joined: 27 May 2015
Location: Canberra

Re: Sudoku16 - Minimal Puzzles

Postby hkociemba1 » Mon Mar 11, 2019 7:06 pm

Mathimagics wrote:
hkociemba1 wrote:I adopted my code to batch solve Tarek's list of 2000 minimal puzzles.

My testing indicates that SAT time for verifying a minimal puzzle is roughly (# of clues) x (time to solve the puzzle itself).


The times for the SAT solver I gabe above are the times it really runs the SAT solver. Doing the preprocessing, initializing the clauses etc. is not included. Thats why in the end for testing of about 90 clue removals it takes about 80 s.
User avatar
hkociemba1
 
Posts: 60
Joined: 08 August 2018

Re: Sudoku16 - Minimal Puzzles

Postby creint » Mon Mar 11, 2019 7:58 pm

With my calculations it takes about 12 seconds or less to check for minimal with WinSAT.
1.000.000 * 12 / cores / 3600 = 23+ days.
Only solving would be much faster.
creint
 
Posts: 92
Joined: 20 January 2018

Re: Sudoku16 - Minimal Puzzles

Postby blue » Mon Mar 11, 2019 8:49 pm

For the 2000 puzzles in the OP, MiniSat gave average times of:

    3.49 msec per puzzle, to find 1st solution
    4.71 msec per puzzle, to verify that there's no other solution
    2.23 msec per clue, in minimality checks
    217.28 msec total, per puzzle
Added: I don't know what other people are dealing with, but here, the MiniSat solver is compiled into the code.
The SAT clauses are fed to the solver in code, and the solver is called as a function.
In particular, there are no intermediate "cnf" files.
The times are "end to end" times.
blue
 
Posts: 837
Joined: 11 March 2013

Re: Sudoku16 - Minimal Puzzles

Postby Mathimagics » Tue Mar 12, 2019 3:36 am

.
Thanks to everybody for your observations and test results! 8-)

I, too, am using the native-mode (compiled) MiniSAT mentioned by blue. creint's "WinSAT" is the same.

My original 2000 puzzles are perhaps "easier" than tarek's puzzles on average. creint's estimate of 23 days (which I assume is based on 6 or 8 cores?) might be a little undercooked.

Here are explicit comparison times on my system for the first 20 puzzles in tarek's list.

  • "SolveU" is the task of solving the puzzle and testing for a 2nd solution
  • "Check Minimal" is the task of checking each clue for redundancy
  • "SAT" is MiniSAT (on-board, via a 32-bit DLL)
  • "dSolve" is dSolver16
  • both solvers use the "0/1" method for redundancy checking (the "model" presented has the clue removed, and the corresponding candidate eliminated. The solver looks for a first solution only. If none is found then the clue is redundant)
Code: Select all
SAT v dSolve first 20 puzzles (Tarek's list)

                   SolveU               Check Minimal
      ===============================================
  Puzzle       SAT      dSolve         SAT     dSolve
       1     0.016       0.000       0.734      0.016
       2     0.234       0.534       9.438      1.477
       3     0.063       0.000      18.156      0.023
       4     0.359       0.039      22.672      9.658
       5     1.157       0.108      22.297      3.392
       6     0.031       0.000      13.187      0.100
       7     0.000       0.000      54.422      0.401
       8     0.625       0.015      65.063      4.744
       9     0.078       0.005      50.015      0.072
      10     0.047       0.000      61.844      5.674
      11     0.187       0.000      40.344      1.016
      12     0.016       0.000       2.562      0.310
      13     0.016       0.000       1.985      0.010
    * 14     1.640      25.036      20.797    900.453
      15     0.422       0.382      21.828      1.727
      16     0.047       0.000      36.125      0.042
      17     0.641       0.049      16.312      2.497
      18     0.000       0.000      14.516      0.010
      19     0.000       0.000      12.922      0.015
      20     0.031       0.000      26.453      0.025
      ===============================================
             5.625       1.124     511.687     31.219


Notes:
  • puzzle #14 is marked (*) as just one example of BGS ruining the party for dSolver16 - the aggregate times at the bottom exclude this entry, not because I wanted to fudge the figures, but to estimate the performance of dSolver16 for "non-infected" cases.
  • SAT minimality checks take 25s per puzzle on average. Admittedly the sample is small, but using this figure gives an estimate of 289 CPU-days for verifying the complete set. (Note: using the "1/2" method for redundancy checks could possibly double this time).
  • for dSolver16, the BGS issue is particularly nasty for minimality checking. Time for solving does predict time for minimality checks. I have found one example where the solve time is just 0.01s, but the minimality checks take over 2 hours!! :?
  • using a guess limit of 64K, dSolver16 can do minimality checks on the tarek mega-set at a rate of 250 puzzles/minute, which gives an estimated 3 CPU-days for the full set, but will only resolve about 55% of the puzzles. Raising the limit to 256K reduces puzzles/minute to 100, which gives an estimated time of 7.5 days, and with coverage increased to 68%. The NCS/BGS problem in a nutshell.

===============================================
The puzzles ("1 to G" format):
Tarek-first20: Show
Code: Select all
.....3.....46..A25.B86..7...F4..A.6.D.9.......18..7.A.B.285.39....85..1.3.6A...79617..5A82B.......2.B....17...E4.D.36..E..4..5......F.......4GC1..5....7..8......3....6.G..................1.....F.....5.....26.41.E9...........C.....81..D35.....9.74.2........
.8....9.7...5.....2....F....67......6.7B.8C.391A..5.48..619.BC.....2.A..5.6.4.39A..B...C.3187.5...6..D.1......E.4..9........2.D......E.....D1B8...38.C1....5...4591......2........D.3..74.....26B...9..23.......75.....3..42.....3....B6...78......1.4C5........
A4...16....3....9..53...B..62.8C8E...5A..G2.9..7....9D...18.AB....5964..7..B1.2.6..A78.2...5B.4.3...........7..94..8..5..........1.......25...6...6........7.951......3.............2.7D4A....3..C..............B..7.....61248.A...68..3..795..2...2C..1....3...
..B..56.......7.4.C.A..8G.....B9.28........7..1.....7...316D5.....3..9.4...A1.57F..95....4.B6..86.........8...2A...5...7E..1....3..4..1...9..B8.....8..37.C4..9.81..27.6..5.3.........A5...3..42..6BD.52.........8.7....9.A...6.....6.3..2.8A..4..5....1..4.....
...........2A.F.5..........6.347..2.3.7....C.5.6F...6..B517389D.C3...A...8.B17.98...7....EC...5....B...9.6.....A....2415....6...A.4...6..5B...7...135..4.......2.8..1..A94.7..........9.2.6...38...5.......8..B..9.84...7.F...6.16..8.32.A.....5.2.4..A1....3...
8.7..E..95.........2.....4...1D6.C192.6..83B....5...1.4.A.7C...9D.9.8....7...2...46....2.3..G.......9..4...A...5....653..C..8..49.58.2A7.6......6..A...5......32...7...9...4..1.3....F..G.28.94....D......6.75.32......A......B.....5..17..2.....1.3.B....5.4.8.
B....8....D....9.3.5.C.6..A1....6.147......B5...87..5..F.9.C2....4..3.7.....1...38.....5.2...9C............5...21B7.8.6...4....3.A.2.....7...D.4..........8D..A.......9...2637.1.5...1A8.43..6.........A6..4..3.29....4.E3.A8.1.....25.39.184......1...9..B.6...
8......B9A.E....C1.72G...........92A..1..8.56.....54A83...7......472..5A.B..1..C.69F...4.5..........1....4...27.....8.6....2...3.D.64....7..9...5..87.2...16.34.........42.35.1...B..............A..3....96.4.25....6.D.5.3.......1.B5.2...4A8...3...4....C8716.
..4.D7.F9..2..16.5.6C38.4......9793...5..E.8A......8.6.....7...3.B.3...A....9....8.....9.56....1....5....C...47.5..4E.6..3.1.2..2...4.....7.......71......25834.C..........361...A.9..2...B...5.8..B7.....1...62E.95...13......A.6..85.4....B7...2A.3....6.4....
....4A...C19...6.5.....D...A......3.5.8.......2...64.13..278.5.B5..31.....4.A2...1....7..56.8.B.......C2....71..2.9....5.3......C6..7...4D8.9..E4........72...6......86.3.91.....E7..3.........A..D....7....1.....BA..F.6....9..3789.6.4....2A5..2.1....C..5...4
..3.B......A5.D..41..8.3...B...9C...7...4D.....89.56.2...C.81..A...3..D..A..85.25.9A.....386.....67....4.....1...........25..3....A.5..2..94....3.B...6..81C..25.84..3.......7.6F5.2..4........3..C.97.1....3...2......A7...BE.4.....68..1..927..1..4......5..6.
6.4.9...87..5..33.7B.4.....1......89...23...4.6...2D..1A.............A..C.7.26..8.B.C.....347..1.91.6..4A..5....7...5.....2E83....F7...168...2.4.A.2..E.4...6.37..5.B....A..E8...C6...5.7......9.6.G8.2...431.....3.....9.........A..593.....7...5..1..B.....4..
.G612...9..3..45..7.....24..1...8.9.....5...3...5....3....8......3......4.......6C..4....1.8.3..F9..6...D..7..58...45.71E....2...8.7...F.6.A9.B..B.A...7.C....D...23B.....54.A8.46....5C8..1..F7..E.786.....2..4..4....3.2.6.87.......42...B.61..1...BD....9.5..
2G.........8B.75..7....6.4...A..498.2...5A..1...5..1C9E.3B............D.B.5..3.......A...3.984..B7..5.1.....A....31...8....492.7.2C.......DA.6...6..42.8....5.91...........7.......7.D5.9C.3....1A.3B...2..5...4..48...7C..6.9.3..2...A.89.....6....94........2.
256..F....1.A784.18......25A.C3.A94.....7G......7.....3.698...............2.7..E8.B....6E3...4AD.A..142......96..67...53B......2.........4.8.3B..8A....95...2.7...3..6..........4..57.1.9..6D.......47.....5......2..385...7.6...3.9.A6B.........C...9..8....215
....BF9...6.CA.5..6....21.A8....98.A....43....7..B5.341............8.........6..27..1.69D...5.B.49..D.2....78......1A...8...239...1.628..4.E.5...A...C3........B..427...A5......3..651..7..2..4.7.F..B..3..5.1...1....7....6D..4.5.C4..6.2....A..........9...837
1...837...4...96........2...4....38A....F.C.7.1..97.C41......25..4.E...........1.8..519BA.23..6..7......4.6....9...6...2.D9E3.8....14..A.5..2....2....59....1..3.E6.7....A...5C...C4..3.9..8..7.8.....A5...69..4.1........8..B3..5.B...67...A......2.....3...6.5
....A75..23..9.6.......14C.65....9AC3..6......811B..84..F...D...3..1...B..69.5....2..97..B...4..58.D.......42..764.7....3..A1.9.7.49...E...8.........5.7.A....E....24.6315...........1..9..3.2..B1.............2......3.6..58.A4.6782.94..C...B..3...........7..
G......8637..4C..B....7..C..F...2.496..5....3..1.A.72.......8..66......3.8..5B.....1.59.4...63...9..8......B12A77..8..C2......9....6..54........D..2.8.13.......8.......1D.47.651....73..2.5A.4...B5A..67...4.....3......4.29.5.A....14..5..E..2.2............8.
...8..5..26..7.AE......21D.B..5.24.9.3.....8...1.73.....A.............E.....61....1F.CA.3.8.....79..26B5...A...84.....7.F.B.5.9....63..B.5....7458..172.....EC.....35..C.4..1.6.......9A...6.8..61.5...4....A2........3.41.29.B...4.B....7......A2....6..3..7E..
User avatar
Mathimagics
2017 Supporter
 
Posts: 1264
Joined: 27 May 2015
Location: Canberra

Re: Sudoku16 - Minimal Puzzles

Postby blue » Tue Mar 12, 2019 5:35 am

Hi Mathimagics,

I don't understand the long times for the DLL version of MiniSat.
For 32-bit and 64-bit non-DLL code, I get times like these:

Code: Select all
                   SolveU               Check Minimal
      ===============================================
  Puzzle     Win32         x64       Win32        x64
       1    0.0059      0.0053      0.2488     0.2256
       2    0.0049      0.0044      0.2416     0.2152
       3    0.0074      0.0066      0.2737     0.2467
       4    0.0057      0.0051      0.2578     0.2309
       5    0.0053      0.0047      0.2558     0.2267
       6    0.0050      0.0047      0.2347     0.2055
       7    0.0051      0.0044      0.2427     0.2137
       8    0.0047      0.0041      0.2281     0.1975
       9    0.0055      0.0049      0.2408     0.2100
      10    0.0054      0.0051      0.2308     0.2037
      11    0.0045      0.0039      0.2182     0.1920
      12    0.0052      0.0045      0.2381     0.2127
      13    0.0063      0.0056      0.2182     0.1929
      14    0.0055      0.0049      0.2559     0.2267
      15    0.0052      0.0042      0.2285     0.1988
      16    0.0045      0.0039      0.2237     0.1977
      17    0.0050      0.0044      0.2316     0.2015
      18    0.0048      0.0041      0.2207     0.1933
      19    0.0048      0.0043      0.2368     0.2135
      20    0.0057      0.0046      0.2424     0.2154
      ===============================================
            0.1064      0.0937      4.7689     4.2200

I know we don't use the same method to encode "weak links", but I can't see it making that much of a difference.
blue
 
Posts: 837
Joined: 11 March 2013

Re: Sudoku16 - Minimal Puzzles

Postby Mathimagics » Tue Mar 12, 2019 7:03 am

Hi blue!

Good point … thanks for pointing this out. I had noticed this at one time but never did any follow-up investigation, as I was focusing on other things …

I will take a closer look and see if I can track down the cause of this anomaly …


PS: Are we starting from the same base? The raw puzzle, no pre-processing?
User avatar
Mathimagics
2017 Supporter
 
Posts: 1264
Joined: 27 May 2015
Location: Canberra

Re: Sudoku16 - Minimal Puzzles

Postby blue » Tue Mar 12, 2019 7:25 am

Mathimagics wrote:PS: Are we starting from the same base? The raw puzzle, no pre-processing?

Same base, yes.

I see that if I build the 32-bit version with Visual C++ 6.0, the times go up by a factor of ~2.5
If I build a "Debug" version, they go up by another factor of ~7.2
Still though, the 20 puzzles complete in ~87 seconds.
blue
 
Posts: 837
Joined: 11 March 2013

Re: Sudoku16 - Minimal Puzzles

Postby Mathimagics » Tue Mar 12, 2019 7:50 am

I build it now with GCC, but that's not the cause (see my PM) … I'll have to look hard at what I changed, compared to your original code … one possible cause DOES come to mind, actually ... :roll:
User avatar
Mathimagics
2017 Supporter
 
Posts: 1264
Joined: 27 May 2015
Location: Canberra

Re: Sudoku16 - Minimal Puzzles

Postby Mathimagics » Tue Mar 12, 2019 8:11 am

blue, I found what I think is your original build, that you had in the project you sent me. It's called MSAT.exe (Release) and dated 22/2/2017.

But when I run it on "SolveU" for puzzle #14 it, too, takes almost a full second, and that's just finding the first solution …

I have no idea how these 60ms solve times are being obtained ???? Can my encoding be that bad?

Could you possibly post here a zip? With:
  • your WinSAT EXE (32 or 64)
  • your CNF for, say, puzzle #14
That would let me decide at least where the anomaly actually is ... it has to be one or the other, surely ....
User avatar
Mathimagics
2017 Supporter
 
Posts: 1264
Joined: 27 May 2015
Location: Canberra

Re: Sudoku16 - Minimal Puzzles

Postby blue » Tue Mar 12, 2019 9:13 am

You said WinSAT above, and in your PM. It's MiniSat, of course.
Here are the zips.
There are 32 and 64-bit exes, built with Visual Studio 2012.
"msat-64 --help", lists command line parameters & options, for anyone else who's interested.

msat-exes.zip
(45.97 KiB) Downloaded 14 times
p14.zip
(37.01 KiB) Downloaded 12 times

Edit: Fixed the CNF file (twice)
Last edited by blue on Tue Mar 12, 2019 12:02 pm, edited 3 times in total.
blue
 
Posts: 837
Joined: 11 March 2013

Re: Sudoku16 - Minimal Puzzles

Postby Mathimagics » Tue Mar 12, 2019 9:58 am

Thanks blue!

I called the MSAT version I built WinSAT, that's why I keep referring to that.

I can see now that It's not the build, or the compiler, or anything I changed at all! It's all down to the encoding ... :?

I have apparently forgotten everything I learned about SAT-for-Sudoku encoding (:roll:), and so I have been including unit clauses for the givens, and I think this has a much greater impact on performance than I anticipated ... why this should be so is unclear to me, but I will try it with the "min # of variables" encoding and see if that does the trick.

BTW, your P14 CNF file produces multiple solutions. Is it meant to do this?

Cheers!
User avatar
Mathimagics
2017 Supporter
 
Posts: 1264
Joined: 27 May 2015
Location: Canberra

Re: Sudoku16 - Minimal Puzzles

Postby blue » Tue Mar 12, 2019 10:25 am

Hi Mathimagics,

(...) I have been including unit clauses for the givens, and I think this has a much greater impact on performance than I anticipated ... why this should be so is unclear to me.

Yes, that's odd.

BTW, your P14 CNF file produces multiple solutions. Is it meant to do this?

Nope, sorry ... I had a bug in the code that wrote the file.
I replaced .zip file attachment, in the original post.
Is it right now ?

BTW: You asked about "preprocessing".
I do the "line of sight" eliminations for the clues, but that's it.
blue
 
Posts: 837
Joined: 11 March 2013

PreviousNext

Return to Sudoku variants