2

次の問題があります。

論理的に同等にならなければならない 2 つの命題式があります。そのうちの 1 つだけが「変数」を含みます。これは、変数を任意の命題式に置き換えることができるという意味です。ここでの問題は、論理的等価性が真になるように、変数の実際の置換を見つける必要があることです。例：

(a ^ ~b) または x = a

ここで、x は変数を表します。この論理的等価性は、x を a ^ b に置き換えることによって真にすることができるため、次のようになります。

(a ^ ~b) または (a ^ b) = a

これが問題です。入力として「1つの変数xを持つ方程式」を取得し、方程式が論理的に等価になるように変数xの出力値として与えるアルゴリズムが必要です。

変数は常に 1 つです。（実際、複数の変数で問題が発生する可能性がありますが、最初に単純なケースを解決したいと考えています）。問題の数式は、任意の形式を持つことができます (それらは CNF または DNF ではありません)。また、数式は実際には FALSE または TRUE になる可能性があり、解がない場合 (たとえば、"a または x = false" の場合、解がない場合) または複数の解 (たとえば、"a and x = false の場合) があります。 " 誤った命題は有効な答えになります)。

私が持っているのは、式が充足可能かどうかを教えてくれるタブロー推論器だけです。だから私は解決策をテストすることができます。しかし、私の問題は、私に解決策を与えることです。

4

1 に答える 1

1

あなたが探しているのは、解釈されていない機能を処理できる推論エンジンだと思います。このようなエンジンは、機能を含む問題を処理できます。

（a ^〜b）またはf（a、b）= a

通常、モデルを作成できます。つまり、実際には、初期式を満たす関数f（...）を生成します。適切な推論エンジンの一例は、いわゆるSMTソルバーです（SMT-LIBを参照）。人気のあるソルバーはMicrosoftのZ3です（Z3を参照）。

この例は、SMT-LIB形式で次のように記述できます。

(set-option :produce-models true)
(declare-const a Bool)
(declare-const b Bool)
(declare-fun f (Bool Bool) Bool)

(assert (= (or (xor a (not b)) (f a b)) a))
(check-sat)
(get-model)
(exit)

そしてZ3はモデルを生成します

(define-fun f ((x!1 Bool) (x!2 Bool)) Bool 
  (ite (and (= x!1 false) (= x!2 true)) false false))

これは元の問題を満たします。一般に、ソリューションは問題を満足させるだけです。完全なソリューションを取得するには、数量詞を使用できます。すべてのSMTソルバーがそれらをサポートしているわけではありませんが、たとえばZ3は、有限領域（ブール値など）の数量詞に完全な推論エンジンを使用し、そのような式のモデルを生成できます。

于 2011-10-12T21:41:46.670 に答える