next up previous
Up: 「集合制約ソルバー」 に関する成果概要 Previous: 研究の内容

研究の成果

(1) 研究上の成果

通常の体を係数環とする多項式環におけるグレブナ基底の計算において単項順 序のおよぼす影響はきわめて大きいことが知られている。一般に全次数逆辞書 式順序が、計算時間及び計算領域ともに一番小さくなり、一番便利な純辞書式 順序が計算時間及び計算領域ともに一番大きくなる傾向がある。これに対し、 ブール多項式環におけるグレブナ基底の計算においては、逆の傾向すなわち、 一番便利な純辞書式順序が計算時間及び計算領域ともに一番小さくなる傾向が あることが、われわれのおこなった計算実験から判明した。おそらくブール多 項式環における多項式が各変数にたいして次数が高々1までしかないのが主要 な原因と思われる。この点について理論的に解明するのはこれからの課題であ る。また、一番便利な純辞書式順序が一般に一番簡単に求められるので、同次 化の手法が計算の高速化に有効なことが予想される。これに関しても計算実験 をおこなって検討することが望まれる。

(2) ソフトウェアとしての成果

集合制約ソルバーのソフトウェアは図 1のように5つのプログラム群で構成さ れる。ユーザは解きたい集合制約を入力する。この集合制約は変換プログラム によって集合ブール環上のブール多項式環を係数ブール環とするブール多項式 環(以下BR1と記すことにする)のいくつかの多項式に変換される。これは主要 エンジン部に渡され、これが生成するイデアルのグレブナ基底(BR1における) が計算される。計算されたグレブナ基底の定数部(BR1における)を用いて要素 変数を解くため、この部分は主要エンジン部のもう一つのソルバーに引き渡さ れる。ここでは、これの集合ブール環を係数ブール環とするブール多項式環 (以下BR2と記すことにする)におけるグレブナ基底を計算する。計算されたグ レブナ基底はさらに要素変数ソルバーへと渡される。ここで各要素変数につい て解かれ、その値を前に求めておいたBR1におけるグレブナ基底へ代入する。 BR1におけるグレブナ基底は、基本的にはBR2におけるcomprehensiveグレブナ 基底なので、代入した結果はBR2におけるグレブナ基底になっている。この結 果を用いて解生成プログラムでは、解きたい集合変数について整理して、その 結果を一般解として出力する。

図 1. 集合制約ソルバーのソフトウェア構成



以上が集合制約ソルバーのソフトウェア構成の概要である。現時点では、変換 プログラム、主要エンジン部が完成している。要素変数ソルバーについては、 解生成プログラムに渡すために一般解をどのような形で表現するかが重要かつ 難解な問題であり、今だに完成していない。いろいろな集合制約を解いてみた 結果、ここを本当に自動化するよりも、いったんユーザーに引渡し、(引き渡 される出力から要素変数についての(特殊)解は容易に得ることができる)ユー ザーが特殊解をここで入力するといったインタラクティブなやり方のほうがよ いという結論に達し、この方向でシステムを開発中である。

主要エンジン部の二つのソルバーは、それぞれ単独でユーザーが使えるように もなっている。これを用いて、ユーザーはわれわれが開発した一風変わったグ レブナ基底についての数学的実験(グレブナ基底およびcmprehensiveグレブナ 基底の計算、イデアルの変数消去、剰余類の代表元の計算等)を楽しむことが できる。

(3) 残された課題

上述のように、要素変数ソルバーが理論的にもソフトにおいても今だ未完成で ある。この部分のさらなる検討が必要である。また(これは2年目以降の課題 であるが)GDCCのような制約論理型言語の制約ソルバーとして使うためには、 どのような形態のソルバーにしていくかも重要な課題である。

(4) 自己評価

ソルバーに用いたグレブナ基底は、われわれのオリジナルであり、世界でも例 のないユニークなソフトウェア(いいソフトウェアかどうかは別にして)になっ ていると確信する。



www-admin@icot.or.jp