QWH, order 30

dukuso · Posted: Sat Dec 03, 2005 4:54 am Post subject:

take the problem to place the 12 pentominoes into a 6*10 rectangle.
How would you solve it ?
Fill it top to bottom with the long side vertical.
This is much faster than taking the small side vertical !

Now you can encode this problem as a SAT-instance.
But how can the solver know, what's the long side of the
rectangle ? All it can see are the clauses.

I feel, that there could be a similar problem with
solving sudokus and QWHs or even SAT-instances in general.
When you have a large sudoku or QWH, you would concentrate
to fill some regions as strategic goal. OK, "tactically"
you would try to complete cells or constraints
with only few candidates, but when there are several
possibilities you would prefer a cell in a dense area
hoping that the whole area might collaps earlier or
later to trivial placements (singles).

We have to tell this strategy somehow to the solver !
Ideas ?

-Guenter

frisch · Posted: Tue Dec 06, 2005 8:39 am Post subject:

Why could'nt a SAT solve infer some topological properties about variables? Also, I'm not sure about what is a good notion of locality between cells in sudoku.

I updated the list of minimal 30x30 QWH in my web pages. It now contains 18 puzzles.

dukuso · Posted: Tue Dec 06, 2005 2:02 pm Post subject:

frisch · Posted: Tue Dec 06, 2005 5:26 pm Post subject:

So it seems your notion of metrics can directly be defined
in terms of the constraints under consideration (and I guess this metrics should evolve while the problem is further reduced). A SAT solver could probably use this kind of information as additional heuristics, if this is relevant (but I'm yet to be convinced this is the case).

dukuso · Posted: Fri Dec 09, 2005 5:11 am Post subject:

I have another idea, on how to improve your weighting function.

It is well known, that QWHs with a balanced spread of holes are much
harder than random QWHs.
See the lsencode-package from Gomes's webpage which I recommend
to download, if you haven't already.

Now, we can measure the "balancedness" of a puzzle to predict
its hardness.
E.g. walk through the constraints c and measure
the deviation of the number of matching placements N(c).
(exact cover formulation with n^3 placements and 3*n^2 contraints)

Or compute the minimum number M of placements per constraint
M = MIN {|N(c)|, c in _C}
Then compute the number Z of constraints with M placements.
Z = |{c in _C , |N(c)|=M }|
Maximize the pair (-M,Z)

gsf · Posted: Fri Dec 16, 2005 10:46 pm Post subject:

dukuso · Posted: Fri Dec 16, 2005 11:06 pm Post subject:

you're trying to beat Satz on QWHs ?!
will your algo work for SAT-instances and you make a SAT-solver
to challenge those in the SAT-competions with a modified
sudoku-solver ?! That would be funny :-)

Satz on those 18 with 2.6GHz

0.385
12.088
1.209
0.110
6.429
4.505
8.791
0.110
21.758
195.824
1.978
4.725
8.956
2.967
1.538
0.055
9.451
0.989

gsf · Posted: Fri Dec 16, 2005 11:24 pm Post subject:

dukuso · Posted: Sat Dec 17, 2005 7:47 am Post subject:

I see, you at least read something about SAT-solving already.
I probably also read something, but forgot most.

What's "backdoor" ? I remember "backbone".
Are you saying the magic cells are useful to speed up the solver
or predict it's hardness ?

I'm wondering, why #10 is so hard. Is this "intrinsic" hardness,
or could it be that we might be able to solve it quickly if we
only concentrated on this one with some special strategies ?

What is it, that makes it so much harder than the others ?

gsf · Posted: Sat Dec 17, 2005 11:55 am Post subject:

frisch · Posted: Sat Dec 17, 2005 2:36 pm Post subject:

My solver is a backtracking solver, so it makes guesses, as far as I understand what a guess is. The solver also does 1-lookahed at each step to reduce the number of candidates.

I've looked a little bit at SAT solvers. It seems that one of their basic techniques is to avoid discarding everything when backtracking occurs but instead keep the information learned when it does not depend on the wrong assumption. This might be equivalent to adding clauses to witness failures.
Is it what you call learning?

gsf · Posted: Sat Dec 17, 2005 4:08 pm Post subject:

frisch · Posted: Sat Dec 17, 2005 8:10 pm Post subject:

gsf · Posted: Sun Dec 18, 2005 5:02 pm Post subject: