充足可能性

数理論理学において、論理式が充足可能（じゅうそくかのう、テンプレート:Lang-en-short）であるとは、その変数への何らかの値の割り当てのもとで真になることをいう。例えば論理式 $x+3=y$ は $x=3$ かつ $y=6$ のときに真になるため充足可能であるが、論理式 $x+1=x$ は整数上では充足可能ではない。充足可能性の双対概念は妥当性である。ある論理式が妥当であるとは、変数へのあらゆる値の割り当てがその論理式を真にすることをいう。例えば $x+3=3+x$ は整数上で妥当であるが、$x+3=y$ はそうではない。

形式的には、充足可能性は一階述語論理・二階述語論理・命題論理など、許容される記号の統語論を定める固定された論理に関して研究される。しかし充足可能性は統語論的な性質ではなく意味論的な性質である。というのも、それは記号の意味に関わるからである。例えば $x+1=x$ のような論理式における $+$ の意味である。形式的には、解釈（またはモデル）を、変数への値の割り当てと、それ以外のすべての非論理記号への意味の割り当てとして定義し、ある論理式を真にする解釈が存在するとき、その論理式は充足可能であるというテンプレート:Sfn。これは $+$ のような記号の非標準的な解釈をも許すが、追加の公理を与えることでその意味を制限できる。テンプレート:仮リンクの問題は、（有限あるいは無限の）公理の集合である形式理論に関する論理式の充足可能性を考える。

充足可能性と妥当性は単一の論理式に対して定義されるが、任意の理論あるいは論理式の集合へと一般化できる。すなわち、ある理論が充足可能であるとは、少なくとも一つの解釈がその理論に属するすべての論理式を真にすることをいい、妥当であるとは、すべての論理式があらゆる解釈において真であることをいう。例えばペアノ算術のような算術の理論は、自然数において真であるため充足可能である。この概念は理論の無矛盾性と密接に関連しており、実際、一階述語論理においては無矛盾性と同値である。これはゲーデルの完全性定理として知られる結果である。充足可能性の否定は充足不能性、妥当性の否定は非妥当性である。これら四つの概念は、アリストテレスの対当の四角形とちょうど同型の仕方で互いに関連している。

命題論理の論理式が充足可能かどうかを判定する問題は決定可能であり、充足可能性問題（SAT）として知られる。一般に、一階述語論理の文が充足可能かどうかを判定する問題は決定可能ではない。普遍代数学、テンプレート:仮リンク、自動定理証明においては、項書き換え、テンプレート:仮リンク、ユニフィケーションといった手法が充足可能性を判定するために用いられる。特定の理論が決定可能かどうかは、その理論が変数を含まないものであるかどうか、およびその他の条件に依存する。

妥当性の充足可能性への還元

否定をもつ古典論理においては、上述の対当の四角形に表される概念間の関係により、論理式の妥当性に関する問いを充足可能性に関する問いへ言い換えることが一般に可能である。とりわけ、φ が妥当であるのは ¬φ が充足不能であるとき、かつそのときに限る。すなわち ¬φ が充足可能であることが偽であるときである。言い換えれば、φ が充足可能であるのは ¬φ が非妥当であるとき、かつそのときに限る。

テンプレート:仮リンクのように否定をもたない論理においては、妥当性と充足可能性の問いは無関係でありうる。正命題計算の場合、すべての論理式が充足可能であるため充足可能性問題は自明である一方、妥当性問題はテンプレート:仮リンクである。

古典論理における命題の充足可能性

テンプレート:Main 古典命題論理の場合、充足可能性は命題論理式について決定可能である。とりわけ充足可能性はNP完全問題であり、計算複雑性理論において最も集中的に研究されてきた問題の一つである。

一階述語論理における充足可能性

