Minzinc 约束问题 - 数独类似

我很好奇如何使用Clingo ASP以简洁的方式对这个问题进行建模，作为 minizinc 的替代方案。它不是约束编程，但与之相关且非常具有声明性，因此它可能会给你一些想法：

（实际上，minizinc也通过flatzingo支持相关的求解器。）

% Define rows and columns
row(1..6).
col(a;b;c;d;e;f).

% Define digits
digit(1..9).

% Each cell has exactly one digit
1 { value(R, C, D) : digit(D) } 1 :- row(R), col(C).

% Each digit appears exactly 4 times in the grid
:- digit(D), #count { R, C : value(R, C, D) } != 4.

% No two adjacent cells in a row or column can have the same digit
:- value(R1, C, D), value(R2, C, D), R1 = R2 - 1.
:- value(R, C1, D), value(R, C2, D), adjacent_col(C1, C2).

% Define adjacency in columns
adjacent_col(a, b). adjacent_col(b, c). adjacent_col(c, d).
adjacent_col(d, e). adjacent_col(e, f).
adjacent_col(X, Y) :- adjacent_col(Y, X).

% Row uniqueness with exceptions
:- row(R), digit(D), #count { C : value(R, C, D) } > 1, not allowed_repeat(R, D).

% Column uniqueness with exceptions
:- col(C), digit(D), #count { R : value(R, C, D) } > 1, not allowed_repeat(C, D).

% Define exceptions for uniqueness constraints
allowed_repeat(2, 6).
allowed_repeat(3, 3).
allowed_repeat(4, 5).
allowed_repeat(5, 7).
allowed_repeat(6, 8).
allowed_repeat(b, 3).
allowed_repeat(d, 8).
allowed_repeat(f, 9).

% Enforce the exact count for the exceptions
:- #count { C : value(2, C, 6) } != 2.
:- #count { C : value(3, C, 3) } != 2.
:- #count { C : value(4, C, 5) } != 2.
:- #count { C : value(5, C, 7) } != 3.
:- #count { C : value(6, C, 8) } != 2.
:- #count { R : value(R, b, 3) } != 2.
:- #count { R : value(R, d, 8) } != 2.
:- #count { R : value(R, f, 9) } != 2.

% Sum constraints row 1, col E
:- #sum { D : value(1, C, D), col(C) } < 38.
:- #sum { D : value(R, e, D), row(R) } != 21.

% Forbidden digits in specific rows and columns
:- value(2, C, 1).
:- value(4, C, 4).
:- value(5, C, 2).
:- value(6, C, 3).
:- value(R, c, 2).

% Column B only has even digits except for two "3"
:- value(R, b, D), D != 2, D != 4, D != 6, D != 8, D != 3.

% Column A must be an ascending or descending sequence
:- value(1, a, D1), value(2, a, D2), value(3, a, D3),
   value(4, a, D4), value(5, a, D5), value(6, a, D6),
   not ascending(D1, D2, D3, D4, D5, D6),
   not descending(D1, D2, D3, D4, D5, D6).

ascending(D1, D2, D3, D4, D5, D6) :-
    value(1, a, D1), value(2, a, D2), value(3, a, D3),
    value(4, a, D4), value(5, a, D5), value(6, a, D6),
    D1 = D2-1, D2 = D3-1, D3 = D4-1, D4 = D5-1, D5 = D6-1.

descending(D1, D2, D3, D4, D5, D6) :-
    value(1, a, D1), value(2, a, D2), value(3, a, D3),
    value(4, a, D4), value(5, a, D5), value(6, a, D6),
    D1 = D2+1, D2 = D3+1, D3 = D4+1, D4 = D5+1, D5 = D6+1.

#show value/3.

输出：（复制粘贴代码即可在线运行）

clingo version 5.7.2 (6bd7584d)
Reading from stdin
Solving...
Answer: 1
value(6,a,8) value(5,a,7) value(4,a,6) value(3,a,5) value(2,a,4) value(1,a,3) value(3,b,3) value(5,b,3) value(4,e,1) value(6,e,2) value(3,e,3) value(5,e,4) value(1,e,5) value(2,e,6) value(1,c,6) value(1,d,7) value(1,b,8) value(1,f,9) value(6,f,9) value(2,d,8) value(6,d,8) value(5,c,7) value(5,f,7) value(4,c,5) value(4,f,5) value(2,b,6) value(4,b,2) value(6,b,4) value(6,c,1) value(3,c,4) value(2,c,9) value(5,d,1) value(3,d,2) value(4,d,9) value(3,f,1) value(2,f,2)
SATISFIABLE

