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
Sudoku16 - Minimal Puzzles
52 posts
• Page 3 of 4 • 1, 2, 3, 4
Re: Sudoku16 - Minimal Puzzles
by 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).
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.
-
hkociemba1 - Posts: 60
- Joined: 08 August 2018
Re: Sudoku16 - Minimal Puzzles
by 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!
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
-
Mathimagics - 2017 Supporter
- Posts: 1926
- Joined: 27 May 2015
- Location: Canberra
Re: Sudoku16 - Minimal Puzzles
by 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.
-
hkociemba1 - Posts: 60
- Joined: 08 August 2018
Re: Sudoku16 - Minimal Puzzles
by 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.
1.000.000 * 12 / cores / 3600 = 23+ days.
Only solving would be much faster.
- creint
- Posts: 393
- Joined: 20 January 2018
Re: Sudoku16 - Minimal Puzzles
by blue » Mon Mar 11, 2019 8:49 pm
For the 2000 puzzles in the OP, MiniSat gave average times of:
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.
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
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: 1045
- Joined: 11 March 2013
Re: Sudoku16 - Minimal Puzzles
by Mathimagics » Tue Mar 12, 2019 3:36 am
.
Thanks to everybody for your observations and test results!
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.
Notes:
===============================================
The puzzles ("1 to G" format):
Thanks to everybody for your observations and test results!
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
-
Mathimagics - 2017 Supporter
- Posts: 1926
- Joined: 27 May 2015
- Location: Canberra
Re: Sudoku16 - Minimal Puzzles
by 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:
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.
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: 1045
- Joined: 11 March 2013
Re: Sudoku16 - Minimal Puzzles
by 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?
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?
-
Mathimagics - 2017 Supporter
- Posts: 1926
- Joined: 27 May 2015
- Location: Canberra
Re: Sudoku16 - Minimal Puzzles
by 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: 1045
- Joined: 11 March 2013
Re: Sudoku16 - Minimal Puzzles
by 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 ... 
-
Mathimagics - 2017 Supporter
- Posts: 1926
- Joined: 27 May 2015
- Location: Canberra
Re: Sudoku16 - Minimal Puzzles
by 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:
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
-
Mathimagics - 2017 Supporter
- Posts: 1926
- Joined: 27 May 2015
- Location: Canberra
Re: Sudoku16 - Minimal Puzzles
by 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.
Edit: Fixed the CNF file (twice)
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 228 times
- p14.zip
- (37.01 KiB) Downloaded 209 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: 1045
- Joined: 11 March 2013
Re: Sudoku16 - Minimal Puzzles
by 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!
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!
-
Mathimagics - 2017 Supporter
- Posts: 1926
- Joined: 27 May 2015
- Location: Canberra
Re: Sudoku16 - Minimal Puzzles
by blue » Tue Mar 12, 2019 10:25 am
Hi Mathimagics,
Yes, that's odd.
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.
(...) 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: 1045
- Joined: 11 March 2013
52 posts
• Page 3 of 4 • 1, 2, 3, 4
