2

問題を SMT に変換していますが、sat インスタンスを解くときに SMT ソルバー (MathSat5 および CVC4) が遅いことに気付きました。私の中断は、私の翻訳に何かがあり、翻訳が遅くなっているためです。

サンプルの 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)

ありがとう

4

1 に答える 1

3

理論ソルバーのため、SMT ソルバーには余分なオーバーヘッドがあります。CVC4 では、次のコマンドを使用してこれを回避できます。

(セットロジック QF_UF)
(セット情報:cvc4-ロジック QF_SAT)

それ以外の

(セットロジック QF_UF)

これは CVC4 拡張機能であり、SMT-LIB 標準の一部ではないことに注意してください。しかし、真にブール推論のみを使用している場合、これにより競争力のあるパフォーマンスが得られるはずです。

于 2014-12-04T18:48:47.340 に答える