2

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

4

3 回答 3

1

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

  • 增加/制定输入以允许计算模型（分配）中评估为 True 的子句数量。调用这个新公式F，并让变量K保持计数。

  • 通过重复调用求解器以获得 K 的不同固定值，对F执行二进制搜索以获得K的最佳（最大）可能值。

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

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

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

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

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

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

于 2014-04-09T22:48:27.080 回答
0

据我所知，Yices确实支持 max-SMT。他们的论文（存档副本）描述了它的工作原理。

于 2013-10-22T23:34:45.187 回答
0

我知道 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由速度恶魔主导。

Fahiem Bacchus（多伦多大学）的 SAT for Optimization是一个关于更多技术细节的较长形式的演示文稿。

于 2021-03-18T23:29:38.030 回答