満足可能性

数理論理学において、ある式は、その変数に何らかの値を割り当てることによって真となる場合に充足可能である。例えば、次の式${\displaystyle x+3=y}$は、次の場合に真となるため、充足可能である。${\displaystyle x=3}$そして${\displaystyle y=6}$式は${\displaystyle x+1=x}$は整数に対して充足可能ではない。充足可能性の双対概念は妥当性である。式は、その変数に値を割り当てるとすべて式が真になる場合に妥当である。例えば、${\displaystyle x+3=3+x}$整数に対して有効ですが、${\displaystyle x+3=y}$そうではない。

形式的には、充足可能性は、一階述語論理、二階述語論理 、命題論理など、許容される記号の構文を定義する固定された論理に関して研究されます。しかし、充足可能性は構文的なものではなく、記号の意味、例えば、の意味に関係するため、意味論的な性質です。${\displaystyle +}$式では${\displaystyle x+1=x}$形式的には、解釈（またはモデル）とは、変数への値の割り当てと、他のすべての非論理記号への意味の割り当てであると定義され、ある解釈によって真となる式が存在する場合、その式は充足可能であると言われます。^{[ 1 ]}これにより、次のような記号の非標準的な解釈が可能になります。${\displaystyle +}$追加の公理を与えることで、その意味を制限することができます。理論による充足可能性問題では、形式理論（有限または無限の公理の集合）に関して、論理式の充足可能性を検討します。

充足可能性と妥当性は単一の式に対して定義されますが、任意の理論または式の集合に一般化できます。理論は、少なくとも 1 つの解釈によって理論内のすべての式が真になる場合に充足可能であり、すべての解釈ですべての式が真である場合に妥当です。たとえば、ペアノ算術のような算術の理論は、自然数において真であるため充足可能です。この概念は理論の一貫性と密接に関連しており、実際には一階述語論理の一貫性と等価であり、ゲーデルの完全性定理として知られる結果です。充足可能性の否定は充足不可能であり、妥当性の否定は無効性です。これら 4 つの概念は、アリストテレスの対立の四角形とまったく同様の方法で互いに関連しています。

命題論理の式が充足可能かどうかを判定する問題は決定可能であり、ブール充足可能性問題、またはSATとして知られています。一般に、一階述語論理の文が充足可能かどうかを判定する問題は決定できません。普遍代数、等式理論、自動定理証明では、充足可能性を判定するために項書き換え、合同閉包、および単一化の方法が使用されます。特定の理論が決定可能かどうかは、その理論が変数フリーであるかどうか、およびその他の条件に依存します。^{[ 2 ]}

否定を含む古典論理においては、上記の対立四角形で表現される概念間の関係性から、論理式の妥当性に関する問題を充足可能性に関する問題に言い換えることが一般的に可能である。具体的には、φ が妥当であるのは、¬φ が充足不可能である場合、すなわち ¬φ が充足可能であることは偽である場合に限る。言い換えれば、φ が充足可能であるのは、¬φ が妥当でない場合に限られる。

否定を含まない論理体系、例えば肯定命題論理では、妥当性と充足可能性の問題は無関係である可能性がある。肯定命題論理の場合、すべての論理式が充足可能であるため、充足可能性の問題は自明である一方、妥当性の問題はco-NP完全である。

古典的な命題論理の場合、命題論理式の充足可能性は決定可能である。特に、充足可能性はNP完全問題であり、計算複雑性理論において最も集中的に研究されている問題の一つである。

一階述語論理(FOL)では、充足可能性は決定不能です。より具体的には、それは共RE完全問題であり、したがって半決定可能ではありません。^{[ 3 ]}この事実は、FOL の妥当性問題の決定不能性に関係しています。妥当性問題の状態に関する疑問は、いわゆる決定問題として、最初にデイヴィッド・ヒルベルトによって提起されました。式の普遍妥当性は、ゲーデルの完全性定理により半決定可能な問題です。充足可能性も半決定可能な問題であれば、反モデルの存在の問題も半決定可能になります (式が反モデルを持つのは、その否定が充足可能である場合に限る)。したがって、論理的妥当性の問題は決定可能になりますが、これは決定問題に対する否定的な答えを述べる結果であるチャーチ・チューリングの定理と矛盾します。

