SATソルバーとソフトウェア検証技術（その5・最終回）
皆さま、こんにちは。
IDAJの小川です。
連載の最終回となる今回は、前回の予告通り、Ansys SCADEのモデル検査を使用して、難解だとされる数独の問題を解いてみましょう。
問題を掲載しておきましたが、実際に取り組まれた方はいらっしゃいますでしょうか？！
Ansys SCADEで、難解な数独にチャレンジ！
数独とは3×3のブロックに均等に分割された9×9のマトリクスのセルに、1~9の数値を以下のルールで入力していくパズルです。
- マトリクスの各行には1~9の数値は1回しか出現しない（必ず1回だけ出現する）
- マトリクスの各列には1~9の数値は1回しか出現しない（必ず1回だけ出現する）
- 3×3のブロックには1~9の数値は1回しか出現しない（必ず1回だけ出現する）
この問題を解いていく方針はこうです。
マトリクスの各行のうち未確定のセルをInput0, Input1, …, Input8の9つの配列で表現し、 上記の3条件を満たす整数（8ビット符号なし整数）の組み合わせを、モデル検査に網羅的に探索させることにします。
このとき、前回の記事のテストケースの生成と同様に、満たして欲しい性質を敢えて否定した性質の反例を探索させることによって、逆にもとの性質を満たす具体例を獲得することを目指します。したがって、モデル検査としてはFalsifiableとなります。
まず、Input0, Input1, … , Input8の各配列が与えられたとして、事前に数字が指定された部分を含めて9×9のマトリックスを構成します。
その後、構成したマトリクスの
- 各行の数字
- 各列の数字
- 3×3の各ブロックの数値
が全て異なるかどうかを判定する論理値を演算します。
詳細は割愛しますが、SCADE言語では配列のような連続するデータを処理する際には、高階オペレータを使用します。今回もmap、foldといった高階オペレータを活用して各配列要素の比較をモデル化しています。
また探索範囲は8ビット符号なし整数全体を対象とする必要はありませんので、assertionによって1~9の範囲に限定しておきます。個数が多くて設定がちょっと大変でしたが、頑張りました。
最後に、上記3つの性質(各行/各列/各ブロックの数値が異なる)の論理積をANDゲートで取得し、さらにその否定(下図の青枠内)を出力するようにして検査モデルの完了です。
この検査モデルに対してモデル検査を実行して反例が得られた場合は、その反例を入力すると3つの性質の論理積がtrue、つまり3つの性質が全て満たされる入力が得られるという算段です。
早速、モデル検査を実行してみましょう。すると、開始早々に無事反例を出力してくれました！
得られた反例の情報を、実際にExcelへ転記して確認してみると、各行、各列、3×3のブロック内の数字の合計が45（1~9の合計）になっており、各行・各列の数字も重複は見られません。
問題なさそうですね。
ということで、無事Ansys SCADEのモデル検査が世界一難しい数独の問題を解いてくれました！
本連載では、SATソルバーから始まり、Ansys SCADEでモデル検査を活用する様々な方法につてご紹介しました。
Ansys SCADEにご興味お持ちいただけましたら、是非弊社（info@idaj.co.jp）までお問い合わせください。
Ansys SCADEに関する詳細については、是非過去のブログ記事もご参照ください。
関連ブログ（記事）
認証取得済みコード生成機能を核とした、組み込みソフトウェアのモデルベース開発環境「AnsysSCADE」 のご紹介（その1）
認証取得済みコード生成機能を核とした、組み込みソフトウェアのモデルベース開発環境「Ansys SCADE」 のご紹介（その2）
認証取得済みコード生成機能を核とした、組み込みソフトウェアのモデルベース開発環境「Ansys SCADE」 のご紹介（その3）
無料オンラインセミナー（Webinar）
弊社では、Ansys SCADEにご興味のあるお客様を対象に、常設で下記のオンラインセミナーを開催しています。
「開発責任者・管理職・シニアエンジニア様向けAnsys SCADEご紹介セミナー」
本セミナーでは、普段、Ansys SCADEを操作されることはなくても、組み込みソフトウェア開発を統括・推進されている開発責任者・管理職・シニアエンジニアの皆様に、Ansys SCADEがどのようなシーンでお役に立つのかをわかりやすくご説明しています。IDAJは単にソフトウェアのご提供だけでなく、機能安全規格に準拠した開発プロセスへのツール適用や効率的なモデルの作成などをコンサルティングサービスとしてご提供します。ぜひご都合の良い時間にご視聴いただければ幸いです。
■オンラインでの技術相談、お打合せ、技術サポートなどを承っています。下記までお気軽にお問い合わせください。ご連絡をお待ちしています。
株式会社 IDAJ 営業部
Webからのお問い合わせはこちら
E-mail：info@idaj.co.jp
TEL： 045-683-1990