日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

SMT ソルバーを用いたパラメータ自動求解システムの開発
冨田 空

安藤 崇央

システムには正常に動作するため，許される入出力パラメータの範囲が限られているものがある．それらのシステムの安全性を確保するため，システムが持つ潜在的な入出力パラメータの範囲が許される入出力範囲とどのような関係にあるのか検査することが必要である．また，SMT ソルバーとは，SAT 問題 (satisﬁability problem) を解く
SAT ソルバーと専用の理論ソルバーを組み合わせたソルバーで，SAT ソルバーが苦手としているデータ構造や算術演算に関する問題などを網羅的に解くことができる．本研究では，SMT ソルバーのこの様な特徴を生かして，システムの許される入出力許可範囲を確認する検査を，自動的に行うシステムの開発を行った．本システムは，パラメータの求解エンジンとして，SMT ソルバーを利用し，全体の境界条件等を解析的ではなく網羅的に探索する手法をとっている．SMT ソルバーから得られる解は，すべてシステムの条件を満たすパラメータの値割り当てとなっている．また，本システムは，SMT ソルバーから得られた解を 2 次元および 3 次元のグラフとして出力する機能を持つ．この機能によりパラメータの許される範囲を直感的に観察することが可能となっている．

さらには，実数や未解釈関数などの背景論理を組み合1 はじめにわせて記述できるため，表現の幅も広い．そのため，現在，自動運転をはじめとした，多くの技術の開発プログラム検証をはじめとしたさまざまな分野で扱が進められている．それらのシステムが世の中に浸透われている．

することで人々の生活を豊かにすることができるが，そのためにはシステムの安全性を確保することが非2 研究目的常に重要である．システムには正常に動作するため，

本研究では，与えられた条件下で入出力パラメータ許される入出力パラメータの範囲が限られているもの許可範囲について自動で確認を行うシステムの提のがある．一般にシステムの入力と出力は，その設計案を行う．

やさまざまな外部環境などの複雑な条件下では関連

SMT ソルバーは，条件を満たす解が存在するか網付けられている．近年，システムの開発は大規模化，羅的に探索することができる．本システムでは入力し複雑化しているため，正しく入力と出力の許可範囲がた条件を満たす解を SMT ソルバーが出力し，その解設定されているか確認することはますます難しくなっの分布をグラフ上で確認できるようにすることを目ている．

的とした．

近年，SAT ソルバーや SMT ソルバーの性能の向上に伴い，それらを他分野に応用する研究が急速に3 要素技術進められている．SMT ソルバーは，SAT ソルバーよ3. 1 SAT ソルバー

りも，元の記述を保ったまま表現することができる．

SAT 問題 (satisﬁability problem) とは命題論理式が与えられたときに，それを真にすることができる真Development of Automatic Parameter Solving System
Using SMT Solver.
Sora Tomita, Takahiro Ando, 群馬大学大学院理工学府,
Dept. of Science and Technology, Gunma University.

偽値の割り当てが存在するかを決定する問題（充足可能性問題）のことで，NP 完全問題の 1 つである．

SAT ソルバーは与えられた充足可能性問題が充足可能かどうかを判定するプログラムで，充足可能であればその値割り当ての一例も出力する [8]．

SAT ソルバーには連言標準形 (Conjunctive normal

図1

システムの構成form, CNF) の論理式を入力として与える．CNF の論理式は 1 つ以上のリテラルが論理和により結合さ

代 表 的 な SMT ソ ル バ ー に は Z3 [3]，CVC4 [1]，れた節を持ち，それらの節が論理積により結合された

yices [4] などがある．本研究では Microsoft Research形式の論理式である．以下に例を示す．

によって開発された Z3 という SMT ソルバーを用いて研究を行った．

(x1 ∨ x2 ) ∧ (¬x1 ∨ x3 ) ∧ (x2 ∨ ¬x3 ) ∧ ¬x3(1)

CNF の論理式 (1) を SAT ソルバーに入力として与4 パラメータ自動求解システムえると，SAT ソルバーは式 (1) が充足可能であると

4. 1 システム構成判定し，(1) を真とする値割り当てとして，x1 と x3システムの構成は図 1 のようになっており，SMTが偽，x2 が真を出力する．実際，この値割り当てをソルバーに条件を与え，1 つの解が得られるたびに，(1) に代入すると，(1) は真となる．

得られたデータは CSV ファイルへ出力する．条件を(x1 ∨ x2 ) ∧ (¬x1 ∨ ¬x3 ) ∧ (x2 ∨ ¬x3 )∧(x1 ∨ ¬x3 ) ∧ x3

満たすデータがすべて得られると，matplotlib を用(2)

いて CSV 上のデータからグラフを表示する．

また論理式 (2) を SAT ソルバーに入力すると SAT

SMT ソルバー 与えられた条件を満たす解を 1 つソルバーは充足不能であると判定する．実際に論理式出力．これを条件を満たす解がなくなるまで繰り(2) は，可能などんな値割り当てを代入しても，真と返す．

