0

2 つの数値 (バイナリ) を取り、それらが 16 に等しい場合に true を返すブール関数があるとします。

01000 + 01000 = 10000
  8   +   8   =  16    -> true


00110 + 01000 = 01110
  6   +   8   =  14    -> false

この例では、関数は 10 個の入力を受け取ります。それらを abcde + fghij と呼びましょう。

内部的には、ゲート ロジックで直接モデル化されており、2 つの加算器といくつかの xnor ゲートを使用してバイナリ文字列 10000 との等価性をチェックします。

次に、この 2 項関数をブール充足可能性アルゴリズムに入力して、真の出力を生成する一連の入力を見つけます (たとえば、上記の最初の例)。

私の質問は次のとおりです: 観察された制約について明示した場合、SAT アルゴリズムはより迅速に解決策を見つけるでしょうか?

「観察された制約」とはどういう意味ですか? まあ、観測された制約の 1 つは、「いずれかの数が 16 より大きい場合は、足し算を実行せずに false を返す」というものかもしれません。

この制約を次のように含めることができます。

(a ^ ¬b ^ ¬c ^ ¬d ^ ¬e) ^ (f ^ ¬g ^ ¬h ^ ¬i ^ ¬j) ^ (以前の機能)

別の制約として、「1 つの数値が偶数で、もう 1 つの数値が奇数の場合は false を返す」というものがあります。

((e ^ ¬j) v (¬e ^ j)) ^ (以前の関数)

これらのブール関数は正確さにおいて同等ですが、ゲート ロジックでは後者の方が (おそらく) 効率的です。問題をモデル化することが SAT に還元する際の唯一の懸念事項ですか、それともこれらの観察された制約を含めることは役立ちますか?

これは良い例ではないことは承知していますが、うまくいけば、私が求めていることを説明できます。

前もって感謝します

4

1 に答える 1

1

サンプル関数は、2^10 = 1,024 の可能な入力の組み合わせのうち 17 で true になります。

これは、次のようなマルチレベル論理回路として実装できます。 ここに画像の説明を入力

SAT ソルバーの主な領域は、すべての入力の組み合わせを列挙することが現実的でない問題です。10 入力はかなり控えめなサイズです。SAT ソルバーは通常、数百、数千、さらには数百万の入力変数に対処する必要があります。PC で数 100.000 の入力の組み合わせ (~ 20 の入力) を評価するのは非常に簡単です。しかし、数十億の組み合わせを超えると、不可能ではないにしても非現実的になります。

通常の方法では、最初に連言正規形(CNF)で問題をエンコードし、次に SAT ソルバーに 1 つの解を見つけさせるか、問題が満足できないことを見つけさせます。ほとんどの SAT ソルバーがすべての解を見つけることはまれです。

問題にブール式がある場合は、まずこの式を CNF またはソルバーが処理できる形式に変換する必要があります。適切なツールにはbc2cnfが含まれます。Z3のようなより一般的なソルバーは、SMT 2.0および CNF (別名DIMACS )以外の他の形式をサポートします。

真理値表を列挙したり、Cryptominisat 2のような SAT ソルバーを使用したりする以外に、制約駆動型ソルバーを使用できます。Google に尋ねるその他の用語には、「回答セット プログラミング」が含まれます。

于 2013-05-26T22:02:11.923 に答える