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