はならない．SAT ソルバーは，可能な値割り当てについて入力の論理式を真とするか，網羅的に確認を行い充足可能性問題を解いている．代表的な SAT ソ
ルバーには miniSAT [5]，picoSAT [2]，SAT4J [6] なCSV 得られたデータは CSV ファイルに保存される．

matplotlib 解をすべて求めることができたら，データからグラフを作成し出力する．

どがある．また，SAT ソルバーは，3.2 節で紹介する，SMT ソルバーの内部エンジンとしても利用され4. 2 すべての解を求めるている．

通常，SMT ソルバーは与えられた一階述語論理式に対して，それを真にするような値割り当てが存在し3. 2 SMT ソルバーていれば値割り当てを出力する．ただし，複数の割りSAT ソルバーが命題論理を扱うことに対して，SMT当てが存在している場合であっても，その中の 1 つソルバーは量化子を除いた一階述語論理を扱う．SMTの割り当てしか出力されない．そのため，すべての解は Satisﬁability Modulo Theories（背景理論付き充を知りたい場合は，複数回 SMT ソルバーを実行し，足可能性問題）の略であり，SMT 問題は SAT 問題

1 つずつ別の解を得る必要がある．ただし，同じ実行のように決まった問題の名前を表しているわけではな

条件では何度やっても同じ割り当てで出力される．そい．SMT は SAT を拡張した技術や研究分野と考えのため，SMT ソルバーの元の入力に，出力された解たほうが良い．

に関する条件を追加し，別の解の出力を促すようにす

SAT ソルバーはデータ構造や算術・比較演算に関る．以下に例を示す．

する問題を扱う場合，入力規模が大きくなりすぎてし

x × y = 12,まう．一方，SMT ソルバーは表現の幅が広く，問題この条件を満たす値割り当てが x = 1, y = 12 となっを簡潔に記述できるため，このような問題を扱うのにた場合，(x ̸= 1) ∨ (y ̸= 12) という条件を追加すれば適している．

よい．これは，SMT ソルバーの出力する解の候補か

x > 0,y>0(x, y は整数である)

ら (x = 1) ∧ (y = 12) を除くことを意味する．次に

x = 12, y = 1 となった場合，(x ̸= 12) ∨ (y ̸= 1) という条件をさらに追加する．これを繰り返すことです
べての解を求めることができる．ただし，以下に示す
ように，追加した条件同士の関係は論理積であることに注意する．

(x × y = 12) ∧ (x > 0) ∧ (y > 0)() ()∧ (x ̸= 1) ∨ (y ̸= 12) ∧ (x ̸= 12) ∨ (y ̸= 1)
4. 3 実数に対して整数変数を用いる場合は，すべての解を求めることができるが，実数変数を用いる場合は，すべての解を

図2x, y の散布図求めることはできない．そのため，追加する条件を変更した．以下に例を示す．

x × y = 12,x > 0,y>0(x, y は実数である)

まず，x と y の上限を決める必要がある．上限がないと 0 以上であればどんなに大きな数でも解になりえるからである．今回は x ≤ 12,y ≤ 12 とする．

次に，この条件を満たす値割り当てが x = 1, y = 12となった場合，整数の時のように (x ̸= 1) ∨ (y ̸= 12)という条件を追加するのではなく，以下のような条件を追加する．
() ()(x < 0) ∨ (2 ≤ x) ∨ (y < 11) ∨ (13 ≤ y)
このような条件を追加することで，x, y がそれぞれ(0 ≤ x < 2), (11 ≤ y < 13) の範囲の数値を，同時に図3

条件を変更した場合の x, y の散布図解として出力しなくなる．2 つ目の解を探索する際にSMT ソルバーに入力される論理式は，まとめると以下のようになる．

(x × y = 12) ∧ (0 < x ≤ 12) ∧ (0 < y ≤ 12)() ()∧ (x < 0) ∨ (2 ≤ x) ∨ (y < 11) ∨ (13 ≤ y)
条件の追加を繰り返すことで，実数変数を用いる場合
でも，決められた範囲内で一定区間ごとの解を探すこ() ()63, 8,, (6, 2),(x, y) = (1, 12), (12, 1), 10,() ( 5)2307 2640
27 40,,,,(4, 3), (2, 6),220 307() ( 10 9 ) ()123684 2947
1842 3254,7 ,,,,72947 307
1627 307
また，追加する条件を以下のように変更した場合の本システムで得られる解は以下のようになり，これ散布図を図 3 に示す．
() ()(x < 0.9) ∨ (1.1 ≤ x) ∨ (y < 11.9) ∨ (12.1 ≤ y)

を x, y 平面上の散布図のグラフとしたものを図 2 に

このように，条件によって出力される値の密度を調整示す．

することができる．とができる．

4. 4 3D グラフの表示
本システムでは 3D グラフを表示することも可能で重み付けをして平均を取って予測値とする．以下に手順を示す．

dy= f (x, y)dx
1. 点 (xi , yi ) の f (xi , yi ) を計算して，傾きとする．
xi から xi+1 へ変化すると k1 は
k1 = hf (xi , yi )2. 次に x = xi + h2 ，y = yi + k21 での傾きを，
f (xi + h2 , yi + k21 ) とする．点 (xi , yi ) から線を引いた時の増加量 k(2 は)h
k1, yi +22
3. 次に x = xi + h2 ，y = yi + k22 での傾きを，
k2 = hf

