理論による充足可能性

コンピュータサイエンスと数理論理学において、理論による充足可能性( SMT ) は、数式が充足可能かどうかを判定する問題です。これは、ブール充足可能性問題(SAT) を、実数、整数、およびリスト、配列、ビットベクトル、文字列などのさまざまなデータ構造を含む、より複雑な数式に一般化したものです。この名称は、これらの式が等号を持つ一階述語論理の特定の形式理論(多くの場合、量化子を禁止) 内で (「モジュロ」で) 解釈されるという事実から来ています。SMTソルバーは、実用的な入力のサブセットに対して SMT 問題を解決することを目的としたツールです。Z3 や cvc5 などの SMT ソルバーは、自動定理証明、プログラム解析、プログラム検証、ソフトウェアテストなど、コンピュータサイエンスの幅広いアプリケーションの構成要素として使用されています。

ブール充足可能性問題はすでにNP完全であるため、SMT問題は一般的にNP困難であり、多くの理論では決定不能です。研究者は、どの理論または理論のサブセットが決定可能なSMT問題につながるか、および決定可能なケースの計算複雑性を研究しています。結果として得られる決定手順は、多くの場合、SMTソルバーに直接実装されます。たとえば、プレスバーガー算術の決定可能性を参照してください。SMTは制約充足問題、したがって制約プログラミングへのある種の形式化されたアプローチと考えることができます。

