5

今日は、Haskell での SAT 解決のオプションについても調べてみました。まず、ピコサット ソルバーへの独自のインターフェイスを作成することに取り組みました。

すると、 SBV ライブラリがあることがわかりました。Z3、Yices、CVC4、および Boolector へのインターフェイスです。

また、github で Google 検索を行ったところ、Picosatバインディングも利用できることがわかりました。

高速/高パフォーマンスの制約を考慮して、検討する価値のある SAT ソルバーへの haskell バインディングは他にありますか? Carification: 高パフォーマンスの SAT 解法に適しています (たとえば、数日間実行される問題や、2^20 以上の SAT 問題をチェックするので、できるだけ早く終了する必要がある問題など)。たとえば、ハックで特に欠けているのは、Plingeling のような高速な並列 SAT ソルバーへのバインドです。(また、github で現在更新されている picosat バインディングを偶然見つけたので、他のオプションを見逃す可能性が非常に高いです)

SBV ライブラリのデフォルト オプションは、Z3 SMT ソルバーです。picosat は Z3 よりも単純な SAT 解法で高速であるという私の知識に基づいた推測は正しいですか?

4

2 に答える 2

6

開示、私はあなたが言及したHaskell picosatバインディングの作者です。

SBV はかなり前から存在する非常に堅牢なライブラリです。Yices や Z3 などの外部 SMT または SAT ソルバーへのインターフェイスが必要な場合に適しています。Picosat は、外部依存関係なしに簡単にインストールできるライブラリが欲しかったという理由だけで、私が作成したはるかに単純なライブラリです。

picosat は Z3 よりも単純な SAT 解法で高速であるという私の知識に基づいた推測は正しいですか?

パフォーマンスの制約が何であるかはわかりませんが、基礎となるソルバー ライブラリに関する限り、非常に大きな問題 (数十億の変数) に遭遇するまで、Z3 と Picosat の大きな違いに気付くことはありません。どちらも非常に最適化されたライブラリであり、(少なくとも Haskell 側からの) ボトルネックは、ライブラリと Haskell のランタイム間のデータのマーシャリングである可能性があります。

于 2014-01-04T23:48:21.657 に答える
5

SBV はスレッドセーフです。

Z3 と Lingeling の SAT パフォーマンスを比較するのは簡単なことではありません。内部ヒューリスティックを微調整するために正確なパラメーターを把握するために時間を割かない限り、それらは多かれ少なかれ同じであると推測する危険があります。

良いことに、SBV は共通のインターフェイスを提供するため、別のブリッジをインポートするだけでソルバーを変更できます。

import Data.SBV.Bridge.Z3

対

import Data.SBV.Bridge.Boolector

boolector をコンパイルして lingeling を使用すると、Haskell の 1 行を変更するだけで簡単にパフォーマンスをテストできます。

于 2014-01-05T03:44:02.803 に答える