xi +f (xi + h2 , yi + k22 ) とする．点 (xi , yi ) から線を引いた時の増加量 k(3 は図4)
k2h, yi +22
4. 次に x = xi + h，y = yi + k3 での傾きを，
k3 = hf

P, V, T の散布図

xi +f (xi + h, yi + k3 ) とする．点 (xi , yi ) から線を引いた時の増加量 k4 はk2 = hf (xi + h, yi + k3 )5. k1 : k2 : k3 : k4 = 1 : 2 : 2 : 1 の重みをつけて平均し，点 (xi , yi ) から x 方向に h 進んだ時の yの変化量を求め，yi+1 を決定する．
1
yi+1 = yi + (k1 + 2k2 + 2k3 + k4 )6
SMT ソルバーへ追加する条件は，実数の時と同様である．以下に例を示す．図 6 は解の散布図である．
dve−v=, c = 0.001, 95 ≤ r, r ≤ 100, e = 10,dt
rct は 0 から 1 の区間で 100 分割する．
図5

別角度からの P, V, T の散布図

r の値が途中で下がってきているが，おおよその概形を確認することができる．

ある．以下のような条件を例として用いる．

P × V = n × R × T,200000 ≤ P,

R = 8300,

P ≤ 300000,

n = 0.05,0.3 ≤ V, V ≤ 0.5,

(P, V, n, R, T は整数である)5 まとめ
本研究では SMT ソルバーを用いて，パラメータを自動で求めるシステムの開発を行った．このシステム

このような条件から得られる解を用いて，図 4 のよは，SMT ソルバーによって与えられた条件を満たすうな 3D グラフを表示することができる．この 3D グ

パラメータを網羅的に求めることができ，得られた

ラフは図 5 のように好きな角度でグラフを観察する

解は CSV ファイルに保存される．また，matplotlibことができる．

によって，CSV 上のデータからグラフを作成し描画することで，値の分布を直感的に観察することがで

4. 5 微分方程式

きる．加えて，追加する条件によって実数を扱うこと

微分方程式の条件に対しては，ルンゲ=クッタ法 [7]や，値の密度を調整することができる．

を用いる．ルンゲ=クッタ法は，4 種類の傾きを求め，と同様の方法で一定区間ごとの解を求めた．
一方で，与えられた条件内から選ばれる数値がばらついてしまい，想定していない間隔が値同士に生じてしまった．今後はこれらを課題とし，実用的な条件を用いてのパラメータ求解について研究していきたい．
また，パラメトリック図で表現された制約を直接入力するようなシステムについても考えていきたい．

参 考 文 献図6v, t, r の散布図

SMT ソルバーで網羅的に解を求めるには以下のような方法を実装した．

1. 値が整数の範囲の場合，条件を満たす値割り当てを 1 組出力した後，その否定を条件としてSMT ソルバーに追加する．このようにすること
で 1 度出力した値を SMT ソルバーの解の候補から除き，別の解を出力するようにした．

2. 値が実数の範囲の場合，条件を満たす値割り当てを 1 組出力した後，それぞれの解の付近の数値を同時に解として出力しないような条件を追加することで，一定区間ごとの解を探すようにした．

3. 微分方程式の条件に対しては，ルンゲ=クッタ法という数値解法を用いることにより，実数の時[1] Barrett, C., Conway, C. L., Deters, M., Hadarean,L., Jovanović, D., King, T., Reynolds, A.,
and Tinelli, C.: Cvc4, International Conference
on Computer Aided Veriﬁcation, Springer, 2011,pp. 171–177.
[2] Biere, A.: PicoSAT essentials, Journal on Satisﬁability, Boolean Modeling and Computation, Vol. 4,
No. 2-4(2008), pp. 75–97.
[3] de Moura, L. and Bjørner, N.: Z3: An Eﬃcient
SMT Solver, Tools and Algorithms for the Construction and Analysis of Systems, Ramakrishnan,
C. R. and Rehof, J.(eds.), 2008, pp. 337–340.
[4] Dutertre, B.: Yices 2.2, International Conference
on Computer Aided Veriﬁcation, Springer, 2014,
pp. 737–744.
[5] Eén, N. and Sörensson, N.: An extensible SATsolver, International conference on theory and applications of satisﬁability testing, Springer, 2003,
pp. 502–518.
[6] Le Berre, D. and Parrain, A.: The Sat4j library, release 2.2, Journal on Satisﬁability, Boolean
Modeling and Computation, Vol. 7, No. 2-3(2010),
pp. 59–64.
[7] 三井斌友: Runge-Kutta 法-その過去, 現在, 未来,総合講演・企画特別講演アブストラクト, Vol. 1998,No. Spring-Meeting(1998), pp. 93–101.
[8] 梅村晃広: SAT ソルバ・SMT ソルバの技術と応用, コンピュータ ソフトウェア, Vol. 27, No. 3(2010),
pp. 3 24–3 35.