2

我正在将我的问题转换为 SMT，并且我注意到 SMT 求解器（MathSat5 和 CVC4）在求解 sat 实例时速度很慢。我的暂停是我的翻译中有一些东西让它变慢了。

我附上了一个示例 cnf 实例和 smt2 翻译以供参考，下面我提供了较大实例的求解器时间（不包括翻译时间）以比较 MathSat5、CVC4 和 MiniSat。

Solver                Solver Time (s)
-------------------------------------
MiniSat               0.028062 s
MathSat5              2.629702 s
CVC4                  7.488870 s
CVC4(QF_SAT)          1.253978 s

那么有没有人知道为什么这些时代截然不同？PS。cvc4 说它花费了 5.862 秒：theory uf Symmetry_breaker

Sample cnf:
-------------------------------------
p cnf 20  91 
4 -18 19 0
...
4 -16 -5 0


Sample smt2:
-------------------------------------
(set-logic QF_UF)
(set-info :smt-lib-version 2.0)
(set-option :produce-models true)

(declare-fun v1 () Bool)
...
(declare-fun x20 () Bool)

(assert (or v4 (not x18) x19))
...
(assert (or v4 (not v16) (not v5)))
(check-sat)
(get-value ( v1 ... x20))
(exit)

谢谢

4

1 回答 1

3

由于理论求解器，SMT 求解器有额外的开销。在 CVC4 中，您可以使用以下命令来避免这种情况：

（设置逻辑 QF_UF）
（设置信息：cvc4-逻辑 QF_SAT）

代替

（设置逻辑 QF_UF）

请注意，这是 CVC4 扩展，不是 SMT-LIB 标准的一部分。但是，如果您真的只使用布尔推理，这应该会给您带来有竞争力的表现。

于 2014-12-04T18:48:47.340 回答