Max-SMT 求解器如何工作？答案

【问题标题】：How Max-SMT solvers do work?Max-SMT 求解器如何工作？
【发布时间】：2012-05-15 13:55:33
【问题描述】：

SMT 求解器是为处理类似于 SAT 的可满足性而开发的。众所周知，SAT 也是可满足性的，并且提出了 SAT 的变体。其中之一是 max-SAT。所以我想问一下是否存在max-SMT求解器，如果存在，它是如何工作的？

【问题讨论】：

标签： formal-verification satisfiability

【解决方案1】：

用于使 max-SMT 工作的技术之一如下：

增加/制定输入以允许计算模型（分配）中评估为 True 的子句数量。将这个新公式称为 F，并让变量 K 保持计数。
对 F 执行二分搜索，以获取 K 的最佳（最大）可能值，方法是针对 K。

例如，在 F 上运行求解器以及子句 (K = 20)。

如果是 SAT，则将 K 的值加倍并使用 (K = 40) 运行求解器。
如果是 UNSAT，将 K 的值减半并使用 (K = 10) 运行求解器。

逐步迭代以接近 K 的最大可能值。

我知道 Yices 使用类似的东西（至少它曾经使用过），但是可能会添加其他一些优化/启发式方法。

其他求解器可能使用不同的技术。

【讨论】：

【解决方案2】：

据我所知，Yices 确实支持 max-SMT。他们的paper (Archived copy) 稍微描述了它的工作原理。

【讨论】：

链接已损坏

【解决方案3】：

我知道 3 个重要策略。所有这些都归结为解决一系列 SAT 问题。我根据必须满足的硬约束和加权软约束制定了我的答案，这些软约束总结起来就是 MAX-SAT 的目标。

线性搜索

对于给定的一组（正加权）子句，您有一个最低目标。最小目标为 0 意味着硬约束部分是可满足的，这是 MAX-SAT 解决方案存在的先决条件。

在一个步骤中，您尝试证明严格大于上一步目标的最小目标。假设我们有 3 个加权为 2、3、7 的软约束。您首先尝试证明（硬约束 + 权重为 2 的约束），如果您成功，您知道 MAX-SAT 目标的下限为 2。严格优于 2 的最小下限是 3。因此，您将尝试证明（硬约束 + 权重为 2 的约束）如果这也是 SAT 则 (hc + 2 + 3) 然后 (hc + 7) 然后 ( hc + 7 + 2) 然后 (hc + 7 + 3) 然后 (hc + 7 + 3 + 2)。

如果您在任何时候遇到 UNSAT，这意味着上一步是最大值。

二分查找

如果您考虑与体重相关的 SAT 问题，您可能会认为按顺序解决这些问题是一种浪费，因为在许多情况下，之前的作业没有用处。因此，您可以尝试一种称为二进制搜索的方法。这个想法是你在体重秤的中间选择一个问题，如果它是SAT你可以丢弃所有权重比它弱的问题，如果它是UNSAT你可以丢弃所有权重比它高的问题。使用它，您可以在 O(log(n)) 中找到最佳值，而不是预期的 O(n/2)，其中 n 是不同权重组合的数量。

但是，这种方法与线性搜索相比并不像您最初想象的那样有利。事实证明，UNSAT 实例往往比 SAT 实例更耗时。基于二进制搜索的 MAX-SAT 求解器在任何时候都有更糟糕的行为，即您不知道求解器何时会停止，并且它必须返回在此之前找到的最佳实例。任何时候的行为对于许多现实世界的应用程序都很重要。

核心驱动搜索

核心驱动搜索基本上是一种反向线性搜索，它会遇到很多 UNSAT 实例，但为了弥补这一点，它可以访问求解器的额外信息，这可能有助于它跳过许多中间问题。

核心驱动搜索可以访问冲突的核心。因此，如果求解器点击 UNSAT，它会得到一个子句来表达存在的矛盾。它现在可以使用该子句并使用它来排除一些加权软约束。通过检查给定该子句中哪些是不可满足的，它可以降低目标的上限，然后在该范围内再次尝试，直到达到 SAT。如果它知道（因为它采用了最大的可行目标）当前的上限就是目标。

总结

对于 MAX-SAT，通常将您的问题作为一系列 SAT 问题来解决。您可能还可以想到一些涉及这些的混合策略。然而，这个问题有一些不同的角度，将来可能会很有趣。

使用权重引导对所有目标值进行一次搜索的方法（如在混合整数线性规划中所做的那样）并不常见。这主要是因为 braniac MILP 方法无法在 SAT 中通常发现的规模的工业实例上运行，分配如何影响软约束并不总是很明显，并且由宽松解决方案提供的分支启发式方法是在两个值之间进行选择时用处不大（MAX-SAT 可以表述为 0-1 整数线性规划）。

Jakob Nordström 目前围绕求解器 RoundingSAT 做了一些有趣的工作，它使用一种称为伪布尔编程的形式，可以编码与 0-1 ILP 和 MAX-SAT 相同的问题。 PB 优化具有比 SAT 求解器使用的 CNF 更强的输入格式，是否可以用两项而不是指数项来编码鸽洞约束。然而，如果一个 PBO 求解器被赋予一个 CNF 作为输入，它就不能做任何更复杂的推理，最终成为一个 SAT 求解器，它认为每个冲突传播的时间更长。 SAT 以速度恶魔为主。

涉及更多技术细节的长篇演示文稿是SAT for Optimization by Fahiem Bacchus (University of Toronto)。

【讨论】：