Solving Japanese Sum Sudoku in MiniZinc

[Patrick Wienhöft]

A Japanese Sum Sudoku is similar to a Sudoku in that you have to fill a 9x9 grid with the numbers 1-9 in each cell such that in each row, column, and sub-sudoku (3x3 square) each digit occurs exactly once. The catch is that each row and column is annotated with a sequence of numbers (or sometimes also question marks). You then have to color each cell either yellow or gray in such a way, that there are as many yellow connected segments as there are numbers for each row/column and the numbers in each yellow segment have to add up to the specified numbers. An example can be seen here: https://www.youtube.com/watch?v=oCkWdcFxtFo

I tried to encode this problem in MiniZinc but found it very slow/scaling very badly. In fact, it's running for 12+ hours now for a single instance. I verified it works correctly by testing a smaller (4x4) instance which finishes correctly in 250ms.

I define the following variables:

% the grid plus annotation which are yellow

set of int: SIZE = 0..8;

array[SIZE, SIZE] of var 1..9: grid;

array[SIZE, SIZE] of var 0..1: is_yellow;

% for each yellow  segment a start and end point

% e.g. the first segment in the upper (0th) line:

var 0..8: r0start1;

var 0..8: r0end1;

% ... same thing for other segments, rows and columns

and the following constraints:

% start comes before end

constraint r0start1 <= r0end1;

% between one end and the next start there is at least one space

constraint r0end1+1 < r0start2;

% ... same for other segments

% a cell is yellow iff its index lies in between some start-end pair

constraint (is_yellow[0,0]=1) <-> (((r0start1 <= 0 /\ 0 <= r0end1)) \/ ((r0start2 <= 0 /\ 0 <= r0end2)) \/ ((r0start3 <= 0 /\ 0 <= r0end3)));

% ... same for all cells, and the same constraint for columns

and lastly, the usual sudoku constraints via alldifferent.

The whole program can be found here: https://pastebin.com/LZRn4nWg

The puzzle this particular one is based on is this one: https://s3.amazonaws.com/gs-geo-images/1f6283b6-f667-4a0f-a8ca-8806c9f9343c.png

Here, the question marks denote there has to be a yellow segment but its sum is left open.

What is the main bottleneck of this approach and how may I fix it?

[Patrick Wienhöft]

I forgot to mention the sum constraints. That's, e.g.,:

% cells in segments have to sum to specified number

constraint sum([ grid[1,i] | i in r1start1..r1end1 ]) = 18;

[Gabriel Hjort Åkerlund]

Hi Pat,

In the constraint programming course I took many years ago we discussed this problem. There are two key insights into modeling this problem:

1. The linear equality constraint (i.e. sum()) propagates poorly from a sum onto the terms. For example, if you have a x + y + z = 9 and you know x, y, z are all non-negative terms greater than zero, the best propagation you can get is x = [1..8], y = [1..8], x = [1..8]. Moreover, sum() typically only reasons on the bounds rather than individual values.
2. The linear inequality constraint does not know that all terms must be different from one another. When taking that into account, you would get x = [1..7], y = [1..7], z = [1..7]. Let's take another example, same as before but where x = 3. Without know about pair-wise distinctness, sum() propagates to y = [1..6], z = [1..6]. When taking pair-wise distinctness into account, you get y = {1,2,5,6}, z = {1,2,5,6}.

You can implement a sum() constraint that knows about distinctness by using the table constraint. Meaning, for each sum value you generate one or more tables where each row contains terms that sum up to that value. The quirk here is that you don't know how many terms you need (although you would know how many terms you AT LEAST need), so you would need to multiple table constrains per sum where only one of them is enforced. I.e.:

array[<as many tables you need>] of var bool: B;

constraint

forall (i in <number of tables>)

(table(<array of X values>, <table i>) <-> B[i]);

constraint sum(B) == 1;

Hope this guides you in this right direction.

Cheers,

Gabriel

[Mikael Zayenz Lagerkvist]

Him

Interesting puzzle variant with a combination of ideas from Sudoku,
Nonogram, and Kakuro.

As Gabriel noted, the combination of a sum and an all different
constraint is better (propagates more) than the two constraints by
themselves, and might be an important factor. Another factor is how to
take a larger view of splitting up a row/column according to the
hints.

In the Gecode distribution, there are examples for both Nonogram and
Kakuro. Nonogram uses regular expressions to model the hints, and is
described in MPG in chapter 17
(https://www.gecode.org/doc-latest/MPG.pdf). The Kakuro example
combines all different (called distinct in Gecode) and a linear using
extensional constraints specified by tables, described in chapter 21
in MPG.

I think that it should be possible to define a reasonable single
regular constraint for each individual row and each column hints
(preferably using finite automata) that encodes all the sums in one
go. It might be possible to incorporate some or all of the all
different reasoning as well, although that might also make the
automata too big. The goal either way is to get a global view of how
to split up each row/column into shaded blocks.

It might take some experimentation to find the right level to specify at.

Good luck,
Mikael

> --
> You received this message because you are subscribed to the Google Groups "MiniZinc" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to minizinc+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/minizinc/4956aeb9-ad6a-4a57-be8b-260f6071a67bn%40googlegroups.com.



--
Mikael Zayenz Lagerkvist

[Gabriel Hjort Åkerlund]

Yes, Mikael, I think you are right about using a regular for this one. That way, you would also be able to encode the constraint that there must be at least one unshaded (grey) square between two shaded (yellow) areas. The tricky thing is of course encoding the regular for each hint...

Cheers,

Gabriel