The New Sudoku Players' Forum

[hkociemba1]

I was interested if my SAT-solver approach also works for SudoKakuro. I can give a positive answer. Solving a puzzle and testing for uniqueness is less than a second, so it is no problem trying to remove some entries.

Code: Select all

SK-17CS-004, reduced to 13CS:
 +----------+----------+----------+
 |  .  .  . |  .  .  . |  .  .  9 |
 |  .  .  . |  .  .  . |  .  .  . |
 | 15  . 30 |  .  .  . |  .  . 22 |
 +----------+----------+----------+
 |  .  .  . |  .  .  . |  .  .  . |
 |  .  .  . |  . 20  . |  .  .  . |
 |  .  .  . |  .  .  . |  .  .  . |
 +----------+----------+----------+
 | 13  . 19 |  .  .  . | 27  . 23 |
 |  .  .  . |  .  .  . |  .  .  . |
 |  6  .  7 |  .  .  . | 14  .  7 |
 +----------+----------+----------+


SK-20CS-002, reduced to 13CS:
 +----------+----------+----------+
 |  .  .  . |  .  .  . |  .  .  . |
 |  .  .  . |  .  .  . |  .  . 19 |
 |  . 22  . |  .  .  . |  . 13  . |
 +----------+----------+----------+
 |  .  .  . |  .  .  . |  .  .  . |
 |  .  .  . | 28  . 21 |  .  .  . |
 |  .  .  . |  . 23  . |  .  .  . |
 +----------+----------+----------+
 |  . 23  . |  .  .  . |  . 21  . |
 | 15  . 18 |  .  .  . | 13  .  . |
 |  . 11  . |  .  .  . |  .  9  . |
 +----------+----------+----------+


And here for example is a minimal puzzle with 12 clues

Code: Select all

  6  9  . 11 12  . 20 21 13
  .  .  .  .  .  .  .  .  .
  .  .  .  .  .  .  .  .  .
  .  .  .  .  .  .  .  .  .
  .  .  .  . 26  .  .  .  .
  .  .  .  .  .  .  .  .  .
  .  .  .  .  .  .  .  .  .
  .  .  .  .  .  .  .  .  .
  6  9 13  .  .  .  .  .  3


and here a symmetric one

Code: Select all

  3  .  .  . 12  .  .  . 11
  .  .  .  .  .  .  .  .  .
  .  .  .  .  .  .  .  .  .
  .  .  . 26  . 28  .  .  .
  .  .  . 12  . 13  .  .  .
  .  .  . 29  . 23  .  .  .
  .  . 27  .  .  . 14  .  .
  .  .  .  .  .  .  .  .  .
 12  .  .  .  .  .  .  .  3

For sourcecode see https://github.com/hkociemba/sudoKakuro

[Mathimagics]

For sourcecode see https://github.com/hkociemba/sudoKakuro

No build instructions!

If you need Delphi to build it that's bad since Delphi is not free!

Can you build it without Delphi? That is, with just FPC Win32 compiler.

If not, can you provide Win EXE file please.

Cheers
MM

[hkociemba1]

If not, can you provide Win EXE file please.

Ok, I added exe.zip to the repository. Invoking Java from a windows exe is of course not the most elegant way, in principle the program is small enough to completely rewrite it in Java. But I do not know if it is worth the time to do so.

[Mathimagics]

.
Thanks! I will try it.

So this program is in Pascal, the build environment is Delphi, and the SAT engine is Java?

That is a rather exotic mix!

[hkociemba1]

Solving a puzzle and testing for uniqueness is less than a second, so it is no problem trying to remove some entries.

I tried some modifications of SK-24CS-001 and with this puzzle

Code: Select all

 +----------+----------+----------+
 |  .  .  . |  .  .  . |  .  .  . |
 |  .  . 19 |  . 23  . | 26  .  . |
 |  . 20  . |  .  .  . |  . 21  . |
 +----------+----------+----------+
 |  .  .  . |  . 19  . |  .  .  . |
 |  . 19  . | 18  . 17 |  . 18  . |
 |  .  .  . |  .  .  . |  .  .  . |
 +----------+----------+----------+
 |  . 18  . |  .  .  . |  . 17  . |
 |  .  . 25 |  . 21  . | 21  .  . |
 |  .  .  . |  . 14  . |  .  .  . |
 +----------+----------+----------+


