Jigsaw Solver Challenge

Programs which generate, solve, and analyze Sudoku puzzles

Jigsaw Solver Challenge

Postby Mathimagics » Fri Feb 17, 2017 6:06 pm

Consider this toroidal Jigsaw on a 12x12 grid:
Toroidal-12-Ex41b.jpg
Toroidal-12-Ex41b.jpg (37.86 KiB) Viewed 1632 times


The text specs are given below. What I am interested in is whether anybody has a solver that can deal with this puzzle at all (JSudoku won't take it, for a start), and if so, how long it takes - preferably with proof of uniqueness, of course.

My standard DLX solver requires a rather sluggish 1280s (21m 20s), but my new DLX hybrid takes just 22s (CPU is 2.8GHz).

Code: Select all
AABBBCDDDEAA
AAABBCCCEEEA
AABBBCCCCEEA
FFFFGGCCHHHA
IFGGGGCCHHHI
IFJGGGGHHIII
FFJJGGHHHIII
FFJJJJDDHIIF
KKBJJJDDDIKF
KKBLLJJLDKKK
KEBLLLLLDKKK
EEBLLLDLDEEE

........8.A.
.5..........
.....2.B6..9
............
.....0...4..
.......0....
2..0.......5
...4....2...
...2.3......
B..7....1...
...8.A......
..51.B.....0
User avatar
Mathimagics
2017 Supporter
 
Posts: 1926
Joined: 27 May 2015
Location: Canberra

Re: Jigsaw Solver Challenge

Postby blue » Fri Feb 17, 2017 8:05 pm

Yes: 0.25s, with the single solution verified.

Code: Select all
0123456789AB
4539870AB216
780A124B6539
5046A89173B2
179B2083546A
39856170AB24
2BA034189675
A31476B52098
6472B3A90851
B26709541A83
96B85A324107
8A519B263740

It's a hybrid solver (hack), that uses DLX to set the clues, and converts the result to a SAT problem -- "boolean satisfiability problem".
The SAT solver, is "MiniSat 2.2.0" -- MiniSat home page

Cheers,
Blue.
blue
 
Posts: 979
Joined: 11 March 2013

Re: Jigsaw Solver Challenge

Postby Mathimagics » Sat Feb 18, 2017 11:03 am

Wows, that's impressive, blue!

I had experimented with a SAT solver but found it unpromising, initially. I will have to revisit that.

Can you explain "uses DLX to set the clues"?

Here are a few more test cases for you:

Code: Select all
AABBBCDCDEEEAAABFGDDDEAAAAABFGGGEEHHIIIIFGGGHHHJIIFFFFFGHHJJJIKFFGGGHJJJIIKKFFGHHJJJIIIKKKKDHJLLLLBBCKKDHJLLLLBBCKKDDDLLLABCCCKCDEELEABBCCCCDEEE
.........9..A..........8.7..............B......1.B..7......3...5.B....0.............6..8....4....0....A.9.5.....8........5....26..7...........8.


Code: Select all
ABCDEFDGHDIBEAIDJFHCGGKHBEFCDKAAJKJDBCAICFFDDLAEBHLIEHKFCEGJCLIIJGBDHKGHHKBFGGCDLEAIJEAKHLABBJLHJIKKFFILJKLHBHACEDCDGFKJLEIGJLIALLICKFCAGEEJBBFG
...........B..0...7...6.......4........A0..1...9...........1..................5.....B......27.......3.........A.................6...........8...


Code: Select all
ABBCDDEFGHIEHFJEJJGCGIDIGGJKCCEKJDHFEKDEKBFFDLGAGEHGAGHHAAEFLBBAKLHDIFDIDIBCBBDCCJKLIEFIFEGCIBKBBLDAHAIKEHGIJJFKHIBHFALJCJAALKHLLFALCJLGEDKCJLKC
......5..............3......B........2....9......8.0..4..61....................0....6.....1...8.................8.7.............A..........1...4
User avatar
Mathimagics
2017 Supporter
 
Posts: 1926
Joined: 27 May 2015
Location: Canberra

Re: Jigsaw Solver Challenge

Postby blue » Sat Feb 18, 2017 9:26 pm

Mathimagics wrote:Here are a few more test cases for you: (...)

The first one, it handled in 1.40 seconds.
For the other two, with no results after ~3 hours each, I killed the processes.
Does your "traversals" code work well with those two, too ?

I had experimented with a SAT solver but found it unpromising, initially. I will have to revisit that.

For situations where DLX performs adequately, a SAT solver would probably (?) be slower.
This one ... MiniSat ... uses something called "conflict driven clause learning", that can keep it from getting bogged down in areas where DLX code can get stuck for a long long time.

Can you explain "uses DLX to set the clues"?

For my DLX code, at least ... there's an inital setup of nodes and "links" (and so on), that would reflect the "pencil mark problem" for an empty sudoku grid. Then when you ask it to solve a particular puzzle, it goes through a phase where it treats each "clue" in the same way that it would treat a "guess" in the search loop. At that point, the nodes & links that are still in play, reflect the (starting) pencil mark problem for the puzzle itself -- clue cells filled, "line of sight" eliminations made ... only so many cell values remaing in each house, and so on. It's that "state" that gets converted into a SAT problem.
For DLX code in general, there's no reason that things should always work in that way.
You could a set up a special "exact cover" problem, for each puzzle, for example, and pass it to a "universal" DLX implementation.
[ Maybe that's what you're doing (?) ]

Cheers,
Blue.
blue
 
Posts: 979
Joined: 11 March 2013

Re: Jigsaw Solver Challenge

Postby Mathimagics » Sat Feb 18, 2017 11:24 pm

Wow, another fascinating insight into the vagaries of NP-completeness ...

Your SAT hack was nearly 100 times faster on the original example, and for the second toroidal case (1st of the additional set), that is still faster but by much less (1.6s vs 14.5s).

But for the arbitrary jigsaw templates mine appears to win by an even greater factor - my times are 35s and 45s for those last two.

I was actually hoping your solver would be consistent across all these examples - I read a paper which suggested SAT solvers actually show the best scaling behaviour, with DLX 2nd and CSP 3rd.

Speaking of scaling, I included that 2nd toroidal case because the regular DLX took nearly 2 hours to complete, ie 5 times the first example, but my traversal solver finds it easier than the first example. Go figure ...

You will note of course that these puzzles are all reduced (minimal clue sets), and so the arbitrary template cases require less givens than the toroidal ones, perhaps that is why your SAT solver has trouble?

Cheers,
Jim
User avatar
Mathimagics
2017 Supporter
 
Posts: 1926
Joined: 27 May 2015
Location: Canberra

Re: Jigsaw Solver Challenge

Postby Mathimagics » Sat Feb 18, 2017 11:30 pm

blue wrote:You could a set up a special "exact cover" problem, for each puzzle, for example, and pass it to a "universal" DLX implementation. Maybe that's what you're doing (?)


More or less - I got hold of a "C" DLX implementation, it has a universal solver (ie generic DLX), and I just set the binary matrix up and call it. I haven't touched the solver itself, just the front-end.
User avatar
Mathimagics
2017 Supporter
 
Posts: 1926
Joined: 27 May 2015
Location: Canberra

Re: Jigsaw Solver Challenge

Postby blue » Mon Feb 20, 2017 8:36 am

Hi Jim,

Mathimagics wrote:You will note of course that these puzzles are all reduced (minimal clue sets), and so the arbitrary template cases require less givens than the toroidal ones, perhaps that is why your SAT solver has trouble?

I don't think it's the clue count. I have used that solver to look for "contiguous region" jigsaw cuts that have just one "essentially distinct" solution, and I don't remember having any trouble with it.

I think it's that the "arbitrary templates" have few cells in the same rows or same, for a given region, and that the effect is that there's "little of use" to be learned by the "clause learning" feature.

It has been a log time since I looked at thier code, but I remember (I think) that whenever it saw a "conflict" resulting from its current sequence of guesses, that it would force itself to learn one new clause, and add it into the mix. Then it had a method of deciding that the learned clauses were using too much RAM, and that it was time to do a "restart" with a pruned down list -- a kind of "restart" that would allow it to remove some of the learned clauses, and continue on, without losing its point in the (hypothetical) "search tree".

It's a guess, but I think that with the "arbitrary templates", the clauses that it learns, are not only "of little use", but they're also "larger", and so using more RAM, and causing restarts to happen more often.

Cheers,
Blue.
blue
 
Posts: 979
Joined: 11 March 2013

Re: Jigsaw Solver Challenge

Postby Mathimagics » Mon Feb 20, 2017 10:51 am

blue wrote:I think it's that the "arbitrary templates" have few cells in the same rows or same, for a given region, and that the effect is that there's "little of use" to be learned by the "clause learning" feature.


So a worst-case scenario would be a template that is itself a Latin Square, while the opposite is true for DLX-T.

How does it perform on larger grids? This 16x16 example, with contig regions, for example, is troublesome for both DLX methods ( ~30 mins):
Code: Select all
AAAAABBBCCCCDDDDAAAABBBCCBCCCDDDAAAABBBBBBCCDDDDAAEFFBBBCCCCDGDDAEEFFFFHCHHHHGGDEEEEFFFHHHHGGGGDEEEEEFFHHHHGGGGGEEEIFFFFFHHHGGGGIEIIIIIJJJJKKKKKIIILLLLLLJJJKKKKIIIILMLLLJJJKNKKIILLLMLLJJOJJNKKPPPLMMMMMOOJNNNKPPPPMMOOOOOJNNNKPPPPPMMMOOOOONNNPPPPMMMMOOONNNNN
01.3.....9A......5.7.013.2...8.....C9.D4.F....12D.......7.....5.F....E0.24.8..............2...6.AF..D...0..2.......01......5.38.....6.....B....C.D.A..4.38..6...4..2B97..A.0....BC.......3.7...A.2A........4.E......7...1.E.5....9.B...5.0C3..4.C.....2.B.....3.
User avatar
Mathimagics
2017 Supporter
 
Posts: 1926
Joined: 27 May 2015
Location: Canberra

Re: Jigsaw Solver Challenge

Postby blue » Mon Feb 20, 2017 11:46 am

Mathimagics wrote:How does it perform on larger grids? This 16x16 example, with contig regions, for example, is troublesome for both DLX methods ( ~30 mins):
Code: Select all
AAAAABBBCCCCDDDDAAAABBBCCBCCCDDDAAAABBBBBBCCDDDDAAEFFBBBCCCCDGDDAEEFFFFHCHHHHGGDEEEEFFFHHHHGGGGDEEEEEFFHHHHGGGGGEEEIFFFFFHHHGGGGIEIIIIIJJJJKKKKKIIILLLLLLJJJKKKKIIIILMLLLJJJKNKKIILLLMLLJJOJJNKKPPPLMMMMMOOJNNNKPPPPMMOOOOOJNNNKPPPPPMMMOOOOONNNPPPPMMMMOOONNNNN
01.3.....9A......5.7.013.2...8.....C9.D4.F....12D.......7.....5.F....E0.24.8..............2...6.AF..D...0..2.......01......5.38.....6.....B....C.D.A..4.38..6...4..2B97..A.0....BC.......3.7...A.2A........4.E......7...1.E.5....9.B...5.0C3..4.C.....2.B.....3.

It works well with that one ...

Code: Select all
1 solution

0123456789ABCDEF
9567C01342DEF8AB
8ABC93D4EF567012
DE3428AB7C019F56
F6195E0D2478ACB3
78CE3DBF912A0564
AF45D68C0B32179E
2B9017CAFE65438D
10786A9E5DBF342C
ED5A024138FC6B79
43F2B978CA10E6D5
BCDFE4596387210A
52A68C30D794BEF1
340D7BF216E95AC8
698BF1E5A0C3D247
C7E1AF26B54D8930

0.14s

1r1c2 is redundant
Cr3c4 is redundant
Dr4c1 is redundant
Fr5c1 is redundant
2r5c9 is redundant
0r8c4 is redundant
Dr10c2 is redundant
4r10c7 is redundant

3.45s
blue
 
Posts: 979
Joined: 11 March 2013

Re: Jigsaw Solver Challenge

Postby Mathimagics » Mon Feb 20, 2017 2:33 pm

Nice work!

Any chance I can lay my hands on that solver?? :roll:

Is the redundant clue list purely on an individual basis, or does it imply the entire set can be removed?

I have at least, managed to reduced that 30m down to 2m 15s (by problem splitting + threading). Still a tad sluggish for full-scale reduction testing ...

Cheers
Jim
User avatar
Mathimagics
2017 Supporter
 
Posts: 1926
Joined: 27 May 2015
Location: Canberra

Re: Jigsaw Solver Challenge

Postby blue » Mon Feb 20, 2017 6:30 pm

Mathimagics wrote:Any chance I can lay my hands on that solver?? :roll:

I hate to say it, but no.
FWIW: The MiniSat code is available on the web.

Is the redundant clue list purely on an individual basis, or does it imply the entire set can be removed?

"Individual basis".

Cheers,
Blue.
blue
 
Posts: 979
Joined: 11 March 2013

Re: Jigsaw Solver Challenge

Postby tarek » Tue Feb 21, 2017 10:17 am

blue wrote:
Mathimagics wrote:Any chance I can lay my hands on that solver?? :roll:

I hate to say it, but no.

My solver(s) will never see the light because it will give an insight into how my chaotically organised brain works ... Basically it is a mess that happens to work :D

DLX for me has just been brilliant in solving any NP complete problems. For me it was Sudoku & variants/hybrids and all the fairy chess puzzles to name a few.

My sudoku generation hit a brick wall at 81x81 with the hardware I've got 7 years ago.

Well done guys for for finding a way through all of that.

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

Re: Jigsaw Solver Challenge

Postby Mathimagics » Tue Feb 21, 2017 11:32 am

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 exe version works fine, I knocked up a CNF generator and managed to replicate some times similar to blue's, but without being able to change the front-end, I'm stuck with a batch mode, single CNF file input and solution output which is clunky and inflexible, sigh ....


The MVS version was guaranteed to compile cleanly, the author assured us ... :evil:
User avatar
Mathimagics
2017 Supporter
 
Posts: 1926
Joined: 27 May 2015
Location: Canberra

Re: Jigsaw Solver Challenge

Postby Mathimagics » Tue Feb 21, 2017 11:45 am

It's interesting that SAT has such trouble with 12x12 arbitrary templates, while doing 16x16 contig jigsaws in the blink of an eye.

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.

Clearly SAT has major problems with this. Since solving the arbitrary jigsaw template case is essentially the same thing as finding an orthogonal LS, I am very surprised they pursued that approach rather that the transversal-DLX method. Might have been a whole heck quicker.
Last edited by Mathimagics on Tue Feb 21, 2017 2:14 pm, edited 1 time in total.
User avatar
Mathimagics
2017 Supporter
 
Posts: 1926
Joined: 27 May 2015
Location: Canberra

Re: Jigsaw Solver Challenge

Postby Mathimagics » Tue Feb 21, 2017 2:07 pm

My Win32 MiniSat solved the 16x16 contig case above in 0.07s (or so it claims) with a 14377 clause formulation, and the first arbitrary 12x12 template case in 2h 50m, with 16000 clauses.

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?
User avatar
Mathimagics
2017 Supporter
 
Posts: 1926
Joined: 27 May 2015
Location: Canberra

Next

Return to Software