使用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和[=的值16=] 最大化计数。

Answer 1

我认为一般情况下您无法做到这一点；也就是说，当您可以对任意理论进行任意约束时。你在问一个 "meta" 问题："Maximize the number of models" 不是关于问题本身的问题，而是关于问题模型的问题； SMTLib 无法处理的东西。

话虽如此，但我认为应该可以针对特定问题对其进行编码。在你给出的例子中，模型space在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 求解神奇地自动化。（除非 Patrick 想出一个聪明的编码，否则他在这方面相当聪明！）

Answer 2

让我们分解一下您的目标：

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

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

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

但是，也有可能您的实际应用在实践中并不那么复杂，因此可以由 SMT 求解器.

处理

总体思路可能是使用一些 SMT 求解器 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 求解器，我建议您开始使用 pysmt 来解决您的任务，这样您就可以轻松选择多个 SMT 引擎。

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

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

Using SMT-LIB to count the number of modules using a formula

python

z3

smt

z3py

pysmt