1

いくつかの変数が特別にマークされている CNF 式があるとします。
SAT ソルバー (minisat など) に真に割り当てられた特殊変数の数を最大化するソリューションを見つける方法はありますか?

4

3 に答える 3

3

あなた (私) が望むものは、Partial Max Sat と呼ばれます。qmaxsat と呼ばれるソルバーがあり、十分に機能しているようです。

于 2013-01-31T22:45:47.190 に答える
0

これらすべてが特殊変数の表示を処理できるかどうかはわかりませんが、少なくともウィキペディアは検索の方向性を示しています。

最後の Max-SAT 評価に提出されたソルバーがいくつかあります。

  • Branch and Bound ベース: Clone、MaxSatz (Satz に基づく)、IncMaxSatz、IUT_MaxSatz、WBO。
  • 充足可能性ベース: SAT4J、QMaxSat。
  • 不満足ベース: msuncore、WPM1、PM2。

それらすべての説明を確認することは、管理できるはずです。

于 2013-02-07T12:44:51.663 に答える
0

minisat+ http://minisat.se/MiniSat+.htmlなどの PBC ソルバーを使用できます。 これらは、疑似ブール制約と呼ばれる追加の制約を使用して通常の CNF ファイルを解決します。Minisat+ はそのような制約の最適化もサポートしており、私の理解では、問題を解決します。

x1, .... xn を最大化したい変数とする o 真の割り当て 次に、制約を定義できます 最大化 +1 x1 ..... +1 xn minisat+ はそのような最適化問題を解決します

于 2014-02-26T12:48:03.310 に答える