2

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

考虑方程

  • a < 10和a > 5
  • b < 5和b > 0
  • b < c < a
  • ,和整数a_bc

存在满足方程 when和的最大模型数的值a和where 。ba=9b=1

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

4

2 回答 2

3

我认为您通常无法做到这一点。也就是说，当您可以对任意理论进行任意约束时。您在问一个“元”问题：“最大化模型数量”不是关于问题本身的问题，而是关于问题模型的问题；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 求解可以神奇地自动化该部分。（除非帕特里克想出一个聪明的编码，否则他很聪明！）

于 2019-01-08T06:33:52.283 回答
2

让我们分解你的目标：

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

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

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

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

一般的想法可能是使用一些SMT Solver API并按如下方式进行：

  • assert整个公式
  • 重复直到完成值的组合：
    • push回溯点
    • assert一种特定的值组合，例如a = 8 and b = 2
    • 永远重复：
      • check寻求解决方案
      • if UNSAT, 退出最内层循环
      • 如果, 为给定的和SAT值组合增加模型的计数器ab
      • 取任何其他变量的模型值，例如c = 5 and d = 6
      • assert要求至少一个“其他”变量更改其值的新约束，例如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 的解决方案的数量。

于 2019-01-08T12:19:55.520 回答