------------------------------------------------------------------
             第 362 回 PTT のお知らせ

    ---  Programming Tools and Techniques  ---
------------------------------------------------------------------
■日時: 2010年2月18日(木) 18時30分から
■場所: 情報理工学科会議室
　　　（早稲田大学西早稲田キャンパス６３号館５階０５−０６号室）
        http://www.ueda.info.waseda.ac.jp/location_j.html

＊なお、この４月から理工は「大久保キャンパス」から「西早稲田キャンパス」
　に呼称変更しています（以前は、「西早稲田キャンパス」は本部や大隈講堂な
　どのあるキャンパスを指していたのですが、副都心線の西早稲田駅が理工の
　キャンパスと直結したため）。ご注意下さい。

■話者: 石井 大輔 (早稲田大学理工学術院)
■題目: 非線形算術制約のための区間解析にもとづく求解手法
■概要:
区間に基づく数値計算手法 (精度保証付き数値計算) では、理論解を計算誤差
とともに精度のよい区間で包囲しながら計算を進めていく。
非線形算術制約で記述される問題を区間に基づき求解する手法として、区間制
約プログラミング手法が開発された。これらの手法では、制約伝播にもとづく
探索技法を用い、効率的に精度のよい区間解を求める。
本発表ではまず、区間制約プログラミングにもとづくソルバーであるElisaと、
非線形常微分方程式のためのソルバーであるVNODE-LPを紹介する。その後、代
数方程式と常微分方程式とを連立した問題 (非線形ハイブリッド制約系) を求
解するために、上記ソルバーを統合したHybridSolverについて紹介する。

質疑応答：

Q: 跳ね返る質点の例題で、x方向に空気抵抗がないのは変では？
A: 人工的な例題なので気にしないことにしています。

Q: 「浮動小数点数が演算で閉じている・閉じていない」というのはどういうことか？
A: （境界付近でない限り）計算結果が浮動小数点数になっているか・いないか、
   （丸め誤差が発生するか・しないか）という意味でいっています。

Q: 「記号計算後に区間演算した」とあるが、記号計算の方法はいろいろある
   のでは？
A: 解き方はいろいろあると思います。
   ここでは例として分数の形に解けた、と仮定しています。

Q: ODE求解系VNODEが想定している問題の前提条件はないのか？
A: explicitな形のODEならば何でも入力できます。
   求解の各ステップでbox中に唯一解が存在することを確認しているので、
   その確認に失敗した場合は、エラー終了します。

Q: 制約システムの解釈というのはinterpretationのことか？
A: そうです。数学的な解釈の例を示しています。

Q: 制約伝播手法が近似解法とはどういうことか？
A: 完全に解けた形（solved form、ドメイン中のすべての点が解になっている）
   を計算できるわけではない、という意味です。

Q: Branch-and-Pruneは単調な制約しか扱えないのか？
A: 任意の式で記述された制約を扱えます。
   ただし、Prune処理は単調な関数を用いて記述された制約でないと
   うまく削減できません（例：区間ニュートン法）。

Q: 跳ね返る質点の例題で、かすった場合に大きなboxが得られてしまうのでは？
A: かすった場合には広い領域が解となる場合があるが、
   そのような場合は複数の小さなboxの集合でその領域を包みます。

Q: 提案手法ではどれくらいのサイズの問題を扱えるのか？
A: 定量的な実験はまだ十分おこなっていません。
   現状、非線形ODEの計算に時間がかかってしまっているので、
   とりあえず非線形ODEの効率的求解が課題だと考えています。

Q: SAT求解の組み合わせというのはどのようなことか？
   ハイブリッドシステムを制約で記述しようとすると論理和を用いる必要が
   出てきます。そのようなときに論理和を含んだ制約式から連言制約式を列挙
   するためにSAT求解を利用しています。