smt/z3可以用来优化吗答案

【问题标题】：can smt/z3 be used for optimazationsmt/z3可以用来优化吗
【发布时间】：2012-11-18 04:22:19
【问题描述】：

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

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

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

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

【问题讨论】：

标签： z3

【解决方案1】：

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

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

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

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

【讨论】：

【解决方案2】：

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

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

【讨论】：