z3 - 如何建模能力奖励，以便可以使用 Z3 动态添加/删除选项

Question

我想使用 Z3 来模拟游戏中的角色统计数据。为简单起见，我们将专注于一项统计数据：护甲等级 (AC)。

在这个游戏中，角色可以穿戴多种类型的盔甲，每种盔甲都有不同的基础盔甲等级。此外，还有许多其他奖励可以添加到盔甲上。为简单起见，让我们考虑以下内容

Armor Type | Base armor class
-----------|-----------------
Chain Mail | 16
Plate Mail | 18

Shield Type  | Armor Bonus
------------------------
Kite Shield  | +2
Magic Shield | +4

Defense Training | Bonus
-------------------------
Without          | +0
With             | +1

角色只能从每种奖励中受益，例如，角色一次只能装备一个盾牌。

角色必须拥有盾牌才能装备它，因此他们可以装备的盾牌组可能会动态变化。

此外，角色可能会在游戏期间的某个时间点（例如升级时）获得防御训练，因此奖励类型的集合也可能会动态变化。

玩家通常希望他们的角色可以获得最高的 AC，因此角色 AC 是他们可以获得的最佳基础 AC，加上他们可以访问的所有类别中每个类别的最佳奖励。

在命令式/OO 编程语言中，我可以像这样对系统建模

class Character():
    base_armor_bonuses = [16, 18]
    shield_armor_bonuses = [2, 4]
    armor_class_bonuses: List[List[Int]] = [base_armor_bonuses, shield_armor_bonuses]

    def armor_class(armor_class_bonus_options):
        sum([max(bonus_kind) for bonus_kind in armor_class bonuses])

    def add_bonus_kind(new_bonus_options):
        armor_class_bonuses.append(new_bonus_options)

    def add_new_armor_type(new_armor_bonus):
        base_armor_bonuses.append(new_armor_bonus)

命令式方法可以很好地编码这些简单的规则，但是我对快速迭代规则更改和新效果很感兴趣，所以我希望 Z3 能够以更灵活的方式编码这些规则。

另外我想用 Z3 来探索一下设计空间，例如找到最大化装甲等级的角色构建，这是命令式方法很难做到的。

编辑：

我希望能够使用系统实时回答诸如“这个角色当前的盔甲等级是什么？”之类的问题。然后响应游戏中发生的事件，例如角色获得新盾牌、走在墙后或脱下盔甲，更新世界状态，以便在我下次制作时更新他们的盔甲等级查询“这个角色的盔甲等级是什么？”。

我也希望能够回答，不一定是实时的。在您可以制作的所有可能角色中，哪个角色的护甲等级最高。这对于简化的示例很容易，但是一旦您引入了许多种类的角色，所有可能的角色都可以从各种不同的选项中获得不同种类的装甲等级奖励，那么枚举所有可能的角色以找到具有最高装甲等级的角色变得不可行从中选择。

对于替代方案，我对 prolog 进行了一些研究，它也可能能够回答查询，尽管我不确定性能差异可能是什么。我还考虑了一个典型的命令式程序，例如下面包含的 python 片段。这将很好地处理实时查询。但是，它会产生与维护正确支持所有不同选项的命令式程序相关的开销。此外，很难甚至不可能从该程序中确定具有最大装甲等级的角色或其他角色。我希望像 z3 这样的声明性逻辑语言可以克服这两个限制。

目前，这是我和我的朋友在玩现有游戏（实时查询）和设计新游戏（非实时查询）时使用的一个爱好项目。

编辑 2

对于基本版本，没有自由变量，它本质上只是计算特定角色的装甲等级和其他统计数据。我想这样做的原因是因为我不想维护 2 个独立的系统，其中包含编码的游戏规则，一个用于游戏，一个用于设计。

对于更复杂的示例，自由变量是您在构建角色时所做的选择。这是一个简单的例子。

角色有一个基类 Fighter、Archer 或 Wizard。每次升级时，您都可以在任何一个职业中升级，获得您尚未拥有的最低职业等级的能力。例如，战士 2/弓箭手 1 将具有战士的一级和二级能力以及弓箭手的一级能力。以下是一些示例能力

level | fighter ability
----------------------
1     | Proficiency with Chain mail and the Kite Shield
2     | Defense Training or Proficiency with plate (players choice, i.e. a free variable)
3     | Defense Training or Proficiency with plate (whichever one they didn't get before)

level | wizard ability
-----------------------
1     | proficiency with Magic Shields
2     | proficiency with chain

所以我想以声明的方式定义每个角色可用的奖金/选项，然后问Z3什么构建在3级时具有最高的装甲等级。战士2（用于板）/巫师1是我能做到的最好的想出这个小例子，总护甲为 18 + 4 = 22。

现在，例如，如果有 12 个角色类别，并且每个类别的级别从 1 到 20，就像第 5 版 D&D 一样。将有 12^20 或大约 2^71 个可能的 20 级角色构建。通过列举所有选项来回答哪个 20 级角色具有最高护甲等级的问题可能需要比我还活着更长的时间。这就是我希望 Z3 能够提供帮助的地方。

编辑 3

我不确定我应该使用什么数据结构/类型来表示特定角色可用的盔甲。我考虑过使用数组，但是当我定义战斗机类选项时，我不知道如何表达“装甲类型数组包含板”之类的语句，然后还表示数组中没有其他未指定的元素。

换句话说，我不知道如何定义数组的内容，使其依赖于自由变量的分配（字符类级别的选择），然后说数组中没有其他内容。

此外，我对 Z3 还不够熟悉，甚至不知道这是否是系统建模的好方法。

标签： z3