The New Sudoku Players' Forum

[blue]

Hi Mathimagics,

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?

That's what I did -- as unsatisfying as it was.
There's probably a way to modify thier source code, to do things like finding all solutions to a problem, using a new "resume()" function.
I never tried it, but maybe someone else has (?).

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.

(...)

Wow !

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 MVS version was guaranteed to compile cleanly, the author assured us ...

I had forgotten about that battle.
Looking at some file dates, it was Feb. 2011, when I fought it -- for MSVC 6.0

My modified source code is attached below.
[ ".cc" files were renamed to ".cpp" (for some reason). "#if defined(WIN32)"/"#if !defined(WIN32)", mark the other changes ]

Many of the changes would have been unnecessary with MSVC 2005 or later, and/or with additional include directories specified in the project file.

Here's an outline of how to use it:

Hidden Text: Show

Code: Select all

- compile & link with
  MiniSat/core/Solver.cpp

- in application-specific code:

- include header files
  #include "MiniSat/core/Solver.h"
  #include "MiniSat/core/SolverTypes.h"

- declare fresh solver instance (on stack)
  Minisat::Solver S;

- for each SAT variable: (indicies start at 0)
  S.newVar() // this can done "on the fly", as needs for new variables arise

- declare scratch clause (on stack)
  Minisat::vec<Minisat::Lit> tmp;

- in a loop:
  tmp.clear();
  - in an inner loop:
    tmp.push(Minisat::mkLit(var));  // if clause is: "... | V | ..."
      or
    tmp.push(~Minisat::mkLit(var)); // if clause is: "... | ~V | ..."
  S.addClause_(tmp);

- to do the solving:

  if (!S.simplify())
    goto xxx; // not satisfiable

  Minisat::vec<Minisat::Lit> dummy;
  Minisat::lbool ret = S.solveLimited(dummy);
  if (ret == l_False)
      goto xxx; // not satisfiable

  if (ret != l_True) {
      puts("unexpected");
      exit(-1);
  }

- to extract the solution
  - loop over SAT variables
    if (S.model[var] == l_Undef)
    {
        // 'var' can take any value in this solution
        puts("unexpected");
        exit(-1);
    }
    else if (S.model[var] == l_True)
    {
        // 'var' is true
    }
    else
    {
        // 'var' is false
    }


MiniSat-msvc6.zip

[blue]

Hi tarek,

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.

Give SAT a try, if you like.
I used it with Mike Metcalf's 225x225 sudoku(s?), and it worked well.

For MxM with large M, you should learn about a "binary encoding" for the "weak links" part, that's necessary for "1 of N" clauses.
Without it, you need N*(N-1)/2 clauses like "(~A | ~B)", for the weak links.
With the binary encoding, you add log2(N) new variables for each clause, and use N*log2(N) clauses for the "weak links".
[ There's also a way to tell MiniSat to not use the new variables in "guessing", but for me, it ran faster if I didn't do that. ]

Cheers,
Blue.

PS: Actually, the binary encoding is easy to explain.
If you (or you, Jim) have trouble finding it, I'll explain it here.

[Mathimagics]

Wonderful, thanks, blue!

I will give it a try for the third time. I don't actually speak c++, which complicates things somewhat.

Nice to know somebody's actually done it, and that I can ask you (nicely ) for help!

I only learned CNF today (or was that yesterday?), but one of the papers I'm working up to is this:

Efficient encoding for selecting 1 of N

which appears to be just what you were discussing. Wow, it seems that a 16x16 can be encoded in less than 4K clauses. Happy days!

[Mathimagics]

Build successful! Nice job blue ...

Now I need to turn this beast into a DLL (aim high, die young)

[tarek]

Hi tarek,

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.

Give SAT a try, if you like.
I used it with Mike Metcalf's 225x225 sudoku(s?), and it worked well.

For MxM with large M, you should learn about a "binary encoding" for the "weak links" part, that's necessary for "1 of N" clauses.
Without it, you need N*(N-1)/2 clauses like "(~A | ~B)", for the weak links.
With the binary encoding, you add log2(N) new variables for each clause, and use N*log2(N) clauses for the "weak links".

Thanks,

I wish I had time to explore this. Solving large grid puzzles and generating random minimal ones as you know are different in terms of time consumption .... have you had any success in producing a minimal 81x81 puzzle or larger !!!

I'm pretty sure that the combination of SAT, better coding and more powerful hardware is going to crack these.

Again, well done!!!

Tarek

[m_b_metcalf]

Give SAT a try, if you like.
I used it with Mike Metcalf's 225x225 sudoku(s?), and it worked well.

However, the puzzle in question, from 2009, was lost when the Sudoku Programmers' Forum disappeared. In case it's of any further interest, I've used my (now faster) program to remove a few more clues, and the result I've posted in the Sudoku variants thread, q.v.

I wish I had time to explore this. Solving large grid puzzles and generating random minimal ones as you know are different in terms of time consumption .... have you had any success in producing a minimal 81x81 puzzle or larger !!!

blue's greatest achievement, in my eyes, was his set of 15 16x16 minimal puzzles that would have SE ratings of 10+ if SE worked on that size. These, too, were lost in the other Forum. Maybe blue could post them in the Variants here. (I have kept a copy, if needed.)

Regards,

Mike

[Mathimagics]

Blue, I've sent you a PM regarding a strange DLL problem ...

[blue]

I wish I had time to explore this. Solving large grid puzzles and generating random minimal ones as you know are different in terms of time consumption .... have you had any success in producing a minimal 81x81 puzzle or larger !!!

