The New Sudoku Players' Forum

[m_b_metcalf]

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)

Don't know whether it's relevant or practical in your context, but another method for redundancy checking is to start the solver at the known solution and ask it to find one extra solution (which is often 'nearby' if it exists). If it finds no extra solution, the clue is redundant.

Regards,

Mike

[Mathimagics]

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.

I thought I could achive that effect by simply passing in the same CNF array, but with the given in question having its sign reversed, remembering to change it back before I goto the next given. But it doesn't work, it remains SAT-ified, which is weird.

That should equate to the same thing, shouldn't it?
============================================
Ah, DOH, I just figured out why that doesn't work ...

[Mathimagics]

Don't know whether it's relevant or practical in your context, but another method for redundancy checking is to start the solver at the known solution and ask it to find one extra solution (which is often 'nearby' if it exists). If it finds no extra solution, the clue is redundant.

That's kind of what we are doing, only a SAT solver is not re-entrant in that way, you have to fiddle with the CNF "formula" and re-start. So the equivalent of what you're suggesting is to say "new problem = previous problem and not(previous solution).".

[m_b_metcalf]

So the equivalent of what you're suggesting is to say "new problem = previous problem and not(previous solution).".

Well, not quite, the whole point is to prevent '(previous solution)' from being found once again.

[Edit] Another short cut is to check whether the clue being tested is the only member of a UA4 or UA6 (or higher if you've enough patience). If it is, it is not redundant.

Regards,

Mike

P.S. Did you know that, in 2004, Euler's Equation was voted the most beautiful of all?

[Mathimagics]

Did you know that, in 2004, Euler's Equation was voted the most beautiful of all?

I voted for it in 1972. What took them so long ...

He keeps popping up - the transversal method I use in DLX-T is based on an idea of his originally. He was always fascinated by Latin Squares.

(Couldn't read that article, it's behind some sort of wall)

[blue]

Hi tarek,

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
(...)
[Edit: the programmers forum is different from the players forum so I may not be successful in my hunt]

Thank you for trying.
Your (relentless) effort, seems to have been well worth the time
[ I think I joined the Programmer's forum, just a few days after the last posts in your backup. ]

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).

In spite of other priorities, I couldn't resist exploring this again.
For 25x25, I produced minimal puzzles, in times ranging from 12.5-545 seconds, depending on the method (and random chance).

For 36x36, the SAT solver choked. It took several seconds, just to solve a blank grid with one clue added
When (using other methods), I got it a proper 36x36 grid, to use as a starting point, it looked like it would take at least 2 days to produce a minimal puzzle from it -- and probably a lot longer.

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.

Interesting ideas !
If you've been able to produce minimal 64x64's, then I bow to your magnificence

Cheers,
Blue.

[Mathimagics]

With ways to reduce the weak links and SAT, I have no doubt that a minimal 81x81 is doable possibly with ease.

Perhaps only with terabytes of RAM and a super cluster!

The following log reveals some unfortunate, and sobering, facts. We are solving with MiniSAT, just like blue, but with none of his pre-processing tricks (only the obvious singles checking):

Code: Select all

12:34:09 Loaded Reduced\Sudoku81-999.txt (3983 givens, 72 are non-removable)
12:34:12 Begin reduction (cumulative)
12:34:12  cell (12,56) is removable, nrem = 1
12:34:13  cell (28,3) is removable, nrem = 2
12:34:13  cell (53,53) is removable, nrem = 3
12:34:14  cell (48,28) is removable, nrem = 4
12:34:15  cell (64,21) is removable, nrem = 5
12:34:16  cell (9,76) is removable, nrem = 6
12:34:16  cell (60,17) is removable, nrem = 7
12:34:17  cell (57,22) is removable, nrem = 8
12:34:18  cell (37,10) is removable, nrem = 9
12:34:48  cell (31,60) is removable, nrem = 10
12:35:26  cell (27,24) is removable, nrem = 11
12:37:07  cell (37,47) is removable, nrem = 12
12:42:17  cell (42,16) is removable, nrem = 13
12:56:51  cell (1,53) is removable, nrem = 14
13:10:38  cell (13,61) is removable, nrem = 15
13:21:51  cell (32,60) is
13:21:51 [ERROR] solver result = -2


I began with a valid grid I pinched from here.

Then I checked every one of the 3983 givens to see whether they were removable (individually). Running 5 jobs checking 16 rows each took only 30 minutes. I began to get quietly excited ...

Only 72 of them were non-removable, so I set up phase 2. In this phase I select a removable given at random, then another, applying them cumulatively. The log above shows the progress.

Everything runs smoothly until the 10th removal, when all of a sudden the time to test jumps from 1-2 seconds to 30s, then 38s, then 101s, then 310s, then 874s, 827s ...

Worse still was the failure at step 16, when it got an "out of memory" exception. So all that effort and all I got was a 3868-given version.

I will run a similar test on 36x36 to see if the same behaviour is being exhibited (the effective time doubling) ... judging from blue's comments above, I think it will get further, but hit the same wall.

[blue]

I will run a similar test on 36x36 to see if the same behaviour is being exhibited (the effective time doubling) ... judging from blue's comments above, I think it will get further, but hit the same wall.

I should mention that I did get a couple of 36x36's, eventually.
One took ~8 hours in the reduction phase, and the other took ~3.