Sudoku Programmers Forum Index

 
 FAQFAQ   SearchSearch   MemberlistMemberlist   UsergroupsUsergroups   RegisterRegister   ProfileProfile   Log inLog in          Games  Calendar

Log in to check your private messagesLog in to check your private messages   

and now the 25*25
Goto page Previous  1, 2, 3, 4, 5
 
Post new topic   Reply to topic    Sudoku Programmers Forum Index -> Puzzles
View previous topic :: View next topic  
Author Message
frisch

Joined: 16 Nov 2005
Posts: 55
:
Location: Paris, France

Items
PostPosted: Thu Dec 01, 2005 7:29 am    Post subject: Reply with quote

My timings for the 16 minimal 25x25:

Code:

Puzzle  1:  time: 1149043 ms
Puzzle  2:  time:   45655 ms
Puzzle  3:  time:   18161 ms
Puzzle  4:  time:   17003 ms
Puzzle  5:  time:    6038 ms
Puzzle  6:  time: 871275 ms
Puzzle  7:  time: 755505 ms
Puzzle  8:  time:   29653 ms
Puzzle  9:  time:   25988 ms
Puzzle 10:  time:  456526 ms
Puzzle 11:  time: 1279949 ms
Puzzle 12:  time: 2176236 ms
Puzzle 13:  time:   20505 ms
Puzzle 14:  time:   25242 ms
Puzzle 15:  time: 532231 ms
Puzzle 16:  time: 1042999 ms
Back to top
View user's profile Send private message Send e-mail Visit poster's website
xyzzy

Joined: 24 Aug 2005
Posts: 80
:

Items
PostPosted: Thu Dec 01, 2005 10:42 pm    Post subject: Reply with quote

dukuso wrote:

but you can reduce the .cnf a lot, by eliminating the variables
corresponding to the givens. And this is, what lsencode does

It seems to me the obvious reductions that can be made from the givens is to eliminate all the singleton clauses, eliminate the given variables from the ALO clauses, and eliminate all the AMO clauses in which the given appears. So, for a QWH of order N with G givens.

Full problem:
N^3 variables
3*N^2 terms of N variables, 3*N^3 total variables
3*(N^4 + N^3)/2 terms of 2 variables
G terms with 1 variable

Reduced problem:
N^3 - G variables
3*N^2 terms of N or fewer variables, with 3*N^3 - 3*G total variables
atleast 3*(N^4 + N^3)/2 - 3*N*G terms of 2 variables

It's surprising that satz would find such a large improvement from reducing the problem. It seems that unit propagation would immediately make these same reductions. Maybe satz only performs unit propagation on the variable it uses as a guess, and doesn't notice single terms in its input. If its search heuristic is such that it never tries a single variable term, then reducing the problem could make a very significant difference.

Quote:

I had assumed, SATZ were somehow doing this reduction by itself,
but apparantly this is not very efficient.
SATZOO is better in doing this, bút it's still faster
to feed it directly with the reduced form.

I also reduce the exact-cover-matrix now before
giving it to my solver for 3-fold (or such) speed-improvement

I don't like this idea of partially solving a problem, then timing just the final part of the solution. It ends as a game of who can cheat the most with a straight face, by finding a way to solve the problem as much as possible 'off the clock'. I think the time it takes to convert a QWH into a SAT problem, including any reductions made, should be included in the time SATZ or SATZOO take to solve the problem. How much faster is your solver when you include the time it takes to reduce the exact cover matrix? In other words, how much is actual improvement to the algorithm and how much is just changing the way you time?
Back to top
View user's profile Send private message Visit poster's website
dukuso

Joined: 14 Jul 2005
Posts: 424
:
Location: germany

Items
PostPosted: Fri Dec 02, 2005 12:56 am    Post subject: Reply with quote

the time needed to reduce the puzzle is negligable
Back to top
View user's profile Send private message Send e-mail Visit poster's website
frisch

Joined: 16 Nov 2005
Posts: 55
:
Location: Paris, France

Items
PostPosted: Fri Dec 02, 2005 4:47 pm    Post subject: Reply with quote

New timings for the 16 minimal 25x25 sudokus:

Code:

Puzzle  1:  time: 662845 ms
Puzzle  2:  time:  36892 ms
Puzzle  3:  time:  17217 ms
Puzzle  4:  time:   8671 ms
Puzzle  5:  time:   4813 ms
Puzzle  6:  time: 613134 ms
Puzzle  7:  time: 558122 ms
Puzzle  8:  time:  24240 ms
Puzzle  9:  time:  19993 ms
Puzzle 10:  time: 260210 ms
Puzzle 11:  time: 934167 ms
Puzzle 12:  time: 1219938 ms
Puzzle 13:  time:  16290 ms
Puzzle 14:  time:  20155 ms
Puzzle 15:  time: 398428 ms
Puzzle 16:  time: 566689 ms
Back to top
View user's profile Send private message Send e-mail Visit poster's website
xyzzy