モデル理論では、原子式は、その式を真にする構造の要素の集合が存在する場合に充足可能である。 ^{[ 4 ]} Aが構造、φが式、aがφを満たす構造から取られた要素の集合である場合、一般に次のように記述される。

A ⊧ φ [a]

φに自由変数がない場合、つまりφが原子文であり、 Aによって満たされる場合、次のように書く。

A ⊧ φ

この場合、Aは φ のモデルである、あるいは φ はAにおいて真であると言うこともできる。TがAによって満たされる原子文の集合 (理論) である場合、次のように書く。

A ⊧ T

充足可能性に関連する問題の一つに、有限充足可能性の問題があります。これは、ある論理式がそれを真にする有限モデルを持つかどうかを判定する問題です。有限モデル特性を持つ論理体系の場合、充足可能性と有限充足可能性の問題は一致します。なぜなら、その論理体系の論理式は、有限モデルを持つ場合に限りモデルを持つからです。この問題は、有限モデル理論という数学分野において重要です。

有限充足可能性と充足可能性は一般に一致する必要はない。例えば、次の文の論理積として得られる一階述語論理式を考えてみよう。${\displaystyle a_{0}}$そして${\displaystyle a_{1}}$定数です。

• ${\displaystyle R(a_{0},a_{1})}$
• ${\displaystyle \forall xy(R(x,y)\rightarrow \exists zR(y,z))}$
• ${\displaystyle \forall xyz(R(y,x)\wedge R(z,x)\rightarrow y=z))}$
• ${\displaystyle \forall x\neg R(x,a_{0})}$

結果として得られる式は無限モデルを持つ${\displaystyle R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots }$しかし、有限モデルは存在しないことが示せる（${\displaystyle R(a_{0},a_{1})}$そして連鎖をたどって${\displaystyle R}$第二公理によって存在しなければならない原子、モデルの有限性にはループの存在が必要であり、それは第三公理と第四公理に違反する、それがループバックするかどうか${\displaystyle a_{0}}$または別の要素上）。

与えられた論理体系において入力式の充足可能性を判定する際の計算複雑度は、有限充足可能性を判定する際の計算複雑度とは異なる場合がある。実際、一部の論理体系では、どちらか一方のみが判定可能である。

古典的な一階述語論理では、有限充足可能性は再帰的に列挙可能（クラスRE内）であり、論理式の否定にトラクテンブロートの定理を適用することで決定不能となる。

数値制約は、数理最適化の分野でよく見られる問題であり、通常は何らかの制約の下で目的関数を最大化（または最小化）することが目的となります。しかし、目的関数はさておき、制約が充足可能かどうかを判断するという基本的な問題自体が、状況によっては困難であったり、決定不能であったりする場合があります。以下の表は、主なケースをまとめたものです。

表の出典：BockmayrとWeispfenning ^{[ 5 ]： 754}

線形制約については、以下の表でより詳細な情報が得られます。

表の出典：BockmayrとWeispfenning ^{[ 5 ]： 755}

• 2-充足可能性
• ブール充足可能性問題
• 回路充足可能性
• カープの21のNP完全問題
• 有効
• 制約充足

• ブーロス、ジョージ；バージェス、ジョン；ジェフリー、リチャード（2007）。計算可能性と論理（第5 版）。ケンブリッジ大学出版局。

• Daniel Kroening ; Ofer Strichman (2008). Decision Procedures: An Algorithmic Point of View . Springer Science & Business Media. ISBN 978-3-540-74104-6。
• A. ビエール、M. ヒューレ、H. ファン・マーレン、T. ウォルシュ編 (2009).満足可能性ハンドブック. IOS Press. ISBN 978-1-60750-376-7。