形式的には、SMT インスタンスは、関数と述語の記号にいくつかの追加解釈がある一階述語論理の式であり、SMT はそのような式が充足可能かどうかを判定する問題です。言い換えれば、ブール充足可能性問題(SAT) のインスタンスで、バイナリ変数の一部が適切な非バイナリ変数の集合に対する述語に置き換えられているものを想像してください。述語は、非バイナリ変数のバイナリ値関数です。述語の例には、線形不等式(例:${\displaystyle 3x+2y-z\geq 4}$）または解釈されていない項と関数記号を含む等式（例：${\displaystyle f(f(u,v),v)=f(u,v)}$どこ${\displaystyle f}$は、2 つの引数の未指定関数です。これらの述語は、それぞれ割り当てられた理論に従って分類されます。たとえば、実変数に関する線形不等式は、線形実数算術の理論の規則を使用して評価されますが、解釈されていない項や関数記号を含む述語は、等号を持つ解釈されていない関数の理論（空理論と呼ばれることもあります）の規則を使用して評価されます。その他の理論には、配列とリスト構造の理論（コンピュータ プログラムのモデリングと検証に役立ちます）、ビットベクトルの理論（ハードウェア設計のモデリングと検証に役立ちます）などがあります。サブ理論も可能です。たとえば、差分論理は線形算術のサブ理論であり、各不等式は の形式に制限されます。${\displaystyle xy>c}$変数について${\displaystyle x}$そして${\displaystyle y}$そして絶え間ない${\displaystyle c}$。

上記の例は、不等式に対する線形整数演算の使用例を示しています。その他の例としては、以下のようなものがあります。

• 充足可能性: が満たされるかどうかを判断する${\displaystyle x\vee (y\wedge \neg z)}$充足可能である。
• 配列へのアクセス: 配列Aに対してA [0]  =  5となるような値を見つけます 。
• ビットベクトル演算：xとyが異なる3ビット数値であるかどうかを判定します。
• 未解釈関数: xとyの値を求め、${\displaystyle f(x)=2}$そして${\displaystyle g(x)=3}$。

ほとんどのSMTソルバーは、量化子を含まない論理フラグメントのみをサポートしています。

SMTソルバーと自動定理証明（ATP）にはかなりの重複があります。一般的に、自動定理証明器は量化子を含む完全な一階述語論理のサポートに重点を置いていますが、SMTソルバーはさまざまな理論（解釈された述語記号）のサポートに重点を置いています。ATPは量化子が多い問題に優れていますが、SMTソルバーは量化子のない大きな問題に優れています。^{[ 1 ]}この境界線は曖昧で、一部のATPはSMT-COMPに参加し、一部のSMTソルバーはCASCに参加しています。^{[ 2 ]}

SMTインスタンスは、ブールSATインスタンスを一般化したもので、様々な変数セットが、多様な基礎理論に基づく述語に置き換えられています。SMT式は、ブールSAT式よりもはるかに豊富なモデリング言語を提供します。例えば、SMT式を用いることで、マイクロプロセッサのデータパス動作をビットレベルではなくワードレベルでモデル化することが可能になります。

それに比べて、解答セットプログラミングも述語（より正確には、原子式から作成された原子文）に基づいています。SMTとは異なり、解答セットプログラムには量化子がなく、線形算術や差分論理などの制約を容易に表現できません。解答セットプログラミングは、解釈されない関数の自由理論に帰着するブール問題に最適です。解答セットプログラミングで32ビット整数をビットベクトルとして実装すると、初期のSMTソルバーが直面したのと同じ問題のほとんどに悩まされます。x + y = y + xのような「明白な」恒等式を推論するのは困難です。      

制約論理プログラミングは線形算術制約をサポートしていますが、全く異なる理論的枠組みの中で行われます。SMTソルバーは高階論理の数式を解くようにも拡張されています。^{[ 3 ]}

SMT インスタンスを解決するための初期の試みでは、それらをブール SAT インスタンスに変換し (たとえば、32 ビット整数変数は適切な重みを持つ 32 個の 1 ビット変数でエンコードされ、「プラス」などのワードレベルの演算はビットに対する低レベルの論理演算に置き換えられます)、この式をブール SAT ソルバーに渡していました。このアプローチは、積極的なアプローチ(またはビットブラスト) と呼ばれ、利点があります。SMT 式を同等のブール SAT 式に前処理することで、既存のブール SAT ソルバーを「そのまま」使用でき、時間の経過とともにパフォーマンスと容量の向上を活用できます。一方、基礎となる理論の高レベルの意味論が失われるため、ブール SAT ソルバーは「明白な」事実 (たとえば、${\displaystyle x+y=y+x}$（整数加算の場合）この観察により、 DPLLスタイルの検索のブール推論と、特定の理論からの述語の論理積（AND）を処理する理論固有のソルバー（ T ソルバー）を密接に統合した多数のSMT ソルバーが開発されました。このアプローチは、遅延アプローチと呼ばれています。^{[ 4 ]}

DPLL(T) [ ^{5 ]と}呼ばれるこのアーキテクチャは、ブール推論の責任を DPLL ベースの SAT ソルバーに委ね、SAT ソルバーは、明確に定義されたインターフェースを介して理論 T のソルバーとやり取りします。理論ソルバーは、式のブール探索空間を探索する際に、SAT ソルバーから渡された理論述語の論理積の実行可能性をチェックすることだけを気にすればよいのです。ただし、この統合がうまく機能するためには、理論ソルバーは伝播と競合分析に参加できなければなりません。つまり、既に確立された事実から新しい事実を推論でき、理論の競合が発生した場合には実行不可能性の簡潔な説明を提供できる必要があります。言い換えれば、理論ソルバーは増分的でバックトラック可能でなければなりません。

研究者たちは、どの理論または理論のサブセットが決定可能なSMT問題につながるか、また決定可能なケースの計算複雑性を研究している。完全な一階述語論理は半決定可能であるため、一階述語論理の断片（実質的には命題論理など）に対する効率的な決定手続きを見つけようとする研究もある。^{[ 6 ]}

別の研究分野としては、有理数と整数に対する線形算術、固定幅ビットベクトル、^{[ 7 ]}浮動小数点算術（ビットブラスト、つまりビットベクトルへの還元によってSMTソルバーで実装されることが多い）、^{[ 8 ] [ 9 ]}文字列、^{[ 10 ]}（共）データ型、^{[ 11 ]}シーケンス（動的配列のモデル化に使用）、^{[ 12 ]}有限集合と関係、^{[ 13 ] [ 14 ]}分離論理、^{[ 15 ]}有限体、^{[ 16 ]}および解釈されない関数など、特殊な決定可能理論の開発がある。

ブール単調理論は、効率的な理論伝播と競合分析をサポートする理論クラスであり、DPLL(T)ソルバー内での実用的な利用を可能にします。^{[ 17 ]}単調理論はブール変数のみをサポートし（ブールが唯一のソート）、そのすべての関数と述語pは公理に従います。

${\displaystyle p(\ldots ,b_{i-1},0,b_{i+1},\ldots )\implies p(\ldots ,b_{i-1},1,b_{i+1},\ldots )}$

単調理論の例としては、グラフ到達可能性、凸包の衝突検出、最小カット、計算ツリーロジックなどがあります。^{[ 18 ]}すべてのDatalogプログラムは単調理論として解釈できます。^{[ 19 ]}

一般的なSMTアプローチのほとんどは、決定可能な理論をサポートしています。しかし、航空機とその挙動など、多くの現実世界のシステムは、超越関数を含む実数上の非線形演算によってのみモデル化できます。この事実から、SMT問題を非線形理論に拡張する動機が生まれます。例えば、次の式が充足可能かどうかを判定する問題などです。

${\displaystyle {\begin{array}{lr}&(\sin(x)^{3}=\cos(\log(y)\cdot x)\vee b\vee -x^{2}\geq 2.3y)\wedge \left(\neg b\vee y<-34.4\vee \exp(x)>{y \over x}\right)\end{array}}}$

どこ

${\displaystyle b\in {\mathbb {B} },x,y\in {\mathbb {R} }.}$

しかしながら、このような問題は一般には決定不能である。（一方、実閉体の理論、ひいては実数の完全な一階理論は、量化子消去法を用いて決定可能である。これはアルフレッド・タルスキによるものである。）加算（乗算は含まない）を伴う自然数の一階理論、すなわちプレスバーガー算術もまた決定可能である。定数による乗算は入れ子になった加算として実装できるため、多くのコンピュータプログラムの算術演算はプレスバーガー算術を用いて表現でき、決定可能な式が得られる。

実数上の決定不能な算術理論からの理論原子のブール結合を扱うSMTソルバーの例としては、^非線形最適化パケットを（必然的に不完全な）従属理論ソルバーとして用いる古典的なDPLL(T)アーキテクチャを採用したABsolver ^{[ 20} ] 、DPLL SATソルビングと区間制約伝播の統合に基づくiSATアルゴリズム^{[ 21 ]} 、およびcvc5 ^{[ 22 ]}がある。

以下の表は、利用可能な多くのSMTソルバーの機能の一部をまとめたものです。「SMT-LIB」列はSMT-LIB言語との互換性を示します。「はい」とマークされているシステムの多くは、SMT-LIBの古いバージョンのみをサポートしているか、言語を部分的にしかサポートしていない可能性があります。「CVC」列はCVC言語のサポートを示します。「DIMACS」列はDIMACSフォーマットのサポートを示します。

プロジェクトは、機能や性能だけでなく、周辺コミュニティの存続可能性、プロジェクトへの継続的な関心、そしてドキュメント、修正、テスト、機能強化への貢献能力においても異なっている。

SMTソルバーは、プログラムの正しさを証明する検証、記号実行に基づくソフトウェアテスト、および可能なプログラムの空間を探索してプログラム断片を生成する合成の両方に役立ちます。ソフトウェア検証以外では、SMTソルバーは型推論^{[ 26 ] [ 27 ]}や、核兵器管理における行為者の信念のモデリングを含む理論的シナリオのモデリングにも使用されています。^{[ 28 ]}

• 解答セットプログラミング
• 自動定理証明
• SATソルバー
• 一階述語論理
• 純粋平等理論

• この記事は、 Karem A. Sakallah氏がACM SIGDAの電子ニュースレターに掲載したコラムを基に作成されたものです。原文はこちらからご覧いただけます。