Joined: 24 Aug 2005
Posts: 80
:

Items
PostPosted: Mon Dec 05, 2005 11:39 am    Post subject: Reply with quote

Quote:

Reduced problem:
N^3 - G variables
3*N^2 terms of N or fewer variables, with 3*N^3 - 3*G total variables
atleast 3*(N^4 + N^3)/2 - 3*N*G terms of 2 variables


I now realize that my description of the reduced SAT problem is completely wrong. I have no idea what I was thinking. Each of the three ALO clauses a given appears in becomes true and goes away. The entire AMO sequence for each of those ALO clauses go away too. Each given variable goes away, as it's forced true, and all the variables in the same row/column/digit as the givens go away, as they are forced false. Then all the AMO clauses that those forced false variables appear in go away, and all the ALO clauses have those variables removed.

I'm also very surprised by your observations about satz's speed. I downloaded the source to satz 215.2 and looked at what it is doing. After it reads in the SAT problem, they very first thing it does it process all unit clauses.

I modified the satz source so that it could read sudoku problems directly instead of going though some kind of sudoku to sat translator. For the first of the "top16 minimal-25" problems, it takes about 2 seconds to generate the SAT from the sudoku, 1 second to reduce it, and then about 876 seconds to solve it.

The reduction in the problem size is huge. With 274 givens that problem starts with 752,774 clauses and 15,625 variables. After reduction there are only 21,641 clauses and 1,871 variables.

I suppose what you've found is that if I had satz print out the problem after doing the reduction and then read it back in, it would only take 9 seconds instead of 876 to solve it.
Back to top
View user's profile Send private message Visit poster's website
dukuso

Joined: 14 Jul 2005
Posts: 424
:
Location: germany

Items
PostPosted: Mon Dec 05, 2005 12:01 pm    Post subject: Reply with quote

the 9sec. for Satz was for random 35*35 QWHs with 396 holes with 1GHz

with the long encoding it was 12 times slower.

Your modified Satz-program, is it available ?
Is it only for sudokus or also for QWHs ?
Back to top
View user's profile Send private message Send e-mail Visit poster's website
xyzzy

Joined: 24 Aug 2005
Posts: 80
:

Items
PostPosted: Thu Dec 08, 2005 5:22 am    Post subject: Reply with quote

I've fixed up my version of satz for sudokus so it's more usable. It can now solve both QWH and Sudoku problems, and prints out the solution as a completed puzzle.

When generating the SAT problem from the QWH/sudoku I avoid creating most of the clauses and variables that would be eliminated when the initial givens are processed. After all unit clauses are processed the problem is the same as if this wasn't done, yet satz is about to solve it about 6 times faster.

For the fist minimal 25x25 sudoku:

Full SATproblem: 752,774 clauses and 15,625 variables
After unit processing: 21,641 clauses and 1,871 variables
Time to solve: 876 seconds (~2 sec for generation/reduction)

Reduced SAT problem: 24,794 clauses and 2,048 variables
After unit processing: 21,641 clauses and 1,871 variables (same!)
Time to solve: 154 seconds (~0 sec for generation/reduction)

You can download the patch http://www.speakeasy.org/~xyzzy/satz215.2-sudoku.diff
Back to top
View user's profile Send private message Visit poster's website
frisch

Joined: 16 Nov 2005
Posts: 55
:
Location: Paris, France

Items
PostPosted: Thu Dec 08, 2005 7:48 am    Post subject: Reply with quote

Stupid question, but do the SAT approaches look for all the solutions, or just one?
Back to top
View user's profile Send private message Send e-mail Visit poster's website
dukuso

Joined: 14 Jul 2005
Posts: 424
:
Location: germany

Items
PostPosted: Thu Dec 08, 2005 8:53 am    Post subject: Reply with quote

just one.
That's the reason, why I switched to that method too.

Of, course, once the solution is found, you could add
one other clause with the negative solution
and run it again to look for other solutions
Back to top
View user's profile Send private message Send e-mail Visit poster's website
Display posts from previous:   
Post new topic   Reply to topic    Sudoku Programmers Forum Index -> Puzzles All times are GMT
Goto page Previous  1, 2, 3, 4, 5
Page 5 of 5

 
Jump to:  
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
Sudoku Programmers topic RSS feed 


Powered by phpBB © 2001, 2005 phpBB Group

Igloo Theme Version 1.0 :: Created By: Andrew Charron