SAT Sudoku Solver and Generator

Programs which generate, solve, and analyze Sudoku puzzles

SAT Sudoku Solver and Generator

Postby hkociemba1 » Wed Aug 08, 2018 2:29 pm

I wrote a program to solve/generate Sudokus (not only for the usual boxsize 3x3 but for any any boxsize NxM and N, M < 16). It uses some basic "human" solving techniques but also a SAT-solver can be selected. Download, program usage and some short explanation how the SAT-part works are here:http://kociemba.org/themen/sudoku/program.html

You must have a 64-bit windows systemfor the basic functions and additionally 64-bit Java for the SAT part.

Any questions, feedbacks and criticism are welcome.
User avatar
hkociemba1
 
Posts: 60
Joined: 08 August 2018

Re: SAT Sudoku Solver and Generator

Postby hkociemba1 » Thu Aug 16, 2018 9:48 pm

Though the feedback is not overwhelming yet with 0 replies I want to announce that I now added support for SudokuP variant for any boxsize. The program also could verify the uniqueness of the recently found three 9-clue SudokuPX for boxsize 3x3 (just check both SudokuX and SudokuP).

http://kociemba.org/themen/sudoku/program.html
User avatar
hkociemba1
 
Posts: 60
Joined: 08 August 2018

Re: SAT Sudoku Solver and Generator

Postby StrmCkr » Fri Aug 17, 2018 6:58 am

http://forum.enjoysudoku.com/composing-a-solution-grid-t34745-15.html

has some feed back regarding your code and ideas.

the langue of choice is more keen to my side of the word and very few others... as i use turbo pascal {syntax} is very close to delphi
most on here use c, c# and java with a few ruby coders kicking around.

