上述のように、提案者は、ICOT在籍中に、ブール多項式環上のグレブナ基底とそれを 用いた集合制約ソルバーを、ESPによって作成した。 その後、提案者はこれをsicstus prologに翻訳して、学生の卒業研究等に利用している。 しかしながら、このプログラムはあくまでもプロトタイプであって、利用できるのは 核となる生のソルバーのみであるため、フリーソフトウェアとして公開できるような ソフトウェアにはなっていない。 今回の委託研究では、このプロトタイプを土台として、特に集合制約ソルバーをユーザ ーインターフェースの部分を中心にしっかりしたものとして制作し、使い安いソフトウ ェアとして提供することを目的の一つとする。 以下に、集合制約の解法の簡単な例をあげ、この例を通じて具体的にどういうことを やりたいのか述べる。
(例)集合制約の解法
学生の就職問題を考える。うちの研究室では10人の学生が来年度卒業予定である。 名前を書くと長くなるので、s1、s2、s3、s4、s5、s6、s7、s8、s9、s10 君とする。 彼らは勉強しているテーマによって、TRS(term rewriting system)、CA(computer algebra)、G(graphics)、OS(operating system) の4つのグループにわけられる。 彼らの内の何人かは大学のクラブに所属していて、それは J(柔道部)、F(フットボール部)、 T(トライアスロン部)、K(空手部) のいずれかである。 さて、うちの研究室に4つの企業(これも名前を書くと長くなるので、A社、B社、C社、D社 とする)から求人の募集があった。それぞれの企業の要求は以下の通りである。 A社はトライアスロンをやっている学生が気にいっていて2人欲しいが、柔道や空手のよう な野蛮なスポーツをする学生はいらないといっている。 B社はoperating systemを勉強している学生を1人欲しいが、柔道部の学生はいらない。 C社はgraphicsを勉強している学生が気にいっていて1人欲しいが、他に条件は出して いない。 D社はクラブ活動などしている学生はいらないと言っていて、term rewriting system か computer algebra を勉強している理論に強い学生を1人ほしいといっている。 各学生の勉強テーマと所属するクラブは以下の通りである。 TRS: s1、s2 君の2人、CA: s3、s4、s5 君の3人、G: s6、s7、s8 君の3人、OS: s9、s10 君 の2人。 s1、s2 君は柔道部とトライアスロン部の両方に所属している。s3 君はフットボール 部のみ、s4 君は柔道部のみ に所属している。s9 君はフットボール部とトライアスロン部の両方に所属している。 s10 君はトライアスロン部のみに所属している。その他の諸君はどのクラブにも所属して いない。 このとき、学生を全員就職させることは可能か？もし可能ならばどのような状態になるのか？ について、考えてみる。 これは、集合制約の解法とみなすことができる。 集合変数として、TRS、CA、G、OS、A、B、C、D、J、F、T、K (この変数はそれぞれに属する 人の名前の集合を表す)、要素定数(ここでは学生の名前を表す)としてs1、s2、s3、s4、s5、 s6、s7、s8、s9、s10、要素変数(学生の名前を表す変数)として x1、x2、x3、x4、x5 を用いて 上の制約は、以下のように方程式として表される。
ここで、
は集合の積、
は集合の和、0 は空集合を表す。
われわれのソルバーを使ってこれを自動的に解くことは可能である。しかしながら現状の
プロトタイプのソルバーでは、まずcomprehensive グレブナ基底を計算しそれをユーザー
が編集して再びグレブナ基底を計算するという方法で解かれる。これではソルバーの中身
に精通していないユーザーには使いものにならない。この点を解消するために、これら一連
の計算をブラックボックスとして提供するプログラムを作成することが、本研究の重要な
目的の一つになる。
ちなみに、comprehensive グレブナ基底の計算は、現時点でのプロトタイプでは、東芝ワー
クステーションAS4080を用いて3分弱で完了し、(この後のグレブナ基底の計算は数秒でおわ
る)上の解の1つとして、
A社には s4、s10 君、 B社には s3、s9 君、 C社には s1、s2、s6 君、 D社には s5、s7、s8 君 が得られる。