Models       : 1+
Calls        : 1
Time         : 3.559s (Solving: 0.59s 1st Model: 0.59s Unsat: 0.00s)
CPU Time     : 0.000s

作为矩阵的唯一解：

更新：

我将 OP 的另一个解决方案添加到模型中，以便在两个方向上进行验证：

value(1,a,3). value(1,b,6). value(1,c,7). value(1,d,8). value(1,e,5). value(1,f,9).
value(2,a,4). value(2,b,8). value(2,c,6). value(2,d,9). value(2,e,6). value(2,f,2).
value(3,a,5). value(3,b,3). value(3,c,4). value(3,d,1). value(3,e,3). value(3,f,9).
value(4,a,6). value(4,b,2). value(4,c,5). value(4,d,2). value(4,e,1). value(4,f,5).
value(5,a,7). value(5,b,3). value(5,c,1). value(5,d,7). value(5,e,4). value(5,f,7).
value(6,a,8). value(6,b,4). value(6,c,9). value(6,d,8). value(6,e,2). value(6,f,1).

…输出结果如下：

clingo version 5.7.2 (6bd7584d)
Reading from stdin
Solving...
UNSATISFIABLE

Models       : 0
Calls        : 1
Time         : 2.543s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s

暗示：

看看第四行！

感谢所有提示！看起来很完美。

另一个解决方案在这里：

再次感谢并致以最诚挚的问候，

冈瑟

这是一段minizinc 代码片段，使用all_different_except()和count()强制第 2 行具有除 2x 6 之外的不同数字：

include "globals.mzn";  % Ensure all global constraints are available

int: n = 6;  % 6x6 matrix
set of int: D = 1..9;  % Digits 1-9
array[1..n, 1..n] of var D: grid;  % 6x6 variable grid

% Constraint: Row 2 must have different values except that 6 appears twice
constraint all_different_except(grid[2, 1..n], {6});
constraint count([grid[2, c] | c in 1..n], 6) = 2;

%%% also works like this:
%%% constraint count(grid[2, 1..n], 6, 2);

solve satisfy;

输出：

{'grid': [
  [1, 1, 1, 1, 1, 1],
  [6, 6, 3, 2, 1, 4],
  [1, 1, 1, 1, 1, 1],
  [1, 1, 1, 1, 1, 1],
  [1, 1, 1, 1, 1, 1],
  [1, 1, 1, 1, 1, 1]
]}

好的，伙计们。这是我的 MiniZinc 模型，给出了正确的结果。

% Solution for Puzzle
%
% Conditions:
% row 1: sum>=38            column A: sequence asc. or desc.
% row 2: two 6, no 1                column B: two 3 but no more odds
% row 3: two 3              column C: no 2
% row 4: two 5, no 4                column D: two 8
% row 5: three 7, no 2          column E: sum = 21
% row 6: two 8, no 3            column F: two 9

include "globals.mzn";
include "alldifferent.mzn";

set of int: digits = 1..9;
array[1..6,1..6] of var digits: matrix;

% sum of row 1 >= 38
constraint (matrix[1,1]+matrix[1,2]+matrix[1,3]+matrix[1,4]+matrix[1,5]+matrix[1,6]>=38);
% sum of column E = 21
constraint (matrix[1,5]+matrix[2,5]+matrix[3,5]+matrix[4,5]+matrix[5,5]+matrix[6,5]=21);

% === Setting for Rows ===
% All different in row 1
constraint alldifferent( [ matrix[1,j] | j in 1..6 ]); 
% All different except 2x6 in row 2
constraint all_different_except(matrix[2, 1..6], {6});
constraint count([matrix[2, j] | j in 1..6], 6) = 2;
% No 1 in row 2
constraint forall(j in 1..6) (matrix[2,j] != 1);
% All different except 2x3 in row 3
constraint all_different_except(matrix[3, 1..6], {3});
constraint count([matrix[3, j] | j in 1..6], 3) = 2;
% All different except 2x5 in row 4
constraint all_different_except(matrix[4, 1..6], {5});
constraint count([matrix[4, j] | j in 1..6], 5) = 2;
% No 4 in row 4
constraint forall(j in 1..6) (matrix[4,j] != 4);
% All different except 3x7 in row 5
constraint all_different_except(matrix[5, 1..6], {7});
constraint count([matrix[5, j] | j in 1..6], 7) = 3;
% No 2 in row 5
constraint forall(j in 1..6) (matrix[5,j] != 2);
% All different except 2x8 in row 6
constraint all_different_except(matrix[6, 1..6], {8});
constraint count([matrix[6, j] | j in 1..6], 8) = 2;
% No 3 in row 6
constraint forall(j in 1..6) (matrix[6,j] != 3);
% Neighbors in rows cannot be the same
constraint forall(i in 1..6) (forall(j in 2..6) (matrix[i,j] != matrix[i,j-1]));

