2

SMT ソルバーは、SAT と同様に充足可能性を考慮して開発されています。私たちが知っているように、SATは充足可能性のためでもあり、SATの変形が提案されています。それらの 1 つが max-SAT です。そこで、max-SMT ソルバーが存在するかどうか、存在する場合はどのように機能するのかをお尋ねしたいと思います。

4

3 に答える 3

1

max-SMT を機能させるために使用される手法の 1 つを次に示します。

  • モデル (割り当て) で True と評価される句の数をカウントできるように、入力を拡張/定式化します。この新しい数式をFと呼び、変数Kにカウントを保持させます。

  • Kの異なる固定値に対してソルバーを繰り返し呼び出して、Kの最適 (最大) 可能な値を求めてFで二分探索を実行します。

たとえば、節(K = 20)と共にFでソルバーを実行します。

  • SAT の場合、Kの値を 2 倍にして(K = 40)でソルバーを実行します。

  • UNSAT の場合、Kの値を半分にして(K = 10)でソルバーを実行します。

Kの可能な最大値に近づくように徐々に繰り返します。

Yices がこのようなものを使用していることは知っていますが (少なくとも以前はそうでした)、他にもいくつかの最適化/ヒューリスティックが追加されている可能性があります。

他のソルバーが異なる手法を使用する可能性があります。

于 2014-04-09T22:48:27.080 に答える
0

私の知る限り、Yicesは max-SMT をサポートしています。彼らの論文( Archived copy ) は、それがどのように機能するかについて少し説明しています。

于 2013-10-22T23:34:45.187 に答える