algorithm - 是否可以通过 SMT 求解器找到 bool 公式的最优解？

Question

我有一个很大的 bool 公式要解决，由于密文的原因，我必须在这里粘贴一张图片:

此外，我已经有一个函数 area测量 4 个整数的维度:area(c,d,e,f)=|c−d|×|e−f|

我想做的不仅仅是弄清楚公式是否可满足:我正在寻找一个最佳的 6 元组 (a,b,c,d,e,f)这使得大公式TRUE和 area(c,d,e,f)大于或等于任何其他也满足该公式的 6 元组的维数。

换句话说，找到Max(area(c,d,e,f))服从大公式。

我想知道 SMT 求解器是否可以帮助解决这个问题。我了解到 Z3支持quantifiers ，并且能够判断一个 bool 表达式是否可满足。但问题是如果 Z3可以帮助找到函数 area 的最优解.

有人知道吗？任何关于 SMT 求解器、Z3 或其他算法的评论将不胜感激...

Answer 1

简而言之，是的。

因为您的公式由量词组成，所以我认为 Microsoft Solver Foundation 不是合适的选择。正如您所说，Z3 支持量词、整数理论并用于检查可满足性。尽管 Z3 不直接支持优化，但您可以使用通用量词轻松编码优化问题:

sat(a, b, c, d, e, f) => (forall a1, b1, c1, d1, e1, f1. sat(a1, b1, c1, d1, e1, f1) && goal(a, b, c, d, e, f) >= goal(a1, b1, c1, d1, e1, f1))

其中:sat 是用于检查可满足性的 bool 表达式，goal 是 area 函数，您的优化目标。

如您所见，该公式是根据您在问题中的要求逐字翻译的。 (a, b, c, d, e, f) 的分配是您需要找到的最佳解决方案。

顺便说一句，Z3 有一个 Linux 发行版并提供 OCaml API，这完全符合您的偏好。