使用 SMT 求解器求解 dimacs 实例似乎很慢（SMT2 格式）

Question

我正在将我的问题转换为 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 说它在：theory uf Symmetry_breaker 中花费了 5.862 秒

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)

谢谢

Answer 1

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

（设置逻辑 QF_UF）
(set-info :cvc4-logic QF_SAT)

而不是

（设置逻辑 QF_UF）

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