平成7年度 委託研究ソフトウェアの提案

(13) 集合制約ソルバー

研究代表者:佐藤 洋祐 助教授
      立命館大学 理工学部 情報学科




[目次]

  1. 研究の背景
  2. 研究の目的
  3. 研究の内容
  4. ソフトウェア成果


[研究の背景]

体を係数環とする多項式環のイデアルの標準基底であるグレブナ基底は、近 年の計算機代数における金字塔的研究成果の一つであり、Maple、Mathematica 等の商用数式処理システムにおいて、なくてはならない最重要ツールの一つに なっている。IFSのGDCCおよびCALにおいても、複素数あるいは実数上の制約を 解くために、有理数体を係数環とする多項式環上のグレブナ基底の計算アルゴ リズムが実装されている。

係数環を一般の環に拡張する試みは多くの研究者によってなされているが、 いずれの場合も整域に限られていた。提案者らはICOT在籍中に、係数環がブー ル環(整域ではない)の多項式環(ブール多項式環)においてもグレブナ基底を拡 張できることを示し、そのときのグレブナ基底が様々の性質を持つことを証明 した。これらのうちの大半は、体あるいは整域を係数とする多項式環上のグレ ブナ基底には無い性質であり、これらの性質によりブール値に関する制約を非 常にスマートに解くことが可能になる。提案者らは、ブール環として集合ブー ル環を考えることにより、われわれのグレブナ基底を用いて集合制約が既存の ものとは全く異なった手法で解かれることを明らかにし、そのプロトタイプを ESPで作成した。

IFSのGDCCおよびCALにはブール多項式環上のグレブナ基底が一応実装されて はいるが、そこで扱えるブール値は基本的には0と1のみであり、係数環は0 と1のみで構成される最も簡単なブール環に限定される。したがって、われわ れのグレブナ基底に関する研究成果のほんの一部分しか反映されておらず、こ れを用いて集合制約ソルバーを実現することも、もちろん不可能である。


[研究の目的]

上に述べたように、ブール多項式環上のグレブナ基底は、独自のM-reduction を用いること、comprehensive グレブナ基底が容易に構成できること、イデア ルの拡張定理によって解を容易に扱えること、計算アルゴリズムに独自の syzygy基底およびS-多項式を用いること等、それまでの体あるいは整域を係数 環にもつ多項式環上のグレブナ基底にはないいろいろな性質を有する。これら のうちのいくつかはすでに論文等の形で発表されているが、本研究において、 実際に動くソフトウェアとして制作し提供することにより、われわれのグレブ ナ基底をより多くの人に紹介することを目的とする。

さらに、グレブナ基底のような計算機代数のテーマにはあまり興味がないけ れども、知識処理を実現する上で集合に関する制約を扱う必要がある人にたい しても、計算機代数に基づく洗練された集合制約ソルバーを推論エンジンとし て提供することを目的とする。


[研究の内容]

上述のように、提案者は、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 、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 君

が得られる。


[ソフトウェア成果]

(1)作成されるソフトウェア名称
Groebner bases and set constraint solvers

(2)そのソフトウェアの機能/役割/特徴
機能:
(*) ブール多項式環上のグレブナ基底の計算
扱える係数ブール環は、以下の2種類。
(i) 集合ブール環
(ii) 集合ブール環上のブール多項式環
どちらのグレブナ基底の計算においても、ユーザーは、単項順序として、 辞書式順序と全次数逆辞書式順序、およびそれらを組み合わせたきめの細かい 順序を設定することができる。また、計算の課程で生成されるS-多項式の数な どの内部情報も提供される。

(**) 集合制約ソルバー
扱える集合制約は以下の言語によって表されるすべての制約
集合変数 扱える変数の数に制限は無い
要素変数 扱える変数の数に制限は無い
要素定数 ユーザーが任意に設定できる、扱える定数の数に制限は無い
集合定数 空集合、全体集合
集合記号 、 ~(補集合)、{、 }
等号 =
論理記号

役割: (*) によってユーザーは、comprehensive グレブナ基底の計算をした り、単項順序がグレブナ基底の計算にどのような影響をおよぼすか等の実験を 行ったりすることが可能になる。

(**) は さまざまな高度知識処理を実現するために、集合に関する制約を解く ことを必要とするユーザーにたいして、そのための推論エンジンとして、計算 機代数に基づく洗練された集合制約ソルバーを提供する。

特徴: 提案者らがICOT在籍中に研究開発したブール多項式環上のグレブナ基 底が本ソフトウェアの核である。このグレブナ基底はわれわれのオリジナルで あり、従って本ソフトウェアはわれわれ独自のユニークなソルバーを提供する。



www-admin@icot.or.jp