% === Setting for Columnns ===
% All different in columns 1, 3, and 5
constraint alldifferent( [ matrix[i,1] | i in 1..6 ]); 
constraint alldifferent( [ matrix[i,3] | i in 1..6 ]); 
constraint alldifferent( [ matrix[i,5] | i in 1..6 ]); 
% All different except 2x3 in col B
constraint all_different_except(matrix[1..6, 2], {3});
constraint count([matrix[i, 2] | i in 1..6], 3) = 2;
% Only even digits in column B except for the 2 Threes
constraint forall(i in 1..6 where matrix[i,2]!=3) (matrix[i,2]=2 \/ matrix[i,2]=4 \/ matrix[i,2]=6 \/ matrix[i,2]=8);
% No 2 in column C
constraint forall(i in 1..6) (matrix[i,3] != 2);
% All different except 2x8 in col D
constraint all_different_except(matrix[1..6, 4], {8});
constraint count([matrix[i, 4] | i in 1..6], 8) = 2;
% All different except 2x9 in col F
constraint all_different_except(matrix[1..6, 6], {9});
constraint count([matrix[i, 6] | i in 1..6], 9) = 2;
% Neighbors in cols cannot be the same
constraint forall(i in 2..6) (forall(j in 1..6) (matrix[i,j] != matrix[i-1,j]));

% Column A: asc. or desc. Sequence
constraint (matrix[1,1]=matrix[2,1]+1/\matrix[2,1]=matrix[3,1]+1/\matrix[3,1]=matrix[4,1]+1/\
            matrix[4,1]=matrix[5,1]+1/\matrix[5,1]=matrix[6,1]+1) \/
           (matrix[1,1]+1=matrix[2,1]/\matrix[2,1]+1=matrix[3,1]/\matrix[3,1]+1=matrix[4,1]/\
            matrix[4,1]+1=matrix[5,1]/\matrix[5,1]+1=matrix[6,1]);

% All Digits must occur 4x in the matrix
constraint count([matrix[i,j] | i,j in 1..6], 1) = 4;
constraint count([matrix[i,j] | i,j in 1..6], 2) = 4;
constraint count([matrix[i,j] | i,j in 1..6], 3) = 4;
constraint count([matrix[i,j] | i,j in 1..6], 4) = 4;
constraint count([matrix[i,j] | i,j in 1..6], 5) = 4;
constraint count([matrix[i,j] | i,j in 1..6], 6) = 4;
constraint count([matrix[i,j] | i,j in 1..6], 7) = 4;
constraint count([matrix[i,j] | i,j in 1..6], 8) = 4;
constraint count([matrix[i,j] | i,j in 1..6], 9) = 4;

solve satisfy;

output ["S O L U T I O N \n",
        "=============== \n",
        "R/C\t A\t B\t C\t D\t E\t F \n",
        "-------------------------------------------------------\n",
        "1\t \(matrix[1,1])\t \(matrix[1,2])\t \(matrix[1,3])\t \(matrix[1,4])\t \(matrix[1,5])\t \(matrix[1,6])  \n",
        "2\t \(matrix[2,1])\t \(matrix[2,2])\t \(matrix[2,3])\t \(matrix[2,4])\t \(matrix[2,5])\t \(matrix[2,6])  \n",
        "3\t \(matrix[3,1])\t \(matrix[3,2])\t \(matrix[3,3])\t \(matrix[3,4])\t \(matrix[3,5])\t \(matrix[3,6])  \n",
        "4\t \(matrix[4,1])\t \(matrix[4,2])\t \(matrix[4,3])\t \(matrix[4,4])\t \(matrix[4,5])\t \(matrix[4,6])  \n",
        "5\t \(matrix[5,1])\t \(matrix[5,2])\t \(matrix[5,3])\t \(matrix[5,4])\t \(matrix[5,5])\t \(matrix[5,6])  \n",
        "6\t \(matrix[6,1])\t \(matrix[6,2])\t \(matrix[6,3])\t \(matrix[6,4])\t \(matrix[6,5])\t \(matrix[6,6])  \n" ];

我确信有些代码部分可以写得更优雅。但我很高兴今天在 MiniZinc 中构建了我的第一个解决方案。

感谢您的所有意见！