問題タブ [sat]

Choco 4.0.1 を使用して SAT 数式をモデル化しようとしています。docsを読み、javadocから理解しようとしていますが、残念ながらこれまでのところ失敗しています。この種の問題とチョコに取り組むのはこれが初めてです。だから、私は非常に明白なことを尋ねているかもしれません。

モデルにいくつかの制約を追加する必要があります (各 var は BoolVar です):

モデルで ifOnlyIf メソッドを使おうとしていますが、変数を否定する方法や and を使用する方法がわかりません。誰かが（理想的には）サンプルコードや、これらのタイプの制約をモデル化する方法に関するアイデアを提供してもらえますか?

私は SAT で問題をモデル化し、cryptominisatで解決しようとしています。変数に制約がない場合は、変数にデフォルト値を設定したいと思います。

私はマニュアルをset_default_polarity調べましたが、答えのようです。試してみましたが、思ったように動作しません。ここの用語がよくわかりませんpolarity。私は論理に慣れていないので、いくつかのグーグルは私を助けませんでした。

だから、私の質問は次のとおりです。

1. polarity入門レベルの情報源を教えてください。

2. 論理変数のデフォルト値を設定するために cryptominisat (または一般的に SAT ソルバー) にインターフェイスはありますか? そのような機能の用語は何ですか?

ありがとう。

関連：CNFの単純化（実際、その質問の送信者は、私がここで欲しいものを求めていたのではないかと思います）

DIMACS 形式の CNF 式を単純化 (または解決する前に「前処理」) するためのツールが多数あり、ほとんどの SAT ソルバーにはいくつかのツールが組み込まれています。しかし、私が知っていることはすべて、自明に充足可能な式をゼロまたは 1 つの変数を持つ自明に充足可能な CNF に単純化することです。つまり、式の充足可能性を維持しようとするだけです。少なくとも、SatELite と cryptominisat の前処理モードを試しました。

ただし、大規模な問題の CNF を構築する場合、問題の明確に定義されたサブセットを一度に単純化することは非常に有用であるように思われます。これらの部分式のいくつかの変数間の制約。

それで、ツールは存在しますか、それとも通常のSATソルバー（または最小化したいCNFを生成するために使用しているZ3のような他のソルバー）を何らかの方法で巧妙に使用して、すべてのソリューションを維持しながらCNF式を単純化できますか与えられた変数のセットについて？