my solver took more than 2 minutes to find a solution and about 3 minutes to find that it is NOT a valid puzzle since there exist other solutions. I wonder if there are valid puzzles which also have this "bad" behaviour.

[Mathimagics]

.
Tried your exe, encountered the 64-bit Sat4J problem (my Java machine is 32-bit)

Found your instructions, went to Sat4J home page, where the download links currently do NOT work

Any suggestions where I can get hold of a 32-bit Sat4J?

This is starting to get really tedious ...

[hkociemba1]

.
Any suggestions where I can get hold of a 32-bit Sat4J?
This is starting to get really tedious ...

I looked around and found some places with the jar file but a nowhere saw a distinction between 32-bit and 64-bit. So is it possible that this is not the problem? If you run my program and press solve, at least the cnf-file cnf.txt will be created in the same directory. If you then open a console-window, change into the directory and enter "java.exe -server -jar org.sat4j.core.jar cnf.txt", what error message do you get? I really should think of doing the SAT part in another way...

I wonder if there are valid puzzles which also have this "bad" behaviour.

Yes there are. The following is a valid puzzle. I took more than 4 min to solve it and even longer to show uniqueness.

Code: Select all

 +----------+----------+----------+
 |  .  .  . |  . 12  . |  .  .  . |
 |  .  . 19 |  . 23  . | 26  .  . |
 |  . 20  . |  .  .  . |  . 21  . |
 +----------+----------+----------+
 |  .  .  . |  . 19  . |  .  .  . |
 |  . 19  . | 18  . 17 |  . 18  . |
 |  .  .  . |  .  .  . |  .  .  . |
 +----------+----------+----------+
 |  . 18  . |  .  .  . |  . 17  . |
 |  .  . 25 |  . 21  . | 21  .  . |
 |  .  .  . |  . 14  . |  .  .  . |
 +----------+----------+----------+


I would be interested to know if this one is also difficult for other solvers.

[Mathimagics]

.

Code: Select all

>  java -server -jar org.sat4j.core.jar cnf.txt
Error: missing `server' JVM at `C:\Program Files\Java\jre1.8.0_181\bin\server\jvm.dll'.
Please install or use the JRE or JDK that contains these missing components.


So my Java installation is client-only, it seems.

But it works fine if I leave the "-server" option out. Perhaps you can make that change in your EXE?

I can see from the SAT output that is has found the solution, so it is basically working.

[Mathimagics]

I would be interested to know if this one is also difficult for other solvers.

Indeed it is.

My solver is still just a VB hack of a DFS Sudoku solver I had lying around, so it is a long, long way from being optimal (yet), but that particular puzzle has set a new DFS iteration record (20 million), and took a very long time (25m) to prove its uniqueness.

Welcome to the world of Kakuro, where this sort of thing happens all the time. Kakuro clues are much weaker than Sudoku clues, generally. The degree to which uniqueness of a puzzle solution can be obscured is potentially huge, so it's possible to create puzzles like these.

These puzzles tend not to be useful as P&P puzzles, of course (since they are generally impossible to solve by hand), but they are of enormous theoretical interest (to people like me, anyway! ).

[Mathimagics]

Ungültige Zeigeroperation!!

Seems your "paste puzzle" logic could be a tad more flexible ...

[EDIT] I found the umlaut + u keyboard code!

[hkociemba1]

I removed the -server flag now. Concerning the Paste logic: At least "Ungültige Zeigeroperation" has vanished. If you prefer a certain format for the input it will be no problem to add it. But as far as I know the program accepts all the examples given in this thread.

but that particular puzzle has set a new DFS iteration record (20 million), and took a very long time (25m) to prove its uniqueness.

