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