z3 - smt/z3 可以用于优化吗

Question

SMT求解器能否有效地找到伪布尔问题的解（或赋值），如下所述：

\sum {i..m} f_i x1 x2.. xn *w_i

其中f_i x1 x2 .. xn是一个布尔函数，w_i是一个 Int 类型的权重。

为方便起见，我突出显示第 1 页和第 3 页中的内容，这足以说明伪布尔问题。

Answer 1

SMT 求解器通常会解决以下问题：给定一个逻辑公式，可选择使用来自基础理论（例如算术理论、位向量理论、数组）的函数和谓词，该公式是否可满足。它们通常不会为您提供指定目标函数的方法，并且通常没有内置的优化程序。

一些特殊情况是仅使用布尔值或布尔值与位向量或整数的组合的公式。伪布尔约束可以用整数表示，也可以使用位向量进行编码（注意考虑溢出语义），或者可以直接将它们编码到 SAT 中。对于使用属于伪布尔问题类的有界整数的某些公式，Z3 将尝试自动缩减为位向量。这仅适用于标记为 QF_LIA 的 SMT-LIB2 格式的 benchmkars，或者如果您明确调用执行此缩减的策略（应该应用“qflia”策略），则适用。

虽然 Z3 没有直接公开目标函数，但研究界正在积极寻求用目标函数增强 SMT 求解器的问题。Nieuwenhuis 和 Oliveras 在 SAT 2006 中提出的一种方法是将“加权最大 SMT”问题作为一种自定义理论来解决。Yices 带有用于加权最大 SMT 的内置功能，Z3 没有，但可以编写自定义理论来执行加权最大 SMT 求解器的回溯搜索，但没有开箱即用的功能。

有时人们会尝试使用量化公式来指定目标函数。理论上，人们可以希望量词消除程序可以解决该目标。在性能方面，这通常非常糟糕。量词消除是一种过度拟合，（我们拥有的）例程将不会有效。

Answer 2

对于您的问题，如果您想从总和中找到优化的（最大或最小）结果，是的，Z3 具有此能力。您可以使用 Z3 库的Optimize类而不是 Solver 类。该类分别提供了“最大化”和“最小化”两种方法。您可以传递需要优化的 SMT 变量，优化类模型将为您提供解决方案。它实际上使用Microsoft.Z3库与 C# API 一起工作。为了给您带来不便，我附上一个片段：

Optimize opt; // initializing object
opt.MkMaximize(*your variable*);
opt.MkMinimize(*your variable*);
opt.Assert(*anything you need to do*);