So it seems that the SAT approach is not that bad compared with other methods. I was not sure if this would really work well. Let me explain how the Kakuro specific part is coded into SAT. Each (row,column,value) tuple with row 0..8, column 0..8 and value 1..9 is mapped to a boolean variable, so there are 9^3 variables from 1..729 (SAT variables are represented by numbers). From these 729 variables exactly 81 have to be true and define a valid solution. Of course there are restrictions in a valid puzzle, these are described by a conjunction of "clauses". Each clause is the disjunction of variables or their negation. If for example the 4 neighbours n1..n4 of a cell must add up to 25 this corresponds to a lot of clauses. It is for example NOT possible that n1=3, n2=5, n3=8 and n4=1. If n1=3 corresponds to variable a, n2=5 to variable b etc. we have not (a and b and c and d) has to be true which is equivalent to not a or not b or not c or not d has to be true. In the SAT definiton file there is just the line
-a -b -c -d 0
where 0 just defines the end of the line. In my program the procedure sumClauses generates these clauses.
There are also clauses which describe that t no two diagonally-adjacent cells can have the same value. For each pair of diagonally adjacent cells we get 9 clauses, for example c1=3 and c2=3 is NOT true which again leads to a clause of the form -a -b 0. In my program the procedure dp_clauses generates these clauses.
So at the end we get often about 30000 clauses which all have to be true.

[Mathimagics]

So it seems that the SAT approach is not that bad compared with other methods.

Well, maybe, maybe not!

Your puzzle, as mentioned earlier, took my VB klunky solver 25m to fully process (uniqueness test).

SAT4J took 20 minutes just to find 1st solution. (Win32, 2.77Ghz cpu).

I'm familiar with SAT/CNF so I added a single constraint to your CNF file to constitute a uniqueness test, cell(0,0) != soln(0,0), ie "-6 0", and that has been running now for 4 hours with no end in sight.

But just to complicate things even further, I am sure that I ran my previous worst-case puzzle (15 minutes) through SAT4J via your CNF generator and it ran in double-quick time, less than a second for both stages.

I need to retest this result since it seems so anomalous, but if it turns out to be correct then that raises further questions ...

[hkociemba1]

I'm familiar with SAT/CNF so I added a single constraint to your CNF file to constitute a uniqueness test, cell(0,0) != soln(0,0), ie "-6 0", and that has been running now for 4 hours with no end in sight.

Though for testing for uniqueness this is not the correct way of course since we have to add cell(0,0) != soln(0,0) or cell(0,1) != soln(0,1) or.... and in this case the solver eventually returns earlier. This is what I do when you use the Button "Find different solutions". I hope ths works now for you and you have not to start the SAT solver manually.

[Mathimagics]

.
Doh! It's obviously past my bedtime ... or early onset dementia

[Mathimagics]

.
OK, a new day, I have dusted off the cobwebs from my ageing brain ...

My SAT4J timings for the test case were both incorrect. For finding the 1st solution, this was done with an older version of SAT4J (2.3.1), and the later version (2.3.5) is 2.5 times faster, it seems, as I now get 8m 20s (as against 20m).

Uniqueness testing, with the correct SAT4J version, and the correct CNF clause (!), takes 10m 20s. So the times are comparable.

Also, I now have the updated copy of HK's program, which now works as intended.

And finally, I have confirmed SAT4J timings for this other puzzle:

Code: Select all

  . 15  .  .  .  .  . 18  .
 18  . 22  .  .  . 18  . 16
  . 17  .  .  .  .  . 17  .
  .  .  .  .  .  .  .  .  .
  .  .  .  . 12  .  .  .  .
  .  .  .  .  .  .  .  .  .
  . 19  .  .  .  .  . 10  .
 10  . 24  .  .  . 17  . 11
  . 17  .  .  .  .  . 14  .


This was the previous worst-case puzzle for my solver, taking 15 mins for 2-stage uniqueness testing.

It takes SAT4J just 1.5s for the 2 stages (Find 1st, find 2nd).

The inference I draw from all this is that this puzzle is actually much, much, simpler than my solver would have me believe, and I need to find out why this is so.