从游戏到数学：将《我的世界》捆绑包问题精确建模为 Z3 约束

在《我的世界》(Minecraft) 中，管理库存是一门永恒的艺术。而在众多存储方案中，“捆绑包”（Bundle）无疑是最具趣味也最挑战逻辑思维的一个。它不像箱子那样提供简单的格子堆砌，而是引入了一套基于物品“堆叠属性”的独特容量系统。当玩家面对一堆杂物，想要最高效地利用捆绑包时，这个问题便从一个简单的游戏操作，升级为了一个典型的组合优化问题——更具体地说，是一个约束满足问题（Constraint Satisfaction Problem, CSP）。

许多文章已经探讨了如何使用 Z3 这类强大的 SMT (Satisfiability Modulo Theories) 求解器来解决游戏中的优化难题。然而，本文的切入点将下沉一级，我们不重点讨论求解器本身的高级功能，而是专注于基础却关键的“建模”过程：如何将《我的世界》中关于捆绑包的规则，一步步精确地翻译成 Z3 能理解的、形式化的数学约束。这对于任何希望利用求解器解决领域特定问题的人来说，是必须掌握的核心技能。

理解捆绑包的核心机制：非典型的“装箱问题”

要建立模型，首先必须精确理解问题的边界和规则。捆绑包的机制初看可能令人困惑，其核心规则可以总结如下：

单一库存槽位容量：一个捆绑包无论内部装了多少东西，它自身在玩家的库存中只占用一个格子。其内部总容量被设计为恰好等同于一个标准物品堆叠槽位的容量。
容量计算基于“分数”：捆绑包的“满载度”不是由物品的绝对数量决定的，而是由每个物品占其“最大堆叠数量”(Max Stack Size) 的比例决定的。例如，一个最大能堆叠 64 个的物品（如圆石），每放入一个，就占据捆绑包 1/64 的容量。一个最大能堆叠 16 个的物品（如雪球或末影珍珠），每放入一个，就占据 1/16 的容量。
总容量上限为 1：所有放入捆绑包的物品，其容量分数之和不能超过 1。例如，你可以放入 32 个圆石（32 * 1/64 = 1/2）和 8 个雪球（8 * 1/16 = 1/2），此时捆绑包恰好装满（1/2 + 1/2 = 1）。
不可堆叠物品的特殊性：像剑、镐、盔甲这类不可堆叠的物品，其“最大堆叠数量”被认为是 1。因此，只要放入一个不可堆叠物品，它就占据了 1/1 的容量，直接将捆绑包填满，无法再放入任何其他物品。

这个机制本质上是一个变种的“装箱问题”（Bin Packing Problem），但箱子的容量和物品的“重量”都由游戏规则动态定义，我们的任务就是将这些规则数学化。

从分数到整数：为 Z3 建模扫清障碍

直接使用分数（例如 1/64, 1/16）进行约束建模在 Z3 中是可行的（使用 Rat 实数类型），但这通常会引入不必要的计算复杂性，并可能导致精度问题。在 SMT 求解领域，一个标准的最佳实践是尽可能将问题转化为整数算术（Integer Arithmetic）。

要实现这一点，我们需要找到一个公分母来统一所有分数的计算。观察捆绑包的机制，最理想的“基准单位”就是 64，因为它是《我的世界》中最常见的最大堆叠数量。我们可以将捆绑包的总容量重新定义为 64 个“容量单位”。

在这个新体系下，每个物品的“重量”也相应地从分数转换为了整数：

物品重量 = 64 / 物品的最大堆叠数量

让我们用这个公式重新计算前面例子中物品的“重量”：

圆石 (Cobblestone)：最大堆叠 64，重量 = 64 / 64 = 1
雪球 (Snowball)：最大堆叠 16，重量 = 64 / 16 = 4
钻石剑 (Diamond Sword)：最大堆叠 1，重量 = 64 / 1 = 64

现在，核心的容量约束被漂亮地转换成了一个线性整数不等式：

Σ (物品 i 的数量 * 物品 i 的重量) ≤ 64

