満足度

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

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

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

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

否定を伴う古典的論理では、上記の対立の四角形で表現された概念間の関係により、式の妥当性の問題を満足可能性を含む問題に再表現することが一般的に可能です。特に、¬φ が満足不可能な場合にのみ φ は妥当であり、つまり、¬φ が満足可能であるというのは誤りです。言い換えると、¬φ が無効な場合にのみ φ は満足可能です。

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

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

一階述語論理（FOL）の場合、充足可能性は決定不能である。より具体的には、これは共RE完全な問題であり、したがって半決定可能ではない。^[3]この事実は、FOLの妥当性問題の決定不能性と関係している。妥当性問題の地位の問題は、いわゆるEntscheidungsproblemとして、最初にDavid Hilbertによって提起された。ゲーデルの完全性定理によれば、式の普遍妥当性は半決定可能問題である。充足可能性も半決定可能問題であれば、反モデルの存在の問題も半決定可能になる（式に反モデルが存在するのは、その否定が充足可能である場合に限る）。したがって、論理的妥当性の問題は決定可能になり、これはEntscheidungsproblem に対する否定の答えを示す結果で あるChurch–Turing 定理と矛盾する。

モデル理論では、原子式が充足可能であるとは、その式を真にする構造の要素の集合が存在する場合である。 ^[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})}$

結果として得られる式には無限モデルがありますが、有限モデルがないことが示されます (事実から始めて、2 番目の公理によって存在する必要がある原子のチェーンをたどると、モデルの有限性にはループの存在が必要になり、ループが別の要素に戻るか、別の要素に戻るかに関係なく、3 番目と 4 番目の公理に違反します)。 ${\displaystyle R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots }$${\displaystyle R(a_{0},a_{1})}$${\displaystyle R}$ ${\displaystyle a_{0}}$

特定のロジックで入力式の充足可能性を決定する計算の複雑さは、有限充足可能性を決定する計算の複雑さとは異なる場合があります。実際、一部のロジックでは、そのうちの 1 つだけが決定可能です。

古典的な一階述語論理の場合、有限充足可能性は再帰的に列挙可能（ REクラス）であり、式の否定に適用された トラクテンブロートの定理によって決定不可能である。

数値制約^{[明確化]は、}数学的最適化の分野でよく登場します。この分野では通常、何らかの制約の下で目的関数を最大化 (または最小化) することが求められます。しかし、目的関数を別にすれば、制約が満たされるかどうかを単純に決定するという基本的な問題は、設定によっては困難であったり、決定不可能であったりすることがあります。次の表は、主なケースをまとめたものです。

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

線形制約については、次の表でより詳しい説明が提供されます。

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

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

• Boolos, George; Burgess, John; Jeffrey, Richard (2007). Computability and Logic (第 5 版). Cambridge University Press.

• ダニエル・クローニング、オフェル・ストリッヒマン（2008年）。意思決定手順：アルゴリズム的観点から。Springer Science & Business Media。ISBN 978-3-540-74104-6。
• A. Biere、M. Heule、H. van Maaren、T. Walsh 編 (2009)。満足度ハンドブック。IOS Press。ISBN 978-1-60750-376-7。