使用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是否支持以下内容:对于a和b的每个值，计数满足公式的模型数量，并给出最大计数的a和b的值。

Answer 1

让我们来分解一下你的目标：

• 您希望枚举可以分配a和b (...and更多)的所有可能方式。
• 对于每一个组合，您都希望计算可满足的模型数。

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

即使可以安全地假设每个其他变量的域包含有限的元素，它仍然是高度低效的。例如，如果问题中只有布尔变量，那么在搜索过程中仍然会有一个指数级的值组合--以及候选模型--来考虑。

但是，您的实际应用程序在实践中也可能没有那么复杂，因此它可以由SMT解决程序处理。

总的想法可以是使用一些SMT解决程序API，并按照以下步骤进行：

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

​

- `pop` backtrack point

​

或者，您可以在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解决方案有疑问，我建议您开始使用https://github.com/pysmt/pysmt解决您的任务，这允许您轻松地在几个SMT引擎中进行选择。

如果对于您的应用程序来说，明确列举模型的速度太慢，不太实用，那么我建议您查看大量关于CSPs的计数解决方案的文献，在这些文献中，这个问题已经得到解决，并且似乎有几种方法可以粗略估计CSP的解决方案的数量。

Answer 2

我不认为你一般能做到这一点，也就是说，当你对任意的理论有武断的约束时。您要问的是"meta"-question：“最大化模型数量”不是关于问题本身的问题，而是关于问题模型的问题；一些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解决方案。(除非Patrick想出了一个聪明的编码方法，否则他是相当聪明的！)