Quite true. I haven't tried anything over 25x25, except with Mike's 225x225.
For the 225x225, we got several clues removed (back then), but at some point it was too much for the SAT solver, too.
(I would try 81x81, but I have another project that I need to get back to).

blue's greatest achievement, in my eyes, was his set of 15 16x16 minimal puzzles that would have SE ratings of 10+ if SE worked on that size. These, too, were lost in the other Forum. Maybe blue could post them in the Variants here. (I have kept a copy, if needed.)

Thanks, Mike.
There were a couple of 25x25's too, that were even more difficult -- maybe enough to stump SE, if it handled 25x25.
I don't have any of them.
Post them if you like, but please don't send them to me, in hopes that I'll do it.

Cheers,
Blue.

[m_b_metcalf]

blue's greatest achievement, in my eyes, was his set of 15 16x16 minimal puzzles that would have SE ratings of 10+ if SE worked on that size. These, too, were lost in the other Forum. Maybe blue could post them in the Variants here. (I have kept a copy, if needed.)

There were a couple of 25x25's too, that were even more difficult -- maybe enough to stump SE, if it handled 25x25.
I don't have any of them.
Post them if you like, but please don't send them to me, in hopes that I'll do it.

Duly done. Anyone wanting an 81x81 will find one here (where I note that my program now solves it ten times faster than back in 2009).

Regards,

Mike

[tarek]

I wish I had time to explore this. Solving large grid puzzles and generating random minimal ones as you know are different in terms of time consumption .... have you had any success in producing a minimal 81x81 puzzle or larger !!!

Quite true. I haven't tried anything over 25x25, except with Mike's 225x225.
For the 225x225, we got several clues removed (back then), but at some point it was too much for the SAT solver, too.
(I would try 81x81, but I have another project that I need to get back to).

blue's greatest achievement, in my eyes, was his set of 15 16x16 minimal puzzles that would have SE ratings of 10+ if SE worked on that size. These, too, were lost in the other Forum. Maybe blue could post them in the Variants here. (I have kept a copy, if needed.)

Thanks, Mike.
There were a couple of 25x25's too, that were even more difficult -- maybe enough to stump SE, if it handled 25x25.
I don't have any of them.
Post them if you like, but please don't send them to me, in hopes that I'll do it.

Cheers,
Blue.

With DLX, the trick is to make your matrix as small as possible and that is where the jump into 81x81 and larger was taxing 7 years ago. With ways to reduce the weak links and SAT, I have no doubt that a minimal 81x81 is doable possibly with ease. Minimizing the 225x225 may still be challenging despite all the advances.

As I have a depth 2 backup of the programmers forum from 2010 hidden somewhere, I'll try to find your 25x25 puzzles and post them

Tarek

[Edit: the programmers forum is different from the players forum so I may not be successful in my hunt]

[Mathimagics]

After some teething troubles, and of course with blue's contribution, I have managed to get a DLL version of MiniSat up and running, and got binary encoding working.

Thus I am able to replicate blue's results (see prev page):

Code: Select all

SAT returned 1, et = 0.093431 (unique soln)

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

Start redundancy checks
  clue (0,1) is redundant
  clue (1,9) is redundant
  clue (2,3) is redundant
  clue (3,0) is redundant
  clue (4,0) is redundant
  clue (4,8) is redundant
  clue (5,A) is redundant
  clue (7,3) is redundant
  clue (9,1) is redundant
  clue (9,6) is redundant
  clue (A,3) is redundant
  clue (C,1) is redundant

SAT redundancy check time = 9.599786


Now curiously, my solve (uniqueness testing) seems to be a tad faster than blue's, but my reduction time is longer - but I wouldn't expect much better because 80 uniqueness tests to perform.

So, blue, 80 x .14 would be over 10s, so what's the story behind that 3.45s you reported for the reductions?

(I have also noticed that I "found" 4 extra - but they are false positives. Investigating ...)

[Mathimagics]

Aha, I had "check for singles enabled", so it was in fact working with 84 givens. The 4 added singles are of course are all redundant wrt the original puzzle.

[blue]

Hi Mathimagics,

Now curiously, my solve (uniqueness testing) seems to be a tad faster than blue's, but my reduction time is longer - but I wouldn't expect much better because 80 uniqueness tests to perform.

So, blue, 80 x .14 would be over 10s, so what's the story behind that 3.45s you reported for the reductions?

For the redundant clue detection, instead of removing the clue and checking for one-vs-two solutions, I'm removing the clue and removing the corresponding candidate from the pencilmark problem, and checking for zero-vs-one solution. If it's zero, the clue is redundant.

About the "0.14s -vs- 0.09s": My code wasn't set up to handle '0's for clue values, in the puzzle specification, so I changed 0 to A, A to B, ..., and F to G [ and then I reversed that in the solution output ]. If I change 0 to 1, 1 to 2, and so on, then I get 0.09s, too.

[Mathimagics]

About the "0.14s -vs- 0.09s": My code wasn't set up to handle '0's for clue values, in the puzzle specification, so I changed 0 to A, A to B, ..., and F to G [ and then I reversed that in the solution output ]. If I change 0 to 1, 1 to 2, and so on, then I get 0.09s, too.

Reminds of a great Monty Python sketch - "so when he says the Comfy-down mattress is 3 feet long, he really means that it's 60 feet long" ...

Reduction method - that's devious indeed, that thunk never occurred to me!

[Mathimagics]

That got it down to about 5.5s.

I would be able to to trim that further, it seems to me, if I wasn't stuck with having to create a new CNF with every call. I'd like to simply add a new clause (removing the pencil mark) and re-Solve, but I can't because of that code-generation problem (which I am assuming it is, can't think of any other possibility)