on-top of that very few share their codes :( information on how to do stuff they do share but direct code is few and far between with the loss of the programmers forum
Some do, some teach, the rest look it up.
stormdoku
User avatar
StrmCkr
 
Posts: 1430
Joined: 05 September 2006

Re: SAT Sudoku Solver and Generator

Postby creint » Fri Aug 17, 2018 3:52 pm

It can generate large grids, that's nice, but it gets slower on lower errors, probably because of the randomness.
The reducing part for large grids is very slow 0.8 sec for each given, that can be improved to probably average 1000 givens/sec or faster when you only want known easy strategies.
Reducing givens will probably faster than generating a random grid in this way.
creint
 
Posts: 393
Joined: 20 January 2018

Re: SAT Sudoku Solver and Generator

Postby hkociemba1 » Sat Aug 18, 2018 8:58 am

creint wrote:The reducing part for large grids is very slow 0.8 sec for each given, that can be improved to probably average 1000 givens/sec or faster when you only want known easy strategies.

For fast detection of the easy strategies I use several arrays of bitvectors. The array rc_n for example returns for a given row r and a column c a bitvector rc_n[r,c] which holds the candidates for this cell. The array rn_c returns for for a given row r and a candidate n a bitvector rn_c[r,n] which holds the columns where the candidate n occurs in row r etc.
Adding a clue is easy since there is no ambiguity which candidates have to be deleted in the bitarrays. But for the reducing process you have to remove clues. If you remove a clue you cannot just reverse the process and set the corresponding bits in the arrays.
So what I do in the moment is to completely recompute the arrays after a single clue is removed (so I start with an empty grid and add again all remaining clues) which of course is very timeconsuming in the case of large grids with tens of thousends clues. Almost all of the 0.8 s goes here - I did not notice this before. Faster approaches are possible and I already have something in mind which should not be too complicated to implement. Thanks for the suggestion.
User avatar
hkociemba1
 
Posts: 60
Joined: 08 August 2018

Re: SAT Sudoku Solver and Generator

Postby hkociemba1 » Tue Aug 21, 2018 9:24 pm

I have completely rewritten the clue removal routine and the reduction is at least one magnitude faster than before for large grids. The new version 0.93 is downloadable on my homepage.
User avatar
hkociemba1
 
Posts: 60
Joined: 08 August 2018

Re: SAT Sudoku Solver and Generator

Postby creint » Sat Oct 20, 2018 6:01 pm

You posted composing-a-solution-grid-t34745.html#p269136
Surprisingly the algorithm does not seem to get stuck in a local minimum. Takes about 30 ms to generate a grid.


Sadly it gets sometime stuck when generating a random grid.

I got a sample that is stuck at 2 possibilities but neither of them can progress to 0 errors.
On row 19 cells in column 2 and 16 can only be swapped:
Hidden Text: Show
11 14 8 16 2 24 4 10 13 18 20 12 17 19 22 3 15 1 25 21 7 5 6 9 23
12 17 23 1 7 16 15 11 25 3 5 14 18 9 6 13 24 22 2 20 21 4 19 8 10
3 6 20 24 5 8 22 7 9 12 2 21 4 13 15 11 10 19 14 23 1 17 16 25 18
21 22 25 18 19 5 17 23 6 2 24 10 1 7 3 8 4 16 12 9 11 20 14 13 15
4 15 9 10 13 20 14 21 1 19 8 11 16 25 23 18 5 6 7 17 24 2 22 12 3
5 24 22 8 21 17 18 3 16 13 12 2 25 11 10 7 19 4 20 15 14 6 1 23 9
9 11 1 17 12 4 2 6 10 5 15 23 21 20 7 14 18 13 24 8 22 16 3 19 25
18 19 4 6 15 1 8 9 23 7 17 13 3 14 5 21 25 20 16 22 2 11 12 10 24
14 23 2 3 25 11 24 15 20 21 19 22 6 16 8 10 12 9 5 1 4 18 13 7 17
7 13 16 2 10 22 12 14 19 25 18 4 9 24 1 17 3 11 23 6 8 21 15 20 5
24 10 7 21 11 15 13 22 5 23 14 1 2 8 25 20 9 18 3 12 17 19 4 6 16
25 9 3 4 1 18 6 24 12 8 16 17 20 5 13 19 2 14 15 10 23 7 11 21 22
2 5 19 23 20 14 7 1 3 10 11 9 15 6 21 16 13 17 22 4 12 25 24 18 8
22 18 13 12 14 21 19 16 17 20 7 24 10 23 4 6 8 25 11 5 3 1 9 15 2
6 16 17 15 8 2 9 25 11 4 22 3 19 18 12 24 1 23 21 7 5 13 10 14 20
19 21 5 20 9 10 11 4 15 16 23 8 14 2 24 25 22 7 6 18 13 12 17 3 1
8 12 18 13 3 23 5 17 7 6 21 25 11 1 9 4 16 24 10 2 15 14 20 22 19
1 7 6 14 16 25 3 20 22 24 4 18 5 15 17 23 11 12 13 19 9 10 8 2 21
17 20 15 11 24 12 1 18 8 14 13 16 22 10 19 2 21 5 9 3 6 23 25 4 7
23 25 10 22 4 13 21 19 2 9 6 7 12 3 20 15 17 8 1 14 16 24 18 5 11
10 1 24 7 18 6 25 5 21 22 3 19 8 4 2 12 14 15 17 11 20 9 23 16 13
15 3 12 19 23 7 20 2 24 1 9 5 13 17 14 22 6 10 18 16 25 8 21 11 4
20 8 14 25 17 9 16 13 4 15 10 6 23 21 11 5 7 3 19 24 18 22 2 1 12
16 2 11 9 22 3 10 8 14 17 25 20 7 12 18 1 23 21 4 13 19 15 5 24 6
13 4 21 5 6 19 23 12 18 11 1 15 24 22 16 9 20 2 8 25 10 3 7 17 14
creint
 
Posts: 393
Joined: 20 January 2018

Re: SAT Sudoku Solver and Generator

Postby hkociemba1 » Sun Oct 21, 2018 7:31 am

creint wrote:You posted composing-a-solution-grid-t34745.html#p269136
Surprisingly the algorithm does not seem to get stuck in a local minimum. Takes about 30 ms to generate a grid.


Sadly it gets sometime stuck when generating a random grid.

I got a sample that is stuck at 2 possibilities but neither of them can progress to 0 errors.
On row 19 cells in column 2 and 16 can only be swapped:


The post you quote http://forum.enjoysudoku.com/composing-a-solution-grid-t34745.html#p269136 refers only a 9x9 Sudoku as you see from line 1 where I say
"1. Fill all rows with numbers from 1..9. in random order. "

So I of course cannot exclude that there is an example where it gets stuck in a 9x9 grid and I would be interested in having such an example. But if it exists it seem not easy to find it.
For larger Sudoku grids I know that the algorithm gets stuck sometimes. And the method becomes unpractical for very large grids anyways since the number of errors converges increasingly slow.
User avatar
hkociemba1
 
Posts: 60
Joined: 08 August 2018

Re: SAT Sudoku Solver and Generator

Postby creint » Mon Oct 22, 2018 8:45 pm

I found some 9x9 examples for you (default fill on rows):
No alternative cells that have lower error score, so stuck in 1 minimum.

Hidden Text: Show
1 6 9 2 4 8 3 5 7
8 7 4 6 3 5 1 2 9
5 2 3 9 1 7 4 8 6
6 9 1 8 2 4 7 3 5
3 4 2 7 6 9 5 1 8
9 5 7 3 8 1 2 6 4
7 3 8 1 5 6 9 4 2
4 1 6 5 7 2 8 9 3
2 8 5 4 9 3 6 7 1

6 3 5 1 7 4 9 8 2
7 4 1 9 8 2 3 5 6
8 2 9 5 3 6 1 7 4
9 6 8 2 5 1 4 3 7
2 7 3 4 6 8 5 9 1
4 5 6 3 1 7 8 2 9
3 1 7 6 9 5 2 4 8
1 9 2 8 4 3 7 6 5
5 8 4 7 2 9 6 1 3

8 4 1 9 2 6 3 7 5
6 2 3 5 7 1 4 8 9
5 7 9 4 3 8 6 2 1
1 6 2 7 8 9 5 4 3
7 9 4 1 5 3 8 6 2
4 3 5 6 1 2 7 9 8
2 1 7 8 6 5 9 3 4
9 5 8 3 4 7 2 1 6
3 8 6 2 9 4 1 5 7

Maybe adding some average timings when using this method would be nice.
I have seen some peeks at 10000+ swaps.
Guessing around 1 in 2000 will get stuck and 1 in 250 gets over 10000 swaps.
creint
 
Posts: 393
Joined: 20 January 2018

Re: SAT Sudoku Solver and Generator

Postby hkociemba1 » Wed Oct 24, 2018 10:28 am

Thanks for the examples.

creint wrote:Maybe adding some average timings when using this method would be nice.


What do you exactly mean by that? Do you mean I should run the generator lets say 100000 times and compute the average time?
User avatar
hkociemba1
 
Posts: 60
Joined: 08 August 2018

Re: SAT Sudoku Solver and Generator

Postby creint » Wed Oct 24, 2018 9:17 pm

hkociemba1 wrote:
creint wrote:Maybe adding some average timings when using this method would be nice.

What do you exactly mean by that? Do you mean I should run the generator lets say 100000 times and compute the average time?

I meant someone could make a normal distribution of swaps needed for a full grid.
creint
 
Posts: 393
Joined: 20 January 2018

Re: SAT Sudoku Solver and Generator

Postby hkociemba1 » Thu Oct 25, 2018 1:34 pm

creint wrote:I meant someone could make a normal distribution of swaps needed for a full grid.

I can give some results now. From 100000 tries to generate a grid by swapping 59 failed (I stopped after 10000 swaps), so your estimate with 1 in 2000 is not bad. They highest number of swaps which led to a valid puzzle was 2517, and there were 20 cases where more than 2000 swaps were needed. Here is the frequency distribution up to 1000 swaps. 800 swaps for the puzzle to be valid occured about 50 times for example.
plot.jpg
plot.jpg (22.95 KiB) Viewed 1820 times

Maybe I should define how I count the swaps here. Only those swaps are counted which do not increase the number of errors. The swaps which are reverted since the number of errors increases are not counted.
User avatar
hkociemba1
 
Posts: 60
Joined: 08 August 2018

Re: SAT Sudoku Solver and Generator

Postby creint » Fri Oct 26, 2018 8:00 pm

Why didn't you plot both, the difference would be interesting? You could also plot errors lower, same and higher.
creint
 
Posts: 393
Joined: 20 January 2018

Re: SAT Sudoku Solver and Generator

Postby hkociemba1 » Sun Oct 28, 2018 2:37 pm

The following graph counts additionally those swaps which must be reverted. The horizontal axis shows the number of swaps div 10, so if we for example read off about 50 for 600 this means that from the 100000 tries to generate a valid grid about 50 needed from 6000 to 6009 swaps. The shape is the same as before, so nothing really new. But the number of swaps counted now is much higher, with a peak at about 2000 swaps.
plot2.jpg
plot2.jpg (18.04 KiB) Viewed 1772 times
User avatar
hkociemba1
 
Posts: 60
Joined: 08 August 2018


Return to Software