使用 SMT-LIB 使用公式计算模块数量

Question

我不确定这是否可以使用 SMT-LIB，如果不可能，是否存在可以做到这一点的替代求解器？

考虑方程式

• a < 10 和 a > 5
• b < 5 和 b > 0
• b < c < a
• 带有a、b 和c 整数

a 和 b 的值，其中存在满足 a=9 和 b=1 时的方程的最大模型数。

SMT-LIB 是否支持以下内容：对于 a 和 b 的每个值，计算满足公式的模型数量，并给出使计数最大化的 a 和 b 的值。

Answer 1

我认为一般情况下您无法做到这一点；也就是说，当您可以对任意理论进行任意约束时。您在问一个“元”问题：“最大化模型数量”不是关于问题本身的问题，而是关于问题模型的问题； SMTLib 无法处理的东西。

话虽如此，但我认为应该可以针对特定问题对其进行编码。在您给出的示例中，当a - b 最大时，模型空间最大化；所以你可以简单地写：

(set-option :produce-models true)

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)

(assert (< 5 a 10))
(assert (< 0 b  5))
(assert (< b c  a))

(maximize (- a b))
(check-sat)
(get-value (a b))

z3 的回应：

sat
((a 9)
 (b 1))

根据需要。或者，您可以使用 Python 绑定：

from z3 import *

a, b, c = Ints('a b c')
o = Optimize()
o.add(And(5 < a, a < 10, 0 < b, b < 5, b < c, c < a))
o.maximize(a - b)

if o.check() == sat:
    m = o.model()
    print "a = %s, b = %s" % (m[a], m[b])
else:
    print "unsatisfiable or unknown"

哪个打印：

a = 9, b = 1

还有针对 C/C++/Java/Scala/Haskell 等的绑定，可以让您在这些主机上或多或少地做同样的事情。

但是这里的关键点是我们必须手动提出最大化a - b 可以解决这里问题的目标。该步骤需要人工干预，因为它适用于您当前的任何问题。 （想象一下，您正在使用浮点理论或任意数据类型；想出这样的测量方法可能是不可能的。）我认为使用传统的 SMT 求解不能神奇地自动化该部分。 （除非帕特里克想出一个聪明的编码，否则他很聪明！）

Answer 2

让我们分解你的目标：

• 您想列举所有可以分配a 和b 的可能方式（...以及更多）
• 对于每个组合，您要计算可满足模型的数量

一般来说，这是不可能的，因为问题中某些变量的域可能包含无限数量的元素。

即使可以安全地假设每个其他变量的域都包含有限数量的元素，它仍然非常低效。 例如，如果您的问题中只有布尔变量，那么在搜索过程中您仍然需要考虑指数级的值组合——因此还有候选模型。

但是，您的实际应用也可能在实践中并不那么复杂，因此它可以由 SMT Solver 处理。

一般的想法可能是使用一些SMT Solver API并按照以下步骤进行：

• assert整个公式
• 重复直到完成值组合：
  • push回溯点
  • assert 一种特定的值组合，例如a = 8 and b = 2
  • 永远重复：
    • check 寻求解决方案
    • 如果UNSAT，退出最里面的循环
    • 如果SAT，为a和b的给定值组合增加模型计数器
    • 取任何其他变量的模型值，例如c = 5 and d = 6
    • assert 一个新的约束，要求至少有一个 "other" 变量更改其值，例如c != 5 or d != 6
  • pop回溯点

或者，您可以隐式而不是显式枚举a 和b 上的可能分配。思路如下：

• assert整个公式
• 永远重复：
  • check 寻求解决方案
  • 如果UNSAT，退出循环
  • 如果SAT，则从模型中获取控制变量的值的组合（例如a = 8 and b = 2），如果您之前遇到过这种组合，请检查内部映射，如果没有将计数器设置为1，否则将计数器增加1。
  • 取任何其他变量的模型值，例如c = 5 and d = 6
  • assert 请求新解决方案的新约束，例如a != 8 or b != 2 or c != 5 or d != 6

---

如果您对选择哪个SMT Solver 有疑问，我建议您使用pysmt 开始解决您的任务，它允许您在多个SMT 中进行选择引擎轻松。

---

如果对于您的应用程序而言，模型的显式枚举速度太慢而无法实用，那么我建议您查看关于CSP 的计数解决方案的大量文献，其中已经解决了这个问题并且似乎存在几种方法来近似估计 CSP 的解决方案的数量。