計算機科学および数理論理学における充足可能性モジュロ理論（じゅうそくかのうせいモジュロりろん、、SMT）とは、ある数学的な論理式が充足可能であるかどうかを判定する問題である。SMTは充足可能性問題（SAT）を、実数・整数やリスト・配列・・といった各種のデータ構造を扱うより複雑な論理式へと一般化したものである。この名称は、これらの式が等号付き一階述語論理における特定の形式的理論の内部で（すなわち「モジュロ」その理論のもとで）解釈されることに由来する（多くの場合、量化子は許容されない）。SMTソルバは、実用的な入力の部分集合について SMT 問題を解くことを目的としたツールである。 や などの SMT ソルバは、自動定理証明、プログラム解析、プログラム検証、ソフトウェアテストなど、計算機科学の広範な応用の構成要素として用いられてきた。
ブール充足可能性がすでにNP完全であるため、SMT 問題は一般にNP困難であり、多くの理論ではである。研究者たちは、どの理論あるいは理論の部分集合が決定可能な SMT 問題を導くのか、および決定可能な場合の計算複雑性について研究している。得られた決定手続きはしばしば SMT ソルバに直接実装される（例としてプレスバーガー算術の決定可能性を参照）。SMT は制約充足問題と見なすこともでき、したがって制約プログラミングへの一定の形式化されたアプローチとも言える。
用語と例 形式的に述べれば、SMT インスタンスとは、いくつかの関数記号や述語記号に追加の解釈が与えられた一階述語論理の論理式であり、SMT はそのような論理式が充足可能であるかを判定する問題である。言い換えると、充足可能性問題（SAT）のインスタンスにおいて、の一部が、二値でない変数の適当な集合上ので置き換えられたものを想像すればよい。述語とは、二値でない変数を引数とする二値関数のことである。述語の例としては、線形不等式（例: ）や、および関数記号を含む等式（例: 。ここで は2引数の未指定の関数）などがある。これらの述語は、それぞれ割り当てられた理論に従って分類される。たとえば、実数変数上の線形不等式は線形実算術の理論の規則を用いて評価され、非解釈項および関数記号を含む述語は等号付きの理論（と呼ばれることもある）の規則を用いて評価される。その他の理論には、（コンピュータプログラムのモデル化・検証に有用な）配列およびリスト構造の理論や、（のモデル化・検証に有用な）の理論などがある。部分理論も可能である。たとえばは線形算術の部分理論であり、各不等式は変数 , と定数 による という形に制限される。
上の例は線形整数算術による不等式の使用を示している。他の例を挙げる。 充足可能性: が充足可能かどうかを判定する。 配列アクセス: 配列 A に対して A = 5 となる値を見つける。 ビットベクトル算術: x と y が異なる 3 ビット数であるかを判定する。 非解釈関数: かつ となる x, y の値を見つける。
ほとんどの SMT ソルバは論理式の量化子を含まない断片のみをサポートする。
自動定理証明との関係 SMT 解法と自動定理証明（ATP）には実質的な重なりがある。一般に、自動定理証明系は量化子を含む完全な一階述語論理の支援に注力するのに対し、SMT ソルバはより多様な理論（解釈付き述語記号）の支援に注力する。ATP は量化子が多く含まれる問題に強く、SMT ソルバは量化子を含まない大規模な問題を得意とする。両者の境界はあいまいであり、ATP の一部は SMT-COMP に参加し、SMT ソルバの一部は に参加している。
表現力 SMT インスタンスは、変数の各集合が多様な基礎理論に由来するで置き換えられたブール SAT インスタンスの一般化である。SMT 論理式は、ブール SAT 論理式で可能なものよりもはるかに豊かなモデリング言語を提供する。たとえば、SMT 論理式では、マイクロプロセッサの演算をビット単位ではなくワード単位でモデル化できる。
比較として、解集合プログラミングもまた述語に基づく（より正確には、原子論理式から作られる原子文に基づく）。SMT とは異なり、解集合プログラムには量化子がなく、線形算術やのような制約を容易に表現できない。解集合プログラミングは、非解釈関数のに還元できるブール問題に最も適している。解集合プログラミングにおいて 32 ビット整数をビットベクトルとして実装することは、初期の SMT ソルバが直面したのと同じ問題の多くを抱える。すなわち、x + y = y + x のような「自明な」恒等式を導出することが困難である。
制約論理プログラミングは線形算術制約のサポートを提供しているが、完全に異なる理論的枠組みの中でである。SMT ソルバは高階論理の論理式を解くようにも拡張されてきた。
ソルバのアプローチ SMT インスタンスを解く初期の試みでは、それらをブール SAT インスタンスに変換していた（たとえば、32 ビット整数変数を適切な重み付きの 32 個の 1 ビット変数として符号化し、「加算」のようなワードレベルの演算をビット上のより低レベルの論理演算に置き換えるといった具合である）。そしてこの論理式をブール SAT ソルバに渡していた。このアプローチは、イーガーアプローチ（ビットブラスティング）と呼ばれ、以下の利点を持つ。すなわち、SMT 論理式を等価なブール SAT 論理式に前処理することで、既存のブール SAT ソルバを「そのまま」利用でき、時間とともに得られる性能・容量の改善を活用できる。他方で、基礎理論の高レベル意味論が失われることは、（整数加算の のような）「自明な」事実を発見するためにブール SAT ソルバが必要以上に多く働かねばならないことを意味する。この観察を受けて、DPLL 方式の探索によるブール推論と、与えられた理論の述語の論理積（AND）を扱う理論固有ソルバ（T ソルバ）とを密結合する多くの SMT ソルバが開発された。このアプローチはレイジーアプローチと呼ばれる。
と呼ばれるこのアーキテクチャは、ブール推論の責任を DPLL に基づく SAT ソルバに委ね、SAT ソルバは適切に定義されたインタフェースを通じて理論 T のソルバと対話する。理論ソルバは、SAT ソルバが論理式のブール探索空間を探索する際に SAT ソルバから渡される理論述語の論理積の充足可能性を確認することだけを心配すればよい。ただし、この統合がうまく機能するためには、理論ソルバが伝搬と衝突解析に参加できる必要がある。すなわち、既に確立された事実から新しい事実を導出でき、また理論衝突が生じた際には非充足性の簡潔な説明を提供できなければならない。言い換えれば、理論ソルバはインクリメンタルであり、かつバックトラック可能でなければならない。
決定可能な理論 研究者たちは、どの理論あるいは理論の部分集合が決定可能な SMT 問題を導くのか、また決定可能な場合の計算複雑性について研究している。完全な一階述語論理はでしかないため、研究の一つの方向はのような一階述語論理の断片に対する効率的な決定手続きを見出すことを試みる。
もう一つの研究方向は、有理数および整数上の線形算術、固定幅ビットベクトル、浮動小数点算術（多くの場合、SMT ソルバでは bit-blasting、すなわちビットベクトルへの還元によって実装される）、、(余)データ型、（動的配列のモデル化に用いられる）列、有限集合および関係、、有限体、その他多くを含む、専門化されたの開発を含む。
ブール単調理論は、効率的な理論伝搬と衝突解析を支援する理論のクラスであり、DPLL(T) ソルバ内で実用的に使用できる。単調理論はブール変数のみをサポートし（ブールが唯一のソートである）、そのすべての関数と述語 は次の公理に従う。
単調理論の例には、グラフ到達可能性、凸包の衝突判定、最小カット、計算木論理などがある。すべての プログラムは単調理論として解釈できる。
決定不能な理論に対する SMT 一般的な SMT アプローチのほとんどはをサポートする。しかし、航空機とその挙動のような現実世界の多くのシステムは、超越関数を含む実数上の非線形算術によってのみモデル化できる。この事実が、SMT 問題を非線形理論へ拡張する動機となる。たとえば以下の等式が充足可能かどうかを判定するといった問題である。
ここで
このような問題は、一般にはである。（他方で、実閉体の理論、したがって実数の完全な一階の理論は、によって決定可能である。これはアルフレト・タルスキによる。）自然数における加算（だが乗算は含まない）の一階の理論、プレスバーガー算術と呼ばれるものもまた決定可能である。定数による乗算はネストした加算として実装できるため、多くのコンピュータプログラムにおける算術はプレスバーガー算術で表現でき、その結果決定可能な論理式が得られる。
決定不能な実数の算術理論に由来する理論原子のブール結合を扱う SMT ソルバの例としては、古典的な DPLL(T) アーキテクチャと（必然的に不完全な）従属理論ソルバとしての非線形最適化パケットを採用する 、iSAT アルゴリズムと呼ばれる DPLL SAT 解法と区間制約伝搬の統合の上に構築される iSAT、そして が挙げられる。
以下の表は、多くの利用可能な SMT ソルバの機能の一部をまとめたものである。「SMT-LIB」列は SMT-LIB 言語との互換性を示す。「yes」と示されている多くのシステムは、SMT-LIB の古いバージョンのみをサポートしているか、言語の部分的なサポートしか提供していない場合がある。「CVC」列は 言語のサポートを示す。「DIMACS」列は フォーマットのサポートを示す。
プロジェクトは、機能や性能だけでなく、周辺コミュニティの実現可能性、プロジェクトへの継続的な関心、ドキュメント・修正・テスト・拡張への貢献能力においても異なる。
プラットフォーム 機能 備考 名称 OS ライセンス SMT-LIB CVC DIMACS 組み込み理論 API SMT-COMP ABsolver Linux CPL 線形算術、非線形算術 C++ no DPLL ベース Linux、Mac OS、Windows CeCILL-C（おおよそ LGPL と同等） 空理論、線形整数・有理算術、非線形算術、多相配列、列挙型データ型、AC 記号、ビットベクトル、レコード型、量化子 OCaml 2008 ML 風の多相一階入力言語。SAT ソルバベース。理論モジュロ推論のために Shostak 風と Nelson–Oppen 風のアプローチを組み合わせる Barcelogic Linux プロプライエタリ 空理論、差分論理 C++ 2009 DPLL ベース、 Beaver Linux、Windows BSD ビットベクトル OCaml 2009 SAT ソルバベース Boolector Linux MIT ビットベクトル、配列 C 2009 SAT ソルバベース CVC3 Linux BSD 空理論、線形算術、配列、タプル、型、レコード、ビットベクトル、量化子 C/C++ 2010 HOL への証明出力 CVC4 Linux、Mac OS、Windows、FreeBSD BSD 有理・整数線形算術、配列、タプル、レコード、帰納的データ型、ビットベクトル、文字列、非解釈関数記号上の等号 C++ 2021 バージョン 1.8 が 2021 年 5 月にリリース Linux、Mac OS、Windows BSD 有理・整数線形算術、配列、タプル、レコード、帰納的データ型、ビットベクトル、有限体、文字列、列、バッグ、および非解釈関数記号上の等号 C++、Python、Java 2021 バージョン 1.0 が 2022 年 4 月にリリース Decision Procedure Toolkit (DPT) Linux Apache OCaml no DPLL ベース iSAT Linux プロプライエタリ 非線形算術 no DPLL ベース MathSAT Linux、Mac OS、Windows プロプライエタリ 空理論、線形算術、非線形算術、ビットベクトル、配列 C/C++、Python、Java 2010 DPLL ベース MiniSmt Linux LGPL 非線形算術 OCaml 2010 SAT ソルバベース、Yices ベース Norn 文字列制約用の SMT ソルバ Linux AGPL 確率論理、算術、関係モデル C++、Scheme、Python no 部分グラフ同型 OpenSMT Linux、Mac OS、Windows GPLv3 空理論、差分、線形算術、ビットベクトル C++ 2011 遅延評価 SMT ソルバ raSAT Linux GPLv3 実数および整数の非線形算術 2014, 2015 テスト付き区間制約伝搬と中間値定理の拡張 SatEEn ? プロプライエタリ 線形算術、差分論理 なし 2009 SMTInterpol Linux、Mac OS、Windows 非解釈関数、線形実算術、線形整数算術 Java 2012 高品質でコンパクトな補間を生成することに注力 SMCHR Linux、Mac OS、Windows GPLv3 線形算術、非線形算術、ヒープ C no を用いて新しい理論を実装できる SMT-RAT Linux、Mac OS MIT 線形算術、非線形算術 C++ 2015 SMT 対応実装のコレクションからなる、戦略的・並列 SMT 解法のためのツールボックス SONOLAR Linux、Windows プロプライエタリ ビットベクトル C 2010 SAT ソルバベース Spear Linux、Mac OS、Windows プロプライエタリ ビットベクトル 2008 STP Linux、OpenBSD、Windows、Mac OS MIT ビットベクトル、配列 C、C++、Python、OCaml、Java 2011 SAT ソルバベース SWORD Linux プロプライエタリ ビットベクトル 2009 UCLID Linux BSD 空理論、線形算術、ビットベクトル、および制約ラムダ（配列、メモリ、キャッシュなど） no SAT ソルバベース、 で書かれている。入力言語は SMV モデル検査器。よく文書化されている。 veriT Linux、OS X BSD 空理論、有理・整数線形算術、量化子、非解釈関数記号上の等号 C/C++ 2010 SAT ソルバベース、証明を生成可能 Linux、Mac OS、Windows、FreeBSD GPLv3 有理・整数線形算術、ビットベクトル、配列、非解釈関数記号上の等号 C 2014 ソースコードはオンラインで入手可能 Linux、Mac OS、Windows、FreeBSD MIT 空理論、線形算術、非線形算術、ビットベクトル、配列、データ型、量化子、文字列 C/C++、.NET、OCaml、Python、Java、Haskell 2011 ソースコードはオンラインで入手可能
標準化と SMT-COMP ソルバ競技会 SMT ソルバ（および自動定理証明系。この用語はしばしば同義的に用いられる）への標準化されたインタフェースを記述する複数の試みがある。最も顕著なのは SMT-LIB 標準であり、これは S式に基づく言語を提供する。他に一般的に支援されている標準化された形式には、多くのブール SAT ソルバによって支援される DIMACS 形式や、CVC 自動定理証明系が用いる CVC 形式がある。
SMT-LIB 形式にはいくつかの標準化されたベンチマークも付属しており、SMT-COMP と呼ばれる SMT ソルバ間の年次競技会を可能にしている。当初、この競技会は 会議（CAV）の間に開催されていた。しかし 2020 年からは、（IJCAR）と提携する SMT ワークショップの一部として競技会が開催されている。
応用 SMT ソルバは、プログラムのの証明、に基づくソフトウェアテストといった検証、およびプログラム合成（可能なプログラムの空間を探索してプログラム断片を生成する）の両方に有用である。ソフトウェア検証の外でも、SMT ソルバは型推論Loncaric, Calvin, et al. "A practical framework for type inference error explanation." ACM SIGPLAN Notices 51.10 (2016): 781-799.や、核軍備管理における当事者の信念のモデル化を含む理論的シナリオのモデル化にも用いられている。
検証 コンピュータプログラムのコンピュータ支援検証では、しばしば SMT ソルバが用いられる。一般的な技法は、事前条件、事後条件、ループ条件、およびアサーションを SMT 論理式に変換し、すべての性質が成立するかを判定するものである。
の上に構築された検証器は数多い。Boogie は Z3 を用いて単純な命令型プログラムを自動的に検査する中間検証言語である。並行 C のための VCC 検証器は Boogie を用いており、命令型オブジェクトベースプログラム向けの Dafny、並行プログラム向けの Chalice、C# 向けの Spec# も同様である。F* は Z3 を用いて証明を見つける依存型付き言語であり、コンパイラはこれらの証明を証明担持バイトコードの生成にまで持ち込む。Viper 検証インフラストラクチャは検証条件を Z3 に符号化する。sbv ライブラリは Haskell プログラムの SMT ベース検証を提供し、ユーザは Z3、ABC、Boolector、cvc5、MathSAT、Yices など多数のソルバから選択できる。
SMT ソルバの上に構築された検証器も数多い。以下は成熟した応用の一覧である。 Why3、演繹的プログラム検証のためのプラットフォーム。主要な証明系として Alt-Ergo を用いる。 CAVEAT、CEA によって開発され Airbus によって使用される C 検証器。Alt-Ergo は最近の航空機の一つの DO-178C 認証に含まれた。 Frama-C、C コード解析のためのフレームワーク。（「演繹的プログラム検証」専用の）Jessie および WP プラグインで Alt-Ergo を用いる。 は SPARK 2014 における一部のアサーションの検証を自動化するために（GNATprove の背後で）CVC4 と Alt-Ergo を用いる。 は主要な証明系の代わりに Alt-Ergo を用いることができる（ANR Bware プロジェクトのベンチマークで成功率が 84% から 98% に増加した）。 、Systerel によって開発された B メソッドフレームワークで、Alt-Ergo をバックエンドとして用いることができる。 Cubicle、配列ベース遷移システムの安全性を検証するオープンソースのモデル検査器。 EasyCrypt、敵対的コードを含む確率的計算の関係的性質について推論するためのツール集。
多くの SMT ソルバは、SMTLIB2 と呼ばれる共通のインタフェース形式を実装している（そのようなファイルは通常「.smt2」拡張子を持つ）。LiquidHaskell ツールは、cvc5、MathSat、Z3 など任意の SMTLIB2 準拠ソルバを使用できる、Haskell 向けの精密化型に基づく検証器を実装している。
シンボリック実行に基づく解析とテスト SMT ソルバの重要な応用は、プログラムの解析とテストのためのである（など）。特にセキュリティ脆弱性の発見を目的としている。このカテゴリのツール例には、Microsoft Research の SAGE、KLEE、S2E、Triton などがある。シンボリック実行の応用に用いられてきた SMT ソルバには、Z3、STP、Z3str 系ソルバ、Boolector などがある。
対話的定理証明 SMT ソルバは、や など、証明支援系と統合されてきた。
合成 SMT ソルバは、仕様からプログラムを自動生成するプログラム合成の中核的構成要素である。代表的なアプローチは（CEGIS）であり、そこでは合成系が候補プログラムを提案し、SMT ソルバがそれを検証する。失敗した検査からの反例が、正しい解が見つかるまで合成系を誘導する。
関連する応用として、がある。バグのあるプログラムとテストスイートが与えられると、その解がパッチを生じさせる SMT 論理式が構築される。たとえば Nopol は、修復された条件式を見つける問題を SMT インスタンスとして符号化し、解を Java プログラムのソースコードパッチへと変換し戻す。
脚注
参考文献
SMT-LIB: The Satisfiability Modulo Theories Library SMT-COMP: The Satisfiability Modulo Theories Competition Decision procedures - an algorithmic point of view
この記事はもともと、による ACM SIGDA の e-newsletter のコラムから翻案されたものである。原文は こちらで入手可能。
関連項目 解集合プログラミング 自動定理証明 SAT ソルバ 一階述語論理