求解9x9数独时出现“unsatisfiable”错误的原因咨询

核心错误分析 #

1. 变量赋值顺序错误 #

你在定义变量之前就直接给变量赋值（比如a2=6;这类语句写在var 1..9: a2;之前），这不符合MiniZinc的语法规范。变量必须先声明类型和范围，才能进行赋值操作。

2. 全局alldifferent约束完全错误 #

你写的第一个约束：

constraint alldifferent([a1,a2,a3,a4,a5,a6,a7,a8,a9,b1,b2,b3,b4,b5,b6,b7,b8,b9,c1,c2,c3,c4,c5,c6,c7,c8,c9,d1,d2,d3,d4,d5,d6,d7,d8,d9,e1,e2,e3,e4,e5,e6,e7,e8,e9,e1,e2,e3,e4,e5,e6,e7,e8,e9,e1,e2,e3,e4,e5,e6,e7,e8,e9,f1,f2,f3,f4,f5,f6,f7,f8,f9,g1,g2,g3,g4,g5,g6,g7,g8,g9,i1,i2,i3,i4,i5,i6,i7,i8,i9,]);

不仅要求所有81个数独格子都必须不同（数独规则是每行、每列、每宫各自不同，不是全局所有格子不同），还重复添加了三次e行的变量，这直接导致约束矛盾，必然无解。

3. 冗余且不完整的两两不等约束 #

你添加的a1 != a2这类约束完全多余——alldifferent已经能保证同一集合内的所有元素互不相等。同时这些约束只覆盖了每行第一个元素和其他元素的不等，没有处理列和3x3宫的唯一性要求，约束完全不完整。

4. 缺失关键约束 #

原代码没有添加列的唯一性约束和3x3宫的唯一性约束，这是数独规则的核心部分，缺少这些约束就算语法正确也无法得到合法的数独解。

修正后的代码示例 #

include "alldifferent.mzn";

// 先定义所有变量，同时给已知值赋值
var 1..9: a1;
var 1..9: a2 = 6;
var 1..9: a3;
var 1..9: a4 = 1;
var 1..9: a5;
var 1..9: a6 = 4;
var 1..9: a7;
var 1..9: a8 = 5;
var 1..9: a9;

var 1..9: b1;
var 1..9: b2;
var 1..9: b3 = 8;
var 1..9: b4 = 3;
var 1..9: b5;
var 1..9: b6 = 5;
var 1..9: b7 = 6;
var 1..9: b8;
var 1..9: b9;

var 1..9: c1 = 8;
var 1..9: c2;
var 1..9: c3;
var 1..9: c4;
var 1..9: c5;
var 1..9: c6;
var 1..9: c7;
var 1..9: c8;
var 1..9: c9 = 6;

var 1..9: d1 = 8;
var 1..9: d2;
var 1..9: d3;
var 1..9: d4 = 4;
var 1..9: d5;
var 1..9: d6 = 7;
var 1..9: d7;
var 1..9: d8;
var 1..9: d9 = 6;

var 1..9: e1;
var 1..9: e2;
var 1..9: e3 = 6;
var 1..9: e4;
var 1..9: e5;
var 1..9: e6;
var 1..9: e7 = 3;
var 1..9: e8;
var 1..9: e9;

var 1..9: f1 = 7;
var 1..9: f2;
var 1..9: f3;
var 1..9: f4 = 9;
var 1..9: f5;
var 1..9: f6 = 1;
var 1..9: f7;
var 1..9: f8;
var 1..9: f9 = 4;

var 1..9: g1 = 5;
var 1..9: g2;
var 1..9: g3;
var 1..9: g4;
var 1..9: g5;
var 1..9: g6;
var 1..9: g7;
var 1..9: g8;
var 1..9: g9 = 2;

var 1..9: h1;
var 1..9: h2;
var 1..9: h3 = 7;
var 1..9: h4 = 2;
var 1..9: h5;
var 1..9: h6 = 6;
var 1..9: h7 = 9;
var 1..9: h8;
var 1..9: h9;

var 1..9: i1;
var 1..9: i2 = 4;
var 1..9: i3;
var 1..9: i4 = 5;
var 1..9: i5;
var 1..9: i6 = 8;
var 1..9: i7;
var 1..9: i8 = 7;
var 1..9: i9;

