ホーンの満足度

形式論理学において、ホーン充足可能性( HORNSAT ) は、与えられた命題ホーン節の集合が充足可能かどうかを判断する問題です。ホーン充足可能性とホーン節は、アルフレッド・ホーンにちなんで名付けられました。

ホーン節は、節のヘッドと呼ばれる最大 1 つの正のリテラルと、節の本体を形成する任意の数の負のリテラルを持つ節です。ホーン式は、ホーン節の結合によって形成される命題式です。

ホーン充足可能性は、実際にはP完全問題という意味で多項式時間で計算可能であることが知られている「最も難しい」または「最も表現力豊かな」問題の1つです。^[1]

ホーンの充足可能性問題は、命題多値論理でも問われることがある。アルゴリズムは通常は線形ではないが、多項式のものもある。概要についてはHähnle (2001 または 2003)を参照のこと。^{[2] [3]}

ホーンの充足可能性の問題は線形時間で解くことができる。^[4] 量化されたホーンの公式の真偽を決定する問題も多項式時間で解くことができる。^[5] ホーンの充足可能性に対する多項式時間アルゴリズムは再帰的である。

• 最初の終了条件は、現在存在するすべての節に負のリテラルが含まれる式です。この場合、節内の現在のすべての変数を false に設定できます。
• 2 番目の終了条件は空の節です。この場合、式には解がありません。
• その他の場合、式には正の単位節が含まれているため、単位伝播を実行します。つまり、リテラルが true に設定され、 を含むすべての節が削除され、 を含むすべての節からこのリテラルが削除されます。結果は新しい Horn 式であるため、繰り返します。${\displaystyle l}$${\displaystyle l}$${\displaystyle l}$${\displaystyle \neg l}$

このアルゴリズムでは、満足できるホーン式の真理値割り当てを決定することもできます。単位節に含まれるすべての変数は、その単位節を満たす値に設定され、他のすべてのリテラルは false に設定されます。結果として得られる割り当ては、ホーン式の最小モデル、つまり、セット包含を使用して比較が行われる、true に割り当てられた変数の最小セットを持つ割り当てです。

単位伝播に線形アルゴリズムを使用すると、アルゴリズムは式のサイズに対して線形になります。

ホーン式では

(¬ a  ∨ ¬ b  ∨  c ) ∧

(¬ b  ∨ ¬ c  ∨  d ) ∧

(¬ f  ∨ ¬ a  ∨  b ) ∧

(¬ e  ∨ ¬ c  ∨  a ) ∧

(¬ e  ∨  f ) ∧

(¬ d  ∨  e ) ∧

(¬ b  ∨ ¬ c )、

各節には否定リテラルがあります。したがって、各変数を false に設定するとすべての節が満たされ、それが解決策となります。

ホーン式では

(¬ a  ∨ ¬ b  ∨  c ) ∧

(¬ b  ∨ ¬ c  ∨  f ) ∧

(¬ f  ∨  b ) ∧

(¬ e  ∨ ¬ c  ∨  a ) ∧

（f）∧

(¬ d  ∨  e ) ∧

(¬ b  ∨ ¬ c )、

1つの節はfが真であることを強制する。fを真に設定して簡略化すると、

(¬ a  ∨ ¬ b  ∨  c ) ∧

（イ）∧

(¬ e  ∨ ¬ c  ∨  a ) ∧

(¬ d  ∨  e ) ∧

(¬ b  ∨ ¬ c )。

ここでbは真である。簡略化すると

(¬ a  ∨  c ) ∧

(¬ e  ∨ ¬ c  ∨  a ) ∧

(¬ d  ∨  e ) ∧

（¬c） .

これは自明なケースなので、残りの変数はすべてfalseに設定できます。したがって、満足できる割り当ては次のようになります。

a  = 偽、

b  = 真、

c  = 偽、

d  = 偽、

e  = 偽、

f  = 真です。

ホーン式では

(¬ a  ∨ ¬ b  ∨  c ) ∧

(¬ b  ∨ ¬ c  ∨  f ) ∧

(¬ f  ∨  b ) ∧

(¬ e  ∨ ¬ c  ∨  a ) ∧

（f）∧

(¬ d  ∨  e ) ∧

(¬ b )、

1つの節はfが真であることを強制する。その後の簡略化により、

(¬ a  ∨ ¬ b  ∨  c ) ∧

（イ）∧

(¬ e  ∨ ¬ c  ∨  a ) ∧

(¬ d  ∨  e ) ∧

(¬ b )。

ここでbは真でなければならない。簡略化すると

(¬ a  ∨  c ) ∧

(¬ e  ∨ ¬ c  ∨  a ) ∧

(¬ d  ∨  e ) ∧

（）。

空の節が得られたので、式は満たされません。

ホーン論理式のクラスの一般化は、名前変更可能ホーン論理式であり、これはいくつかの変数をそれぞれの否定に置き換えることによってホーン形式にすることができる論理式の集合である。そのような置き換えの存在の確認は線形時間で行うことができる。したがって、そのような論理式の充足可能性は、最初にこの置き換えを実行し、次に結果として得られるホーン論理式の充足可能性をチェックすることによって解決できるため、Pに含まれる。^{[6] [7] [8] [9]}ホーン充足可能性と名前変更可能ホーン充足可能性は、多項式時間で解決可能な充足可能性の2つの重要なサブクラスのうちの1つを提供する。もう1つのサブクラスは2充足可能性である。

Horn SAT の双対バリアントはDual-Horn SATであり、各節には最大で 1 つの否定リテラルが含まれます。すべての変数を否定すると、Dual-Horn SAT のインスタンスが Horn SAT に変換されます。1951 年に Horn によって Dual-Horn SAT がPに属することが証明されました。^[要出典]

• ユニット伝播
• ブール充足可能性問題
• 2-満足可能性

• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel ; Vardi, Moshe Y .; Venema, Yde ; Weinstein, Scott (2007).有限モデル理論とその応用。理論計算機科学テキスト。EATCS シリーズ。ベルリン: Springer- Verlag。ISBN 978-3-540-00428-8.ZBL1133.03001  。​