SMTソルバ

SMT(satisfiability modulo theories)

充足可能性モジュロ理論？

モジュロはどういう意味なのだろうか

SATソルバではできなかったことができる、より広範囲に適用できるやつ

算術演算

データ構造

ビットベクトル(bit-vectors)

配列

文字列

浮動小数点

etc

SMT LIBのページに対応しているものっぽいのが書かれていた

SMTソルバは、与えられたSMT問題が充足可能(SAT) か充足不能 (UNSAT)かを判定するソフトウェア

いろいろな算術演算や各データ構造を処理するソルバは、理論ソルバと呼ばれる

ソフトウェア

その他のソフトウェアのリストはこっちが詳しそう

SMTソルバの競技ページ

toysolverというSMTソルバの実装例

確認用

Q. SMTソルバ

参考

関連