// 行约束：每行所有元素不同
constraint alldifferent([a1,a2,a3,a4,a5,a6,a7,a8,a9]);
constraint alldifferent([b1,b2,b3,b4,b5,b6,b7,b8,b9]);
constraint alldifferent([c1,c2,c3,c4,c5,c6,c7,c8,c9]);
constraint alldifferent([d1,d2,d3,d4,d5,d6,d7,d8,d9]);
constraint alldifferent([e1,e2,e3,e4,e5,e6,e7,e8,e9]);
constraint alldifferent([f1,f2,f3,f4,f5,f6,f7,f8,f9]);
constraint alldifferent([g1,g2,g3,g4,g5,g6,g7,g8,g9]);
constraint alldifferent([h1,h2,h3,h4,h5,h6,h7,h8,h9]);
constraint alldifferent([i1,i2,i3,i4,i5,i6,i7,i8,i9]);

// 列约束：每列所有元素不同
constraint alldifferent([a1,b1,c1,d1,e1,f1,g1,h1,i1]);
constraint alldifferent([a2,b2,c2,d2,e2,f2,g2,h2,i2]);
constraint alldifferent([a3,b3,c3,d3,e3,f3,g3,h3,i3]);
constraint alldifferent([a4,b4,c4,d4,e4,f4,g4,h4,i4]);
constraint alldifferent([a5,b5,c5,d5,e5,f5,g5,h5,i5]);
constraint alldifferent([a6,b6,c6,d6,e6,f6,g6,h6,i6]);
constraint alldifferent([a7,b7,c7,d7,e7,f7,g7,h7,i7]);
constraint alldifferent([a8,b8,c8,d8,e8,f8,g8,h8,i8]);
constraint alldifferent([a9,b9,c9,d9,e9,f9,g9,h9,i9]);

// 3x3宫约束：每个宫内所有元素不同
constraint alldifferent([a1,a2,a3,b1,b2,b3,c1,c2,c3]); // 左上宫
constraint alldifferent([a4,a5,a6,b4,b5,b6,c4,c5,c6]); // 中上宫
constraint alldifferent([a7,a8,a9,b7,b8,b9,c7,c8,c9]); // 右上宫
constraint alldifferent([d1,d2,d3,e1,e2,e3,f1,f2,f3]); // 左中宫
constraint alldifferent([d4,d5,d6,e4,e5,e6,f4,f5,f6]); // 中中宫
constraint alldifferent([d7,d8,d9,e7,e8,e9,f7,f8,f9]); // 右中宫
constraint alldifferent([g1,g2,g3,h1,h2,h3,i1,i2,i3]); // 左下宫
constraint alldifferent([g4,g5,g6,h4,h5,h6,i4,i5,i6]); // 中下宫
constraint alldifferent([g7,g8,g9,h7,h8,h9,i7,i8,i9]); // 右下宫

solve satisfy;

output[
    show(a1), " ", show(a2), " ", show(a3), " | ",
    show(a4), " ", show(a5), " ", show(a6), " | ",
    show(a7), " ", show(a8), " ", show(a9), "\n",
    show(b1), " ", show(b2), " ", show(b3), " | ",
    show(b4), " ", show(b5), " ", show(b6), " | ",
    show(b7), " ", show(b8), " ", show(b9), "\n",
    show(c1), " ", show(c2), " ", show(c3), " | ",
    show(c4), " ", show(c5), " ", show(c6), " | ",
    show(c7), " ", show(c8), " ", show(c9), "\n",
    "---------------------", "\n",
    show(d1), " ", show(d2), " ", show(d3), " | ",
    show(d4), " ", show(d5), " ", show(d6), " | ",
    show(d7), " ", show(d8), " ", show(d9), "\n",
    show(e1), " ", show(e2), " ", show(e3), " | ",
    show(e4), " ", show(e5), " ", show(e6), " | ",
    show(e7), " ", show(e8), " ", show(e9), "\n",
    show(f1), " ", show(f2), " ", show(f3), " | ",
    show(f4), " ", show(f5), " ", show(f6), " | ",
    show(f7), " ", show(f8), " ", show(f9), "\n",
    "---------------------", "\n",
    show(g1), " ", show(g2), " ", show(g3), " | ",
    show(g4), " ", show(g5), " ", show(g6), " | ",
    show(g7), " ", show(g8), " ", show(g9), "\n",
    show(h1), " ", show(h2), " ", show(h3), " | ",
    show(h4), " ", show(h5), " ", show(h6), " | ",
    show(h7), " ", show(h8), " ", show(h9), "\n",
    show(i1), " ", show(i2), " ", show(i3), " | ",
    show(i4), " ", show(i5), " ", show(i6), " | ",
    show(i7), " ", show(i8), " ", show(i9), "\n"
];

额外说明 #

• 修正后的代码先声明变量并赋值已知数，然后分别添加行、列、3x3宫的alldifferent约束，完全符合数独规则。
• 输出部分添加了空格和分隔线，让结果更易读。

内容的提问来源于stack exchange，提问作者Noor