SMT求解器是在处理类似于SAT的满足性时开发的。众所周知，SAT也是为了满足，并提出了SAT的变体。其中之一是最大SAT。所以我想问一下是否存在最大SMT求解器，如果存在，它是如何工作的？
用于使最大SMT工作的技术之一如下：
-
扩充/制定输入，以允许计算模型中计算结果为 True 的子句数(赋值(。将此新公式称为 F，并让变量 K 保存计数。
-
通过重复调用不同固定值 K 的求解器，对 F 执行二叉搜索以获取 K 的最佳(最大(可能值。
例如，在 F 上运行求解器以及子句 (K = 20(。
-
如果为 SAT，则将 K 的值加倍并使用 (K = 40( 运行求解器。
-
如果为 UNSAT，则将 K 的值减半，并使用 (K = 10( 运行求解器。
逐步迭代接近 K 的最大值。
我知道 Yices 使用这样的东西(至少以前是这样(，但是可能还添加了其他几个优化/启发式方法。
其他求解器可能会使用不同的技术。
据我所知，Yics确实支持max-SMT。他们的论文(存档副本(描述了它是如何工作的。
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(。如果您在任何时候遇到联合国卫星，这意味着上一步是最大值。
二叉搜索
如果您考虑与它们的权重相关的 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。