ユニット伝播

単位伝播( UP ) またはブール制約伝播( BCP ) または1 リテラル規則( OLR ) は、一連の (通常は命題の)節を簡略化できる自動定理証明の手順です。

この手順は、単位節、つまり、連言標準形の単一のリテラルで構成される節に基づいています。各節が満たされる必要があるため、このリテラルは必ず真であることがわかります。節のセットに単位節が含まれている場合、他の節は次の 2 つの規則を適用することで簡略化されます。 ${\displaystyle l}$

1. を含むすべての節（ユニット節自体を除く）が削除されます（ の場合、節は満たされます）。${\displaystyle l}$${\displaystyle l}$
2. このリテラルを含むすべての節で、このリテラルが削除されます (満たされることに貢献することはできません)。${\displaystyle \neg l}$${\displaystyle \neg l}$

これら 2 つの規則を適用すると、古い規則と同等の新しい条項セットが作成されます。

たとえば、次の節のセットには単位節が含まれているため、単位伝播によって簡略化できます。 ${\displaystyle a}$

${\displaystyle \{a\vee b,\neg a\vee c,\neg c\vee d,a\}}$

にはリテラル が含まれているため、この節は完全に削除できます。 にはunit 節のリテラルの否定が含まれているため、このリテラルは節から削除できます。 unit 節は削除されません。削除すると、結果のセットが元のセットと同等ではなくなります。この節は、すでに他の形式で保存されている場合は削除できます (「部分モデルの使用」セクションを参照)。 unit 伝播の効果は、次のようにまとめることができます。 ${\displaystyle a\vee b}$${\displaystyle a}$${\displaystyle \neg a\vee c}$${\displaystyle a}$

結果として得られる節のセットは、上記のものと同等です。単位伝播の結果として得られる新しい単位節は、単位伝播のさらなる適用に使用でき、次のように変換されます。 ${\displaystyle \{c,\neg c\vee d,a\}}$${\displaystyle c}$${\displaystyle \neg c\vee d}$${\displaystyle d}$

単位伝播の 2 番目の規則は、解決の制限された形式と見なすことができます。この規則では、2 つの解決のうちの 1 つは常に単位節でなければなりません。解決に関しては、単位伝播は、古い節によって含意されなかった新しい節を生成することはないという点で、正しい推論規則です。単位伝播と解決の違いは次のとおりです。

1. 解決は完全な反駁手順ですが、単位伝播はそうではありません。言い換えれば、一連の節が矛盾している場合でも、単位伝播によって矛盾が生成されない可能性があります。
2. 解決される 2 つの節は、生成された節がセットに追加された後は一般に削除できません。逆に、単位伝播に含まれる非単位節は、その簡略化がセットに追加されたときに削除できます。
3. 解像度には、一般に単位伝播で使用される最初のルールは含まれません。

包含を含む解決計算では、ルール 1 を包含によってモデル化し、ルール 2 を単位解決ステップとそれに続く包含によってモデル化できます。

新しい単位節が生成されるたびに繰り返し適用される単位伝播は、命題ホーン節の集合に対する完全な充足可能性アルゴリズムです。充足可能な場合は集合の最小モデルも生成します。ホーン充足可能性を参照してください。

節のセット内に存在するか、またはそこから派生できる単位節は、部分モデルの形式で保存できます (この部分モデルには、アプリケーションに応じて他のリテラルも含まれる場合があります)。この場合、単位の伝播は部分モデルのリテラルに基づいて実行され、単位節のリテラルがモデル内にある場合は削除されます。上記の例では、単位節が部分モデルに追加されます。節のセットの簡略化は、単位節がセットから削除されるという違いを除いて、上記と同じように進行します。結果の節のセットは、部分モデルのリテラルの有効性を前提とした元のセットと同等です。 ${\displaystyle a}$${\displaystyle a}$

単位伝播を直接実装すると、チェックするセットの合計サイズの2 乗の時間がかかります。これは、すべての節のサイズの合計として定義され、各節のサイズは、そこに含まれるリテラルの数です。

ただし、各変数について、各リテラルが含まれる節のリストを保存することで、単位伝播を線形時間で実行できます。たとえば、上記のセットは、次のように各節に番号を付けることで表すことができます。

${\displaystyle \{1:a\vee b,2:\neg a\vee c,3:\neg c\vee d,4:a\}}$

そして、各変数について、その変数またはその否定を含む節のリストを格納します。

${\displaystyle a:1\ 2\ 4}$

${\displaystyle b:1}$

${\displaystyle c:2\ 3}$

${\displaystyle d:3}$

この単純なデータ構造は、セットのサイズに比例した時間で構築でき、変数を含むすべての節を非常に簡単に見つけることができます。リテラルの単位伝播は、リテラルの変数を含む節のリストのみをスキャンすることで効率的に実行できます。より正確には、すべての単位節の単位伝播を実行するための合計実行時間は、節のセットのサイズに比例します。

• ホーンの満足度
• ホーン条項
• 自動定理証明
• DPLLアルゴリズム

• ダウリング、ウィリアム F.;ガリエ、ジャン H. (1984)、「ホーン命題式の充足可能性をテストするための線形時間アルゴリズム」、ロジックプログラミングジャーナル、1 (3): 267–284、doi : 10.1016/0743-1066(84)90014-1、MR  0770156。
• H. Zhang および M. Stickel (1996)。ユニット伝播のための効率的なアルゴリズム。人工知能と数学に関する第 4 回国際シンポジウムの議事録。