Greater Than Sudoku and DLX

Post the puzzle or solving technique that's causing you trouble and someone will help

Greater Than Sudoku and DLX

Postby ThemePark » Sat Jan 12, 2019 5:33 pm

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?
ThemePark
 
Posts: 15
Joined: 27 September 2008

Re: Greater Than Sudoku and DLX

Postby Mathimagics » Sat Jan 12, 2019 6:31 pm

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.
User avatar
Mathimagics
2017 Supporter
 
Posts: 1134
Joined: 27 May 2015
Location: Canberra

Re: Greater Than Sudoku and DLX

Postby ThemePark » Thu Jan 17, 2019 3:22 pm

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.
ThemePark
 
Posts: 15
Joined: 27 September 2008

Re: Greater Than Sudoku and DLX

Postby creint » Thu Jan 17, 2019 6:58 pm

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
creint
 
Posts: 83
Joined: 20 January 2018

Re: Greater Than Sudoku and DLX

Postby SpAce » Thu Jan 17, 2019 7:43 pm

creint wrote: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.)
SpAce
 
Posts: 1285
Joined: 22 May 2017

Re: Greater Than Sudoku and DLX

Postby creint » Thu Jan 17, 2019 8:11 pm

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
creint
 
Posts: 83
Joined: 20 January 2018

Re: Greater Than Sudoku and DLX

Postby SpAce » Thu Jan 17, 2019 8:54 pm

creint wrote: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))
SpAce
 
Posts: 1285
Joined: 22 May 2017

Re: Greater Than Sudoku and DLX

Postby creint » Thu Jan 17, 2019 9:30 pm

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.
creint
 
Posts: 83
Joined: 20 January 2018

Re: Greater Than Sudoku and DLX

Postby jaap » Fri Jan 18, 2019 6:56 am

ThemePark wrote: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.
jaap
 
Posts: 2
Joined: 18 January 2019

Re: Greater Than Sudoku and DLX

Postby Mathimagics » Fri Jan 18, 2019 3:41 pm

Glad to see that you guys seem to have sorted that out! 8-)

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.
User avatar
Mathimagics
2017 Supporter
 
Posts: 1134
Joined: 27 May 2015
Location: Canberra

Re: Greater Than Sudoku and DLX

Postby creint » Fri Jan 18, 2019 4:53 pm

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.
creint
 
Posts: 83
Joined: 20 January 2018

Re: Greater Than Sudoku and DLX

Postby blue » Fri Jan 18, 2019 6:26 pm

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.
blue
 
Posts: 784
Joined: 11 March 2013

Re: Greater Than Sudoku and DLX

Postby Mathimagics » Fri Jan 18, 2019 6:51 pm

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? 8-)
User avatar
Mathimagics
2017 Supporter
 
Posts: 1134
Joined: 27 May 2015
Location: Canberra

Re: Greater Than Sudoku and DLX

Postby tarek » Fri Jan 18, 2019 8:53 pm

Hi all,

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

tarek
User avatar
tarek
 
Posts: 2909
Joined: 05 January 2006

Re: Greater Than Sudoku and DLX

Postby eleven » Fri Jan 18, 2019 10:01 pm

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.
eleven
 
Posts: 2031
Joined: 10 February 2008

Next

Return to Help with puzzles and solving techniques

cron