这个表达式简洁、高效，完美地适配了 Z3 求解器的整数运算核心，为我们接下来的建模铺平了道路。

使用 Z3py 构建约束模型

假设我们有一个 Python 环境，并且已经安装了 Z3 的 Python 绑定 z3-solver。现在，我们可以开始编写代码，将上述逻辑转化为 Z3py 脚本。

第一步：定义我们的物品库

首先，我们需要一个数据结构来存储我们当前拥有、并考虑放入捆绑包的物品信息。一个字典是十分合适的选择，其中包含了我们关心的所有属性：最大堆叠数、我们拥有的数量以及我们刚刚计算出的整数“重量”。

# 假设我们拥有以下物品
available_items = {
    "cobblestone": {"max_stack": 64, "available": 128, "weight": 1},
    "snowball": {"max_stack": 16, "available": 30, "weight": 4},
    "diamond_sword": {"max_stack": 1, "available": 1, "weight": 64},
    "oak_log": {"max_stack": 64, "available": 20, "weight": 1},
    "ender_pearl": {"max_stack": 16, "available": 5, "weight": 4}
}

第二步：为每个物品创建 Z3 决策变量

对于每一种希望放入捆绑包的物品，我们需要一个变量来代表“最终决定放入多少个”。在 Z3 中，我们使用 Int('variable_name') 来创建整数变量。

# 导入 Z3 库
from z3 import Int, Solver, Sum

# 为每种物品创建一个整数变量，代表要放入捆绑包的数量
item_vars = {
    name: Int(name) for name in available_items.keys()
}

第三步：添加核心约束

这是建模的核心环节。我们需要将所有游戏规则和逻辑限制，通过 solver.add() 方法告知 Z3。

数量非负约束：放入捆ля包的物品数量不能是负数。
库存上限约束：放入捆ля包的数量不能超过我们拥有的数量。
捆绑包容量约束：所有物品的总重量不能超过 64。

# 创建一个求解器实例
s = Solver()

# 添加约束
for name, var in item_vars.items():
    # 1. 数量必须大于等于 0
    s.add(var >= 0)
    # 2. 数量不能超过我们拥有的
    s.add(var <= available_items[name]['available'])

# 3. 核心约束：总重量不超过 64
total_weight = Sum([
    item_vars[name] * data['weight'] 
    for name, data in available_items.items()
])
s.add(total_weight <= 64)

第四步：求解与解读

模型建立完毕后，我们就可以让 Z3 开始工作了。调用 s.check() 会告诉我们是否存在一个满足所有约束的解。如果存在（sat），s.model() 将返回一个具体的赋值方案。

# 检查是否存在解决方案
if s.check() == sat:
    # 获取一个可行的模型
    m = s.model()
    print("找到一个可行的捆绑包填充方案：")
    for item_name, var in item_vars.items():
        quantity = m.evaluate(var).as_long()
        if quantity > 0:
            print(f"- {item_name}: {quantity} 个")
else:
    print("在当前约束下，找不到任何填充方案。")

这个基础模型只会给出一个“可行”解，而非“最优”解。但在许多场景下，这已经足够。例如，只想知道能否把一组特定物品塞进去。

结语：从建模到优化

我们成功地将一个具体、带有独特规则的游戏机制，抽象成了一个形式化的整数约束模型。这个过程的核心在于：识别核心规则、选择合适的数学抽象（整数权重）、并用求解器的语言逐条定义边界。

通过将捆绑包问题转化为 Z3 模型，我们不仅能验证一个物品组合是否可行，更可以进一步扩展模型以追求“最优”方案。例如，我们可以要求 Z3 在满足所有约束的前提下，最大化放入捆绑包的物品总数，或者最大化物品的种类数。这只需要在模型中加入 solver.maximize() 或 solver.minimize() 目标函数即可。

这种从特定领域问题到通用约束模型的翻译能力，是解决现实世界中复杂的调度、规划和资源分配问题的基础。下一次当你在《我的世界》里整理行囊时，不妨想一想背后那有趣的数学模型。