用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说它花了5.862秒在理论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)

谢谢

Answer 1

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

(集合逻辑QF_UF)

(set-info :cvc4 4-逻辑QF_SAT)

而不是

(集合逻辑QF_UF)

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