The New Sudoku Players' Forum

[ThemePark]

I've been pondering this for a while, but have been unable to come to any solid conclusion for or against. Is it possible to use DLX to solve a Greater Than Sudoku? The problem is in how to add the constraint of two neighbouring cells being greater/less than each other, and I'm not sure whether or not it's possible, and if it is, how to implement it.

Any thoughts?

[Mathimagics]

DLX is an exact cover problem solver method, and I am pretty sure that you can't define a "greater than" Sudoku (ie a Futoshiki on a Sudoku grid) in this way.

The problem is that the extra constraints are context-sensitive, not global.

On the other hand, you can set it up as a Constraint Satisfaction problem, so a SAT solver can be used, but it does not necessarily follow that this can be converted to an exact-cover problem. Only a subset of SAT problems can be expressed as exact cover problems.

I am "pretty sure", not "absolutely certain", that this one can't.

[ThemePark]

Having given this some thought, I'm afraid you're right. The columns in DLX signify that you can choose exactly one row that satisfies that given constraint, so even if I make rows for each possible combination of values between two neighbouring cells, I think that would cause problems with the other constraints in a standard DLX sudoku grid.

However, I've read up a bit on a SAT format (Dimacs, I believe it's called) and struggle to see how I could do this with a SAT solver.

[creint]

Would work with SAT, use xor functions. If you give a sample I can implement it in my solver.

a xor b = !a or !b

cell a < cell b
!a1 or !b2
!a1 or !b3
...till b9
!a2 or !b3
...
!a8 or !b9

[SpAce]

a xor b = !a or !b

What does "=" mean here? Did you mean implication:

a xor b => (!a or !b)

? That works but equivalence (<=>) obviously doesn't. (Just to be clear, I'm only talking about the logical statement. I don't know anything about the real topic at hand.)

[creint]

both statements are equal; (a xor b) give same results as (!a or !b).
For cnf format you need it in or notation.

a b result
0 0 0
1 0 1
0 1 1
1 1 0

[SpAce]

both statements are equal; (a xor b) give same results as (!a or !b).

I don't think so. Even if they were, I wouldn't use "=" to indicate equivalence, especially in a sudoku context where it's OR in AICs.

a b result
0 0 0
1 0 1
0 1 1
1 1 0

That's the truth table for XOR. This is the truth table for (!a OR !b) ( <=> !(a AND b) ), assuming "!" means NOT:

0 0 1
1 0 1
0 1 1
1 1 0

See the difference? To get the same result you have to add a term:

a XOR b <=> ((a OR b) AND (!a OR !b)) <=> ((a OR b) AND !(a AND b))

If you need everything in ORs, then I guess this would work:

!(!(a OR b) OR !(!a OR !b))

[creint]

What is meant was still xor, like your answer: (!a v !b) ^ (a v b). On a normal sudoku you already have (a v b) clauses.
For this constraint you only need to add the (!a v !b) clauses if you already have the defaults.
So my statement (a xor b = !a or !b) was wrong.

[jaap]

I've been pondering this for a while, but have been unable to come to any solid conclusion for or against. Is it possible to use DLX to solve a Greater Than Sudoku? The problem is in how to add the constraint of two neighbouring cells being greater/less than each other, and I'm not sure whether or not it's possible, and if it is, how to implement it.

If you have a standard DLX solver that allows for optionally covered columns (i.e. columns that do not need to be covered - the chosen matrix rows may have values in that column that sum to 1 or 0), then you can encode Futoshiki problems for it.

For each inequality on an nxn puzzle, you make n-1 optionally covered columns. One column signifies that 1.5 does not lie between the values on either side of the inequality, one column for 2.5 not lying between the values, etc., all the way up to value n-0.5.
If you were to violate an inequality, one of those columns would be covered twice, which is not allowed.

For example, the placing of 3 on the small side of an inequality (3<?) is represented by a matrix row that has ones in 1.5 and 2.5 columns, because after placing the 3 it is no longer the case that 1.5 or 2.5 lies between the two values of the inequality, regardless of the right hand side.
Similarly, the placing of 2 on the large side of an inequality (?<2) is represented by a matrix row that has ones in the 2.5, 3.5, 4.5, ... columns, because after placing the 2 it is no longer the case that 2.5 or larger lies between the two values of the inequality, regardless of the left hand side.
Clearly placing both (3<2) would cover the 2.5 column twice, which the DLX solver will not allow.

[Mathimagics]

Glad to see that you guys seem to have sorted that out!

For the OP (wherever he may be) the answer is still NO for DLX, context constraints like X < Y can't be "encoded" in a DLX model.

[creint]

DLX could work, with normal sudoku you probably unlink rows/columns/boxes for the same digit.
You use an extra check if that cell has an greater than link. Find the other cell and unlink other digits for target cell. Only unlink when cell is empty.
Only know for sure when I build one DLX solver.

[blue]

You can do it with auxiliary varibles ... one for each "!(a & b)" that needs to be encoded.
For example, for "r1c1 > r1c2", !(3r1c1 & 5r1c2) can be encoded as "exactly one of { 3r1c1, 5r1c2, v_311_512 }".

Unless you can tell the solver to not use clauses like that in "guessing", it's probably a bad idea.

[Mathimagics]

It would be interesting to see the SAT clause count for a typical "Sudoku Inequality" puzzle with NO givens (a puzzle form that I am particularly partial to).

creint, I am keen to see your DLX idea in action ... although it does sound like some considerable tinkering under the hood is involved.

I can lend you a hacksaw, or maybe rent you a shed?

[tarek]

Hi all,

The fact that you're using external checks is probably why it isn't DLX that is doing the solving

tarek

[eleven]

I don't quite understand, why to think of DLX or SAT for a program to solve "greater than's".
Is this theoretical interest ?
I guess, that like for normal sudokus straight forward implementations would be faster.