一个与元组不同的东西(An alldifferent for tuples)

一个与元组不同的东西(An alldifferent for tuples)

我试图用每个数字有9个位置的观点来解决数独。 这是我的数独的表示：

从表中可以看出，数字5在数独中具有以下位置（行，列）:( 2,8），（4,2），（6,5）。

当我在解释中提到一行时，我的意思是这样一行：

例如，上面的行是第1行。

我所做的是以下内容：

对于每一行，使用与ic_global不同的方法alldifferent该行中的所有ROW值是否不同。 执行与上面相同的操作，然后执行COLUMN-Values。 对于每一行，检查方形数是否不同（每次使用行和col值计算），再次使用alldifferent 。

以上的工作正常，我得到了数独的解决方案，但不是正确的解决方案。 这是因为我还要检查一件事： 每个位置都必须不同 。 根据我的求解器的当前状态，我可以得到一个在同一位置有多个数字的解，fe： 2和3都可以在位置（5,7），因为我不检查所有位置是否不同。

我该如何解决这个问题？ 我试图以元组形式将所有位置放在一个列表中，然后检查所有元组是否不同但我已经挣扎了好几个小时而且我真的很绝望。 我希望我能在这里找到解决方案。

编辑：添加代码

I'm trying to solve a sudoku with the viewpoint that every number has 9 positions. This is the representation for my sudoku:

From the table you can read that number 5 has following positions (Row,Col) in the sudoku: (2,8),(4,2),(6,5).

When I mention a row in my explanation, I mean a row like this:

For example, the above row is row 1.

What I have done is the following:

For every row check if all ROW-Values in that row are different using alldifferent from ic_global. Do the same as above but then for the COLUMN-Values. For every row, check if the square numbers are different (calculated using a row and col value each time), using alldifferent again.

The above things work fine and I get a solution for the sudoku but not the correct one. This is because I have to check one more thing: every position must be different. With the current state of my solver I could get a solution that has multiple numbers on the same position, f.e.: 2 and 3 could both be at position (5,7) because I don't check if all positions are different.

How would I tackle this problem? I tried to get ALL the positions in one list in tuple form and then check if all tuples are different but I have been struggling for hours and I'm getting really desperate. I hope I can find a solution here.

EDIT: Added code

最满意答案

如您所知， all_different/1和相关约束适用于整数 。 此外，在您的情况下，您实际上对元组的特殊情况感兴趣，即由行和列组成的对 。

所以，你的问题实际上可以简化为：

我怎样才能将整数对映射到整数？

假设您有AB形式的对，其中A和B都被约束为1..9 。

我可以通过多种方式将这些对与整数一一对应 。 一个非常简单的功能是： 9×A + B. 想一想！

因此，我建议您以这种方式或类似的方式将这些位置映射到整数，然后在这些整数上发布all_different/1 。

练习 ：考虑其他可能的映射和它们的特性。 然后概括它们来处理元组 。

As you already know, all_different/1 and related constraints work on integers. Also, in your case, you are actually interested in a special case of tuples, namely pairs consisting of rows and columns.

So, your question can actually be reduced to:

How can I injectively map pairs of integers to integers?

Suppose you have pairs of the form A-B, where both A and B are constrained to 1..9.

I can put such pairs in a one-to-one correspondence to integers in several ways. A very easy function that does this is: 9×A + B. Think about it!

Thus, I recommend you map such positions to integers in this way or a similar one, and then post all_different/1 on these integers.

Exercise: Think about other possible mappings and their properites. Then generalize them to work on tuples.