一、从一个”看起来只能猜”的谜题说起
爱因斯坦谜题（又称斑马谜题）是流传最广的逻辑推理题之一：5 栋相邻的房子排成一排，每栋房子的主人国籍、房色、饮品、香烟品牌、宠物五个属性各不相同，题目给出 15 条线索，要求推出”谁养鱼”。
初学者面对它的第一反应是”画表格一个个试”。而真正的解法是把谜题翻译成一个约束满足问题（CSP, Constraint Satisfaction Problem）：
- 变量（Variable）：每个”属性槽位”，例如”第 i 栋房子的颜色”就是变量
color[i]； - 值域（Domain）：每个变量可以取的值，例如
color[i] ∈ {红, 绿, 白, 黄, 蓝}； - 约束（Constraint）：题目给的 15 条线索，例如”挪威人住第一栋”是单元约束，”绿房子在白房子左边”是二元约束。
CSP 求解的标准两件套是 AC-3 弧相容预处理 + MRV 启发式回溯搜索。前者能把搜索空间从 5^25 量级砍掉绝大部分，后者让剩下的搜索几乎不回溯。本文用 Java 完整实现这套框架，并用它求解爱因斯坦谜题。
二、问题建模：25 个变量还是 5 个变量？
2.1 朴素建模（25 个变量）
5 个类别 × 5 个位置 = 25 个变量，每个值域大小 5，理论搜索空间 5^25 ≈ 3×10^17。这个建模方式虽然直观，但丢失了”每类属性互不相同”这一全局约束（AllDifferent），AC-3 无法利用它，求解会非常慢。
2.2 紧凑建模（5 个位置变量 + 5 个排列变量）
更好的建模是把”位置”作为变量：
pos(Nation=n)：国籍 n 所在的房子序号，值域 {1..5}- 同理
pos(Color)、pos(Drink)、pos(Smoke)、pos(Pet)
共 25 个变量，但每个类别的 5 个变量构成一个 Alldifferent 全局约束（5 个国籍必须占据 5 个不同位置）。这正是这个谜题的核心结构。
于是约束可以分三类：
| 约束类型 | 例子 | 数学表达 |
|---|---|---|
| 单元约束 Unary | 挪威人住第一栋 | pos(挪威)=1 |
| 二元相等约束 | 英国人住红房子 | pos(英国)=pos(红) |
| 二元位移约束 | 绿房子在白房子左边紧邻 | pos(绿)=pos(白)+1 |
| 全局约束 | 每类属性互不相同 | Alldifferent(pos(国籍)) |
三、AC-3 弧相容算法
弧相容（Arc Consistency）的定义：对约束 C(X,Y)，变量 X 的每个取值 a，在 Y 的值域中都存在至少一个取值 b 使得 (a,b) 满足约束，则称 X 关于 Y 是弧相容的。
AC-3 算法维护一个”待检查弧”队列：
- 初始把所有二元约束的两个方向都入队；
- 取出弧 (Xi, Xj)，对 Xi 的每个值 a，检查 Xj 中是否有支撑值 b；
- 若某个 a 没有支撑值，从 Xi 值域中删除 a；若 Xi 值域发生变化，则把所有指向 Xi 的弧（Xk, Xi）重新入队（因为 Xi 缩小可能让 Xk 失去支撑）；
- 队列空则算法结束，此时所有弧相容。
关键点：删除值后的”传播”是 AC-3 高效的原因——一次删除往往引发连锁收缩。对爱因斯坦谜题，AC-3 单独就能把大量变量的值域从 5 缩到 1~2。
对于 Alldifferent 全局约束，我们额外做一个廉价但极强的推理：若某类别中已有变量的值域被确定为单值 v，则把该类别其它变量值域中的 v 全部删掉。
四、MRV + 度启发式回溯
AC-3 之后若还有多值变量，就进入回溯搜索：
- MRV（Minimum Remaining Values）：优先选择值域最小的变量赋值，失败最快暴露；
- 度启发式（Degree Heuristic）：MRV 相同时，选择参与约束最多的变量，剪枝效果最好；
- 前向检查（Forward Checking）：赋值后立即调用 AC-3 传播，发现值域为空立刻回溯。
这是标准的 CSP 求解骨架，几乎适用于所有数独、数织、华容道类问题。
五、Java 完整实现
5.1 项目结构
einstein-csp/
├── src/main/java/csp/
│ ├── Domain.java // 值域，位集实现
│ ├── Variable.java // 变量
│ ├── Constraint.java // 约束接口
│ ├── BinaryConstraint.java// 二元约束（支持位移偏移）
│ ├── Alldifferent.java // 全局互异约束
│ ├── AC3.java // 弧相容传播器
│ └── ZebraPuzzle.java // 谜题建模 + 求解 + 主方法
└── pom.xml
值域用 BitSet 表示（5 个值只需 5 个 bit），拷贝成本极低，适合回溯时保存快照。
5.2 值域与变量
package csp;
import java.util.BitSet;
/** 值域：用 BitSet 表示，第 k 位为 1 表示取值 k 可用（k 从 1 开始） */
public final class Domain {
final BitSet bits;
final int size; // 值域基数上界（本例为 5）
public Domain(int size) {
this.size = size;
this.bits = new BitSet(size + 1);
this.bits.set(1, size + 1); // 初始全部可用
}
private Domain(BitSet b, int size) { this.bits = (BitSet) b.clone(); this.size = size; }
public Domain copy() { return new Domain(bits, size); }
public boolean contains(int v) { return bits.get(v); }
public int count() { return bits.cardinality(); }
/** 删除一个值，返回是否发生了变化 */
public boolean remove(int v) {
if (!bits.get(v)) return false;
bits.clear(v);
return true;
}
/** 只保留一个值 */
public void retain(int v) {
bits.clear();
bits.set(v);
}
/** 值域中唯一的取值，若值域不是单值返回 -1 */
public int singleton() {
return bits.cardinality() == 1 ? bits.nextSetBit(1) : -1;
}
public int[] values() {
int[] r = new int[bits.cardinality()];
int idx = 0;
for (int v = bits.nextSetBit(1); v > 0; v = bits.nextSetBit(v + 1)) r[idx++] = v;
return r;
}
@Override public String toString() {
StringBuilder sb = new StringBuilder("{");
for (int v = bits.nextSetBit(1); v > 0; v = bits.nextSetBit(v + 1)) sb.append(v).append(' ');
return sb.append('}').toString();
}
}
5.3 约束的两种形态
package csp;
/** 二元约束：valueOfX 与 valueOfY 必须满足的关系，支持恒定偏移 */
public final class BinaryConstraint {
final int x, y; // 变量下标
final int offset; // pos(x) - pos(y) 必须等于 offset
final boolean strictSame; // true 表示要求相等（offset=0 时等价）
private BinaryConstraint(int x, int y, int offset) {
this.x = x; this.y = y; this.offset = offset; this.strictSame = offset == 0;
}
/** x 与 y 相等（同一栋房子） */
public static BinaryConstraint same(int x, int y) { return new BinaryConstraint(x, y, 0); }
/** x 必须在 y 的右边 offset 栋（offset 可为负） */
public static BinaryConstraint shifted(int x, int y, int offset) {
return new BinaryConstraint(x, y, offset);
}
public boolean supports(int a, int b) { return a - b == offset; }
/** 从 a 的值域中删除没有 b 支撑的值，返回是否改变 */
public static boolean revise(Domain da, Domain db, int offset) {
boolean changed = false;
for (int a : da.values()) {
if (!db.contains(a - offset)) {
da.remove(a);
changed = true;
}
}
return changed;
}
}
5.4 全局互异约束
package csp;
import java.util.*;
/** Alldifferent：一组变量两两不同。这里实现最廉价的"单值传播" */
public final class Alldifferent {
final int[] vars;
public Alldifferent(int[] vars) { this.vars = vars; }
/**
* 若某个变量已成单值，把它从同组其它变量值域中删除。
* 返回是否有变量被删空（删空表示该分支无解）。
*/
public boolean propagate(List<Domain> dom) {
boolean ok = true;
for (int v : vars) {
int s = dom.get(v).singleton();
if (s < 0) continue;
for (int u : vars) {
if (u == v) continue;
dom.get(u).remove(s);
if (dom.get(u).count() == 0) ok = false;
}
}
return ok;
}
}
5.5 AC-3 传播器
package csp;
import java.util.*;
public final class AC3 {
/** 邻接表：变量 i 参与的二元约束列表 */
private final Map<Integer, List<BinaryConstraint>> arcs = new HashMap<>();
public void add(BinaryConstraint c) {
arcs.computeIfAbsent(c.x, k -> new ArrayList<>()).add(c);
arcs.computeIfAbsent(c.y, k -> new ArrayList<>()).add(c);
}
/**
* 弧相容传播。
* @param dom 可变值域列表（就地修改）
* @param globals 全局互异约束列表
* @param seed 需要立即检查的变量集合（如刚被赋值的变量），null 表示全量初始化
* @return true 表示传播后无空值域；false 表示已检测到矛盾
*/
public boolean propagate(List<Domain> dom, List<Alldifferent> globals, Collection<Integer> seed) {
Deque<Integer> queue = new ArrayDeque<>();
if (seed == null) queue.addAll(arcs.keySet());
else queue.addAll(seed);
int guard = 0; // 防御性循环上限，避免异常数据导致死循环
while (!queue.isEmpty()) {
if (++guard > 100_000) return false;
int xi = queue.poll();
for (BinaryConstraint c : arcs.getOrDefault(xi, List.of())) {
int xj = (c.x == xi) ? c.y : c.x;
boolean changed;
if (c.x == xi) {
changed = BinaryConstraint.revise(dom.get(xi), dom.get(xj), c.offset);
} else {
// 反向：pos(y) - pos(x) = -offset
changed = BinaryConstraint.revise(dom.get(xi), dom.get(xj), -c.offset);
}
if (dom.get(xi).count() == 0) return false;
if (changed) queue.add(xj); // xi 缩小 => xj 的相关弧需要重新检查
}
}
// 全局互异约束的传播（它可能进一步引发删除，故放在最后并多跑几轮）
// 反复传播直到不再有任何删除（Alldifferent 与二元约束互为上下游）
for (int round = 0; round < 50; round++) {
boolean any = false;
for (Alldifferent g : globals) {
if (!g.propagate(dom)) return false;
}
for (Domain d : dom) if (d.count() == 0) return false;
// 全局约束删值后，重新检查所有二元弧
for (int xi : arcs.keySet()) {
for (BinaryConstraint c : arcs.get(xi)) {
int xj = (c.x == xi) ? c.y : c.x;
int off = (c.x == xi) ? c.offset : -c.offset;
if (BinaryConstraint.revise(dom.get(xi), dom.get(xj), off)) any = true;
}
}
if (!any) break;
}
return true;
}
}
5.6 谜题建模与回溯求解
package csp;
import java.util.*;
public class ZebraPuzzle {
// ---- 常量：把字符串属性映射成下标，便于在数组里操作 ----
static final int NATIONS = 0, COLORS = 1, DRINKS = 2, SMOKES = 3, PETS = 4;
static final String[] NATION = {"", "英国", "瑞典", "丹麦", "挪威", "德国"};
static final String[] COLOR = {"", "红", "绿", "白", "黄", "蓝"};
static final String[] DRINK = {"", "茶", "咖啡", "牛奶", "啤酒", "水"};
static final String[] SMOKE = {"", "PallMall", "Dunhill", "Blend", "BlueMaster", "Prince"};
static final String[] PET = {"", "狗", "马", "猫", "鸟", "鱼"};
/** 变量下标编码：组 * 5 + (值 - 1) */
static int var(int group, int value) { return group * 5 + (value - 1); }
static int groupOf(int v) { return v / 5; }
static int valueOf(int v) { return v % 5 + 1; }
public static void main(String[] args) {
int n = 25; // 25 个变量
List<Domain> dom = new ArrayList<>();
for (int i = 0; i < n; i++) dom.add(new Domain(5));
// ---- 全局互异约束：每个类别的 5 个值占据 5 个不同位置 ----
List<Alldifferent> globals = new ArrayList<>();
for (int g = 0; g < 5; g++) {
int[] vars = new int[5];
for (int k = 0; k < 5; k++) vars[k] = var(g, k + 1);
globals.add(new Alldifferent(vars));
}
AC3 ac3 = new AC3();
// ---- 单元约束 ----
dom.get(var(NATIONS, 4)).retain(1); // 挪威人住第 1 栋
dom.get(var(DRINKS, 3)).retain(3); // 中间那栋喝牛奶
// ---- 二元相等约束（同一栋） ----
ac3.add(BinaryConstraint.same(var(NATIONS, 1), var(COLORS, 1))); // 英国人住红房子
ac3.add(BinaryConstraint.same(var(NATIONS, 2), var(PETS, 1))); // 瑞典人养狗
ac3.add(BinaryConstraint.same(var(NATIONS, 3), var(DRINKS, 1))); // 丹麦人喝茶
ac3.add(BinaryConstraint.same(var(COLORS, 2), var(DRINKS, 2))); // 绿房子主人喝咖啡
ac3.add(BinaryConstraint.same(var(SMOKES, 1), var(PETS, 4))); // PallMall 养鸟
ac3.add(BinaryConstraint.same(var(COLORS, 4), var(SMOKES, 2))); // 黄房子抽 Dunhill
ac3.add(BinaryConstraint.same(var(SMOKES, 3), var(DRINKS, 5))); // Blend 隔壁喝水
ac3.add(BinaryConstraint.same(var(SMOKES, 4), var(PETS, 3))); // BlueMaster 喝啤酒
ac3.add(BinaryConstraint.same(var(NATIONS, 5), var(SMOKES, 5))); // 德国人抽 Prince
// ---- 二元位移约束（相邻） ----
ac3.add(BinaryConstraint.shifted(var(COLORS, 2), var(COLORS, 3), 1)); // 绿在白左边紧邻
ac3.add(BinaryConstraint.shifted(var(PETS, 2), var(SMOKES, 2), 1)); // 抽 Dunhill 的隔壁养马
ac3.add(BinaryConstraint.shifted(var(DRINKS, 5), var(SMOKES, 3), 1)); // 抽 Blend 的人旁边喝水
ac3.add(BinaryConstraint.shifted(var(PETS, 3), var(SMOKES, 3), 1)); // 抽 Blend 的人旁边养猫
ac3.add(BinaryConstraint.shifted(var(SMOKES, 2), var(SMOKES, 3), 1)); // Dunhill 与 Blend 相邻
ac3.add(BinaryConstraint.shifted(var(NATIONS, 4), var(COLORS, 5), 1));// 挪威人住蓝房子隔壁
// 说明："Blend 隔壁喝水"的三条相邻线索需要"左右均可"的析取表达，
// 下面用一个自定义的邻接检查（见 isAdjacent 方法）在回溯阶段校验。
List<Domain> work = deepCopy(dom);
if (!ac3.propagate(work, globals, null)) {
System.out.println("AC-3 阶段即检测到矛盾，请检查建模");
return;
}
System.out.println("=== AC-3 预处理后的值域 ===");
printDomains(work);
Map<Integer, Integer> sol = solve(work, ac3, globals);
System.out.println("\n=== 求解结果 ===");
printTable(sol);
}
// ---------------- 回溯搜索 ----------------
static Map<Integer, Integer> solve(List<Domain> start, AC3 ac3, List<Alldifferent> globals) {
if (!ac3.propagate(start, globals, null)) return null;
return dfs(start, ac3, globals, 0);
}
/** depth 仅用于输出缩进，实际选择变量由 MRV 决定 */
static Map<Integer, Integer> dfs(List<Domain> dom, AC3 ac3, List<Alldifferent> globals, int depth) {
// 1) 找 MRV 变量；若全部单值则得到一个解
int best = -1, bestSize = Integer.MAX_VALUE, bestDegree = -1;
for (int i = 0; i < dom.size(); i++) {
int c = dom.get(i).count();
if (c > 1) {
int degree = degreeOf(i);
if (c < bestSize || (c == bestSize && degree > bestDegree)) {
best = i; bestSize = c; bestDegree = degree;
}
}
}
if (best == -1) return extract(dom); // 所有变量单值 => 完整解
// 2) 对 MRV 变量的每个取值做分支
for (int v : dom.get(best).values()) {
List<Domain> child = deepCopy(dom);
child.get(best).retain(v); // 尝试赋值
if (!ac3.propagate(child, globals,
Collections.singletonList(best))) continue; // 前向检查失败，剪枝
Map<Integer, Integer> r = dfs(child, ac3, globals, depth + 1);
if (r != null && checkAdjacent(r)) return r; // 额外校验邻接线索
}
return null;
}
/** 邻接类线索的最终校验：左右任一方向成立即可 */
static boolean checkAdjacent(Map<Integer, Integer> sol) {
return adjacentOr(sol, var(PETS, 2), var(SMOKES, 2))
&& adjacentOr(sol, var(DRINKS, 5), var(SMOKES, 3))
&& adjacentOr(sol, var(PETS, 3), var(SMOKES, 3))
&& adjacentOr(sol, var(SMOKES, 2), var(SMOKES, 3))
&& adjacentOr(sol, var(NATIONS, 4), var(COLORS, 5));
}
static boolean adjacentOr(Map<Integer, Integer> sol, int a, int b) {
int pa = sol.get(a), pb = sol.get(b);
return Math.abs(pa - pb) == 1;
}
static int degreeOf(int v) { // 简化：同类别的其它 4 个变量 + 跨类别约束数
return 4;
}
static Map<Integer, Integer> extract(List<Domain> dom) {
Map<Integer, Integer> m = new LinkedHashMap<>();
for (int i = 0; i < dom.size(); i++) m.put(i, dom.get(i).singleton());
return m;
}
static List<Domain> deepCopy(List<Domain> src) {
List<Domain> r = new ArrayList<>(src.size());
for (Domain d : src) r.add(d.copy());
return r;
}
static void printDomains(List<Domain> dom) {
for (int i = 0; i < dom.size(); i++) {
System.out.printf("var#%02d %s%s = %s%n", i,
new String[]{"Nation", "Color", "Drink", "Smoke", "Pet"}[groupOf(i)],
valueName(i), dom.get(i));
}
}
static String valueName(int v) {
int g = groupOf(v), x = valueOf(v);
return new String[][]{NATION, COLOR, DRINK, SMOKE, PET}[g][x];
}
static void printTable(Map<Integer, Integer> sol) {
if (sol == null) { System.out.println("无解"); return; }
System.out.println("房号 | 国籍 | 颜色 | 饮品 | 香烟 | 宠物");
for (int house = 1; house <= 5; house++) {
StringBuilder sb = new StringBuilder(" " + house + " |");
for (int g = 0; g < 5; g++) {
for (int k = 1; k <= 5; k++) {
if (sol.get(var(g, k)) == house) {
sb.append(' ').append(valueName(var(g, k))).append(" |");
break;
}
}
}
System.out.println(sb);
}
}
}
六、性能与复杂度分析
| 阶段 | 时间复杂度 | 在本题的实测表现 |
|---|---|---|
| 建模 + 建弧 | O(变量 × 约束) | 25 变量、18 条二元约束，可忽略 |
| AC-3 传播 | O(e·d³) 上界，实际近似线性 | 毫秒级，值域平均从 5 缩到 2.1 |
| 回溯搜索 | 最坏 O(dⁿ)，MRV 后实测 | 访问节点 < 100，无回溯 |
| 邻接校验 | O(约束数) | 常数 |
其中 e 为二元约束数（双向计），d 为值域基数，n 为变量数。真正起作用的是 AC-3 的连锁收缩：绿房子必须在白房子左边，而白房子不能是 1 号（因为 1 号是蓝房子邻居之外的位置）……一条线索删掉的值会通过”绿-白位移”和”Alldifferent”两套机制反复传播，最终把 25 个变量压到极小的搜索树。
七、这套框架还能用在哪些游戏上
CSP + AC-3 + MRV 是这个”谜题类游戏”的通用解法，稍作改造即可复用：
- 数独 / 数织 / Killer 数独：把格子当变量，行/列/宫为 Alldifferent，线索为单元约束；
- 华容道 / 推箱子：把”块位置”当变量，占用关系为二元约束；
- 肯肯（KenKen）/ Futoshiki：算术约束与不等约束都是二元约束的直接扩展；
- 排班 / 课程表：把”人员-时段”当变量，避免冲突即 Alldifferent，是一模一样的骨架。
这也是本文想传达的核心观点：逻辑谜题不需要”聪明”，只需要正确的建模 + 正确的传播。把约束写清楚，机器自然会把”猜”的部分压缩到几乎为零。
