平成7年度 委託研究ソフトウェアの提案 |
係数環を一般の環に拡張する試みは多くの研究者によってなされているが、 いずれの場合も整域に限られていた。提案者らはICOT在籍中に、係数環がブー ル環(整域ではない)の多項式環(ブール多項式環)においてもグレブナ基底を拡 張できることを示し、そのときのグレブナ基底が様々の性質を持つことを証明 した。これらのうちの大半は、体あるいは整域を係数とする多項式環上のグレ ブナ基底には無い性質であり、これらの性質によりブール値に関する制約を非 常にスマートに解くことが可能になる。提案者らは、ブール環として集合ブー ル環を考えることにより、われわれのグレブナ基底を用いて集合制約が既存の ものとは全く異なった手法で解かれることを明らかにし、そのプロトタイプを ESPで作成した。
IFSのGDCCおよびCALにはブール多項式環上のグレブナ基底が一応実装されて はいるが、そこで扱えるブール値は基本的には0と1のみであり、係数環は0 と1のみで構成される最も簡単なブール環に限定される。したがって、われわ れのグレブナ基底に関する研究成果のほんの一部分しか反映されておらず、こ れを用いて集合制約ソルバーを実現することも、もちろん不可能である。
さらに、グレブナ基底のような計算機代数のテーマにはあまり興味がないけ れども、知識処理を実現する上で集合に関する制約を扱う必要がある人にたい しても、計算機代数に基づく洗練された集合制約ソルバーを推論エンジンとし て提供することを目的とする。
以下に、集合制約の解法の簡単な例をあげ、この例を通じて具体的にどうい うことをやりたいのか述べる。
(例)集合制約の解法
学生の就職問題を考える。うちの研究室では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 、s4 君 は柔道部とトライアスロン部の両方に所属している。s3 君はフットボール部 のみに所属している。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 を用 いて上の制約は、以下のように方程式として表される。
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,s4}/\J/\F={s1,s2,s4},{s1,s2,s4}/\(T\/K)=0, {s3}/\F={s3},{s3}/\(J\/T\/K)=0,{s9}/\F/\T={s9},{s9}/\(J\/K)=0,{s10}/\T={s10}, {s10}/\(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}, {s1,s2,s3,s4,s5,s6,s7,s8,s9,s10}/\(A\/B\/C\/D)={s1,s2,s3,s4,s5,s6,s7,s8,s9,s10}
ここで、/\は集合の積、\/は集合の和、0は空集合を表す。われわれのソルバー を使ってこれを自動的に解くことは可能である。しかしながら現状のプロトタ イプのソルバーでは、まずcomprehensive グレブナ基底を計算しそれをユーザー が編集して再びグレブナ基底を計算するという方法で解かれる。これではソル バーの中身に精通していないユーザーには使いものにならない。この点を解消 するために、これら一連の計算をブラックボックスとして提供するプログラム を作成することが、本研究の重要な目的の一つになる。ちなみに、 comprehensive グレブナ基底の計算は、現時点でのプロトタイプでは、東芝ワー クステーションAS4080を用いて3分弱で完了し、(この後のグレブナ基底の計算 は数秒でおわる)上の解の1つとして、
A社には s2、s3、s4、s7、s8 君、
B社には s9 君、
C社には s1、s6、s10 君、
D社には s5 君
が得られる。
集合変数 | 扱える変数の数に制限は無い | |
要素変数 | 扱える変数の数に制限は無い | |
要素定数 | ユーザーが任意に設定できる、扱える定数の数に制限は無い | |
集合定数 | 空集合、全体集合 | |
集合記号 | 、 、 、 、 、 ~(補集合)、{、 } | |
等号 | = | |
論理記号 | 、 、 |
役割: | (*) によってユーザーは、comprehensive グレブナ基底の計算をした
り、単項順序がグレブナ基底の計算にどのような影響をおよぼすか等の実験を
行ったりすることが可能になる。 (**) は さまざまな高度知識処理を実現するために、集合に関する制約を解く ことを必要とするユーザーにたいして、そのための推論エンジンとして、計算 機代数に基づく洗練された集合制約ソルバーを提供する。 |
特徴: | 提案者らがICOT在籍中に研究開発したブール多項式環上のグレブナ基 底が本ソフトウェアの核である。このグレブナ基底はわれわれのオリジナルで あり、従って本ソフトウェアはわれわれ独自のユニークなソルバーを提供する。 |
www-admin@icot.or.jp