一階述語論理（FOL）においては、充足可能性は決定不能である。より正確には、これはテンプレート:仮リンク問題であり、したがってテンプレート:仮リンクですらない。この事実はFOLの妥当性問題の決定不能性と関係している。妥当性問題の位置づけについての問いを最初に提起したのはダフィット・ヒルベルトであり、いわゆるテンプレート:仮リンクである。論理式の普遍的妥当性はゲーデルの完全性定理により半決定可能な問題である。もし充足可能性もまた半決定可能な問題であったならば、反例モデルの存在の問題もそうであることになる（論理式が反例モデルをもつのは、その否定が充足可能であるとき、かつそのときに限る）。そうすると論理的妥当性の問題は決定可能となり、決定問題への否定的な答えを述べた結果であるテンプレート:仮リンクと矛盾する。

モデル理論における充足可能性

モデル理論において、原子論理式が充足可能であるとは、その論理式を真にする構造の元の集まりが存在することをいう。A が構造、φ が論理式、a が構造から取られた φ を充足する元の集まりであるとき、通常次のように書かれる。

A ⊧ φ [a]

φ が自由変数をもたない場合、すなわち φ が原子文であって A によって充足される場合には、次のように書く。

A ⊧ φ

この場合、A は φ のモデルである、あるいは φ は A において真である、ともいう。T が A によって充足される原子文の集まり（理論）であるとき、次のように書く。

A ⊧ T

有限充足可能性

充足可能性に関連する問題として有限充足可能性がある。これは、ある論理式がそれを真にする有限なモデルをもつかどうかを判定する問いである。テンプレート:仮リンクをもつ論理においては、充足可能性の問題と有限充足可能性の問題は一致する。その論理の論理式がモデルをもつのは、有限モデルをもつとき、かつそのときに限るからである。この問いは有限モデル理論という数学の分野において重要である。

有限充足可能性と充足可能性は一般には一致しない。例えば、$a_0$ と $a_1$ を定数として、次の文の連言として得られる一階述語論理の論理式を考える。

• $R(a_0,a_1)$
• $\mathrm{\forall }xy(R(x,y)\to \mathrm{\exists }zR(y,z))$
• $\mathrm{\forall }xyz(R(y,x)\wedge R(z,x)\to y=z))$
• $\mathrm{\forall }x\mathrm{\neg }R(x,a_0)$

得られる論理式は無限モデル $R(a_0,a_1),R(a_1,a_2),\dots$ をもつが、有限モデルをもたないことが示せる（事実 $R(a_0,a_1)$ から出発し、第2の公理により存在しなければならない $R$ 原子式の連鎖をたどると、モデルが有限であるためにはループの存在が必要となるが、それが $a_0$ に戻る場合でも別の元に戻る場合でも、第3および第4の公理に反する）。

与えられた論理において入力論理式の充足可能性を判定することの計算複雑性は、有限充足可能性を判定することの計算複雑性と異なりうる。実際、ある種の論理では一方だけが決定可能である。

古典的な一階述語論理については、有限充足可能性は帰納的可算（クラスREに属する）であり、論理式の否定にテンプレート:仮リンクを適用することにより決定不能である。

数値制約

テンプレート:Further 数値制約テンプレート:要説明は数理最適化の分野にしばしば現れる。そこでは通常、いくつかの制約のもとで目的関数を最大化（または最小化）することが求められる。しかし目的関数を措いても、制約が充足可能かどうかを単に判定するという基本的な問題が、設定によっては困難であったり決定不能であったりする。次の表は主要な場合をまとめたものである。

制約の対象:	実数	整数
線形	PTIME（線形計画法を参照）	NP完全（整数計画問題を参照）
多項式	決定可能（例えばテンプレート:仮リンクによる）	決定不能（テンプレート:仮リンク）

出典: Bockmayr and Weispfenningテンプレート:Rp。

線形制約については、次の表がより詳しい状況を示している。

制約の対象:	有理数	整数	自然数
線形方程式	PTIME	PTIME	NP完全
線形不等式	PTIME	NP完全	NP完全

出典: Bockmayr and Weispfenningテンプレート:Rp。

関連項目

• テンプレート:仮リンク
• 充足可能性問題
• 回路充足可能性
• テンプレート:仮リンク
• 妥当性
• 制約充足問題

参考文献

• テンプレート:Cite book

関連文献

• テンプレート:Cite book
• テンプレート:Cite book