在《我的世界》(Minecraft) 中，捆绑包（Bundle）是一种独特的物品，它允许玩家将多种不同类型的物品打包在一起，极大地提高了物品栏的管理效率。然而，捆绑包的填充规则并非简单地累加物品数量，而是基于一个独特的“装填度”系统，这使得“如何最优化地填满一个捆绑包”成为一个有趣的组合优化问题。
许多文章可能已经探讨过使用现成的求解器来解决这类问题，但本文将下沉一级，专注于整个流程中最关键且最考验思维精确度的环节：建模。我们将详细拆解如何将《我的世界》中的游戏逻辑，一步步精确地翻译成 Z3（一个强大的 SMT 求解器）能够理解的数学约束。这不仅是一个游戏策略问题，更是一次将现实世界复杂规则形式化、逻辑化的绝佳实践。
理解捆绑包的核心机制：装填度
要为问题建模，首先必须精确理解其规则。捆绑包的核心机制并非物品“数量”或“种类”，而是一个名为“装填度”（Fullness）的内部值。一个空的捆绑包总容量为 64 点装填度。玩家放入的每一种物品都会消耗一定的装填度，直到总和达到 64 为止。
关键在于，每件物品消耗的装填度与其自身的“最大堆叠数量”（Max Stack Size）负相关。这个规则可以总结为以下公式：
单个物品消耗的装填度 = 64 / 该物品的最大堆叠数量
这个设计非常精妙，它使得无论是大批量堆叠的方块，还是不可堆叠的珍稀工具，都能被统一量化。让我们看几个例子：
| 物品 (Item) |
最大堆叠数量 (Max Stack Size) |
单个物品消耗的装填度 |
计算过程 |
| 泥土 (Dirt) |
64 |
1 |
64 / 64 |
| 鸡蛋 (Egg) |
16 |
4 |
64 / 16 |
| 信号桶 (Beacon) |
1 |
64 |
64 / 1 |
| 钻石剑 (Diamond Sword) |
1 |
64 |
64 / 1 |
从表中可以清晰地看到：
- 像泥土这样可以大量堆叠的物品，每件只占用 1 点装填度。
- 像鸡蛋这样中等数量堆叠的物品，每件占用的装填度更高。
- 而像钻石剑、信号桶这样完全不可堆叠的物品，只要放入一件，就会直接占满整个捆绑包的 64 点装填度。
因此，我们的优化问题的本质，就是在给定一系列可用物品的情况下，挑选一个组合，使其总装填度恰好（或尽可能接近）64。
将游戏规则翻译成 Z3 的数学约束
Z3 是一个定理证明器和约束求解器。我们不需要告诉它如何去“计算”结果，只需要用逻辑和数学语言向它“描述”什么是合法的解（即满足所有约束的解）。Z3 会利用其强大的内部算法，为我们找到一个或多个符合条件的解。
下面，我们将这个过程分解为三个步骤。
步骤 1：定义决策变量
建模的第一步是确定问题中的“未知数”。在这个场景下，未知数就是“我们应该在捆绑包中放入每种物品各多少个？”。假设我们当前物品栏里有泥土、鸡蛋和一把钻石剑可供选择，我们可以为每种物品定义一个整型（Integer）变量来代表其数量。
在 Z3 的 SMT-LIB 语言中，这可以表示为：
; 为每种物品定义一个整型常量（变量）
(declare-const dirt_count Int)
(declare-const egg_count Int)
(declare-const sword_count Int)
步骤 2：施加基本约束
接下来，我们需要根据常识和游戏规则，为这些变量添加约束。
-
数量非负约束：放入捆绑包的物品数量不可能是负数。
(assert (>= dirt_count 0))
(assert (>= egg_count 0))
(assert (>= sword_count 0))
-
可用库存约束：我们放入捆绑包的物品数量，不能超过我们物品栏里实际拥有的数量。假设我们有 100 块泥土、20 个鸡蛋和 1 把钻石剑。
(assert (<= dirt_count 100))
(assert (<= egg_count 20))
(assert (<= sword_count 1))
步骤 3：施加核心的“装填度”约束
这是整个建模过程的核心。我们需要将前文分析的“装填度”公式转化为一个线性不等式。根据公式，总装填度是每种物品的数量乘以其单位装填度的总和。这个总和必须小于等于 64。
dirt_count * 1 (泥土的总装填度)egg_count * 4 (鸡蛋的总装填度)sword_count * 64 (钻石剑的总装填度)
将它们加总并约束在 64 以内，Z3 的断言（assert）如下：
(assert (<= (+ (* dirt_count 1) (* egg_count 4) (* sword_count 64)) 64))
这个表达式精确地捕捉了捆绑包的容量限制。+ 和 * 分别代表加法和乘法，整个语句的含义是“（泥土数量 * 1 + 鸡蛋数量 * 4 + 钻石剑数量 * 64）的结果必须小于或等于 64”。
整合与求解：一个完整的 Z3 脚本
现在，我们将所有部分组合成一个完整的 Z3 脚本。除了找到一个“可行解”，我们通常还想找到一个“最优解”。例如，我们可能希望在不超载的前提下，让捆绑包的装填度尽可能高。这可以通过 maximize 指令实现。
; --- 1. 定义决策变量 ---
(declare-const dirt_count Int)
(declare-const egg_count Int)
(declare-const sword_count Int)
; --- 2. 施加约束 ---
; 数量非负
(assert (>= dirt_count 0))
(assert (>= egg_count 0))
(assert (>= sword_count 0))
; 可用库存限制 (假设有 100 泥土, 20 鸡蛋, 1 钻石剑)
(assert (<= dirt_count 100))
(assert (<= egg_count 20))
(assert (<= sword_count 1))
; 核心：捆绑包总装填度 <= 64
(assert (<= (+ (* dirt_count 1) ; 泥土 (单位装填度 1)
(* egg_count 4) ; 鸡蛋 (单位装填度 4)
(* sword_count 64)) ; 钻石剑 (单位装填度 64)
64))
; --- 3. 设定优化目标 ---
; 目标：最大化总装填度
(maximize (+ (* dirt_count 1) (* egg_count 4) (* sword_count 64)))
; --- 4. 求解与输出 ---
(check-sat) ; 检查是否存在满足所有约束的解
(get-model) ; 如果存在，输出一组具体的变量值
当我们将这个脚本交给 Z3 求解时，它可能会返回类似这样的结果：
sat
(
(define-fun sword_count () Int 0)
(define-fun egg_count () Int 16)
(define-fun dirt_count () Int 0)
)
这个结果告诉我们：
(check-sat) 的结果是 sat，表示问题有解。(get-model) 给出了一个最优解：放入 0 把钻石剑、16 个鸡蛋和 0 块泥土。- 在这个解中，总装填度为
0*64 + 16*4 + 0*1 = 64，恰好填满了整个捆绑包，实现了我们的优化目标。
如果我们改变库存，比如我们只有 15 个鸡蛋，Z3 会自动找到下一个最优解，可能是 15*4 + 4*1 = 64，即 15 个鸡蛋和 4 块泥土。
结论：建模是思考的艺术
通过这个《我的世界》捆绑包的例子，我们完整地体验了将一个具体、带有独特规则的游戏机制，抽象并形式化为数学约束的过程。这个过程的价值远超游戏本身。无论是物流规划、资源调度还是金融建模，其核心都是识别问题中的变量、约束和优化目标，然后用形式化语言将其精确地描述出来。
Z3 这类工具的强大之处在于，一旦建模完成，求解过程就是自动的。真正的挑战和智力活动，在于前期对问题深刻的理解和精确的“翻译”能力。学会如何将现实世界的模糊逻辑转化为求解器能够理解的严谨数学，是连接领域知识和计算能力的桥梁，也是所有工程师和问题解决者都应具备的核心技能。