对于我正在开始的项目,我将需要使用SAT求解器.我之前使用过其中一些但主要用于实验,而这里项目的主要约束是良好的性能.我正在尝试寻找替代方案,并尝试了解每种方案如何根据我的具体要求定位.特别是:
我需要提取令人满意的任务,不仅要检查是否满足,而且解算器应该允许我重复求解相同的公式,寻找不同的可能令人满意的任务,最终以有效的方式迭代所有这些,(例如,没有我)必须添加一个条款并重新开始).
该项目应该仍然是积极维护和相当的生产质量,而不是自出版以来放弃的一些竞争获胜的研究项目(见picosat).
此外,由于我使用的是C++,解算器应该提供一个高效且(可能)良好的编写C++接口.
我考虑的第一个候选人是Z3,但我对文档感到困惑,如果上面的第1点得到支持则无法理解,如果我只需要SAT而不是SMT就可能有点过分.C++界面似乎也很容易使用,但我无法忍受这样一个事实:我必须使用普通字符串命名变量(这与我周围的算法配对非常糟糕.这是不是可以避免？).
那么你能否给我一些关于哪个SAT求解器使用的建议,或者对Z3的怀疑有所启发？
如何使用z3计算解决方案的数量？例如,我想证明,对于任何一个n,方程组有2个解{x^2 == 1, y_1 == 1, ..., y_n == 1}.以下代码显示给定的可满足性n,这不是我想要的(我想要任意数量的解决方案n).
#!/usr/bin/env python
from z3 import *
# Add the equations { x_1^2 == 1, x_2 == 1, ... x_n == 1 } to s and return it.
def add_constraints(s, n):
assert n > 1
X = IntVector('x', n)
s.add(X[0]*X[0] == 1)
for i in xrange(1, n):
s.add(X[i] == 1)
return s
s = Solver()
add_constraints(s, 3)
s.check()
s.model()
Z3中是否有办法证明/显示给定模型是唯一的，并且不存在其他解决方案？
一个小例子来演示
(declare-const a1 Int)
(declare-const a2 Int)
(declare-const a3 Int)
(declare-const b1 Int)
(declare-const b2 Int)
(declare-const b3 Int)
(declare-const c1 Int)
(declare-const c2 Int)
(declare-const c3 Int)
(declare-const ra Int)
(declare-const rb Int)
(declare-const rc Int)
(declare-const r1 Int)
(declare-const r2 Int)
(declare-const r3 Int)
(assert (>= a1 0))
(assert (>= a2 0))
(assert (>= a3 0))
(assert (>= b1 0))
(assert (>= b2 0))
(assert (>= b3 0))
(assert (>= c1 0))
(assert (>= c2 0))
(assert …我有一个非常简单的示例Z3程序，如下所示：
(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)
此示例程序可以在Z3在线编译器中执行，没有问题。但是当我想使用以下命令使用命令行提示符执行同一程序时：
Z3 <script path>
我收到错误消息：
ERROR: line 1 column 21: could not match expression to benchmark .
并对程序中的每一行重复此错误。谁能帮我看看我在做什么错？