多くのSMTソルバが対応するSMT2形式の記述方法を説明します。

SMTソルバーとは

SMT(Satisfaction Modulo Theory)ソルバとは与えられた複数の制約式の充足可否や、 充足可能時の値の組み合わせを求める事が出来るソフトウェアです。 この分野には先行してSATソルバというものがあり、こちらは全量演算子∀などが扱えないという条件があります。 SMTソルバではこのような条件はなくほとんどすべての論理制約を解析可能であると同時に、ビット幅のある変数の宣言などを直接記述できるなど使い勝手が向上しています。個人的には、多様な変数名を設定できることはとても便利です。

SATソルバは数十万変数から数百万変数の制約式が解析可能と言われていますが、SMTソルバは高機能故にそこまでのスケーラビリティを実現出来ていません。大きな問題を解く場合にはSATソルバをうまく活用する事を考える必要があるけれど、それほど大きな問題を解かないのであればSMTソルバの活用を考えるべきでしょう。

このポストでは、今までSATソルバで記述できていたような制約式(CNF式、DIMACS形式など)を、SMT2式で書く方法について説明します。

変数の宣言

まずは変数の宣言を行います。例えば1bit変数aは以下のようにして宣言します。

( declare-fun a () Bool )

制約の追加

必要な変数を宣言し終わったら、制約を追加することができます。例えば変数bが変数aの否定である場合(b != a)は以下のように制約を記述します。

( assert (=  (not a) b) )

##例） 2入力AND回路の出力が1になるかどうかの検査 2入力ANDの出力が1になるのは、両方の入力が1になる時です。「1になるかどうか」という命題は真ですので、その旨を出力させたいです。

( declare-fun in0 () Bool )
( declare-fun in1 () Bool )
( declare-fun out () Bool )
( assert (= out (and in0 in1) ) )
( assert (= out true) )
( check-sat )

これをSMTソルバに入力すると以下のように出力するはずです。今回はZ3というSMTソルバを使います。

$ z3 -smt2 test1.stm2
sat

“sat”と表示されました。できれば、どのようなときに1になるかも出力させたいので、それもやってみます。

SATの場合に値の割り当てを見たい場合には、get-valueを用います。以下のようになるはずです。

( declare-fun in0 () Bool )
( declare-fun in1 () Bool )
( declare-fun out () Bool )
( assert (= out (and in0 in1) ) )
( assert (= out true) )
( check-sat )
( get-value (in0) )
( get-valule (in1) )

では、実行してみましょう。

$ z3 -smt2 test2.stm2
sat
((in0 true))
((in1 true))

まだまだあるSMT2形式の言語仕様

SMT2式の書き方についてはPDFにまとまっている言語仕様を参照すると良いでしょう。 http://smtlib.cs.uiowa.edu/

SMTソルバによってはPythonAPIなどを提供していることもあるので、それを利用して実装を簡単にすることもできます。