(10) 集合制約ソルバー
研究代表者:佐藤洋祐 助教授
立命館大学理工学部情報学科
[目次]
- 研究体制
- 2年目の研究内容
- 想定されるソフトウェア成果
氏名 所属
研究代表者 佐藤 洋祐 立命館大学理工学部情報学科助教授
研究協力者 高山 幸秀 立命館大学理工学部情報学科助教授
研究協力者 俣野 正晴 立命館大学理工学部情報学科修士2回生
研究協力者 赤沢 聡 立命館大学理工学部情報学科修士2回生
研究協力者 吉松 宏真 立命館大学理工学部情報学科修士2回生
研究協力者 三橋 元洋 立命館大学理工学部数学科 学部4回生
研究協力者 奈良 隆之 立命館大学理工学部情報学科 学部4回生
研究協力者 吉尾 彰則 立命館大学理工学部情報学科 学部4回生
研究協力者 上野 貴康 立命館大学理工学部情報学科 学部4回生
研究協力者 中村 昌弘 立命館大学理工学部情報学科 学部4回生
体を係数環とする多項式環のイデアルの標準基底であるグレブナ基底は、近
年の計算機代数における金字塔的研究成果の一つであり、Maple、Mathematica
等の商用数式処理システムにおいて、なくてはならない最重要ツールの一つに
なっている。IFSのGDCCおよびCALにおいても、複素数あるいは実数上の制約を
解くために、有理数体を係数環とする多項式環上のグレブナ基底の計算アルゴ
リズムが実装されている。
係数環を一般の環に拡張する試みは多くの研究者によってなされているが、
いずれの場合も整域に限られていた。研究代表者らはICOT在籍中に、係数環が
ブール環(整域ではない)の多項式環(ブール多項式環)においてもグレブナ基底
を拡張できることを示し、そのときのグレブナ基底が様々の性質を持つことを
証明した。これらのうちの大半は、体あるいは整域を係数とする多項式環上の
グレブナ基底には無い性質であり、これらの性質によりブール値に関する制約
を非常にスマートに解くことが可能になる。研究代表者らは、ブール環として
集合ブール環を考えることにより、われわれのグレブナ基底を用いて集合制約
が既存のものとは全く異なった手法で解かれることを明らかにし、そのプロト
タイプをESPで作成した。
IFSのGDCCおよびCALにはブール多項式環上のグレブナ基底が一応実装されて
はいるが、そこで扱えるブール値は基本的には0と1のみであり、係数環は0
と1のみで構成される最も簡単なブール環に限定される。したがって、われわ
れのグレブナ基底に関する研究成果のほんの一部分しか反映されておらず、こ
れを用いて集合制約ソルバーを実現することも、もちろん不可能である。
上に述べたように、ブール多項式環上のグレブナ基底は、独自のM-reduction
を用いること、comprehensive グレブナ基底が容易に構成できること、イデア
ルの拡張定理によって解を容易に扱えること、計算アルゴリズムに独自の
syzygy基底およびS-多項式を用いること等、それまでの体あるいは整域を係数
環にもつ多項式環上のグレブナ基底にはないいろいろな性質を有する。これら
のうちのいくつかはすでに論文等の形で発表されているが、本研究において、
実際に動くソフトウェアとして制作し提供することにより、われわれのグレブ
ナ基底をより多くの人に紹介することを目的とする。
また、グレブナ基底のような計算機代数のテーマにはあまり興味がないけれ
ども、知識処理を実現する上で集合に関する制約を扱う必要がある人にたいし
ても、計算機代数に基づく洗練された集合制約ソルバーを推論エンジンとして
提供することを目的とする。
今年度は、前年度作成したprologのプログラムをもとに、klic版を作成し、
GDCC用の制約解消系も作成する。
- (1)作成されるソフトウェア名称
- Gr\"{o}bner bases and set constraint solvers
- (2)そのソフトウェアの機能/役割/特徴
機能:
- (*) ブール多項式環上のグレブナ基底の計算
扱える係数ブール環は、以下の2種類。
- (i) 集合ブール環
- (ii) 集合ブール環上のブール多項式環
- どちらのグレブナ基底の計算においても、ユーザーは、単項順序として、
辞書式順序と全次数逆辞書式順序、およびそれらを組み合わせたきめの細かい
順序を設定することができる。
また、計算の課程で生成されるS-多項式の数などの内部情報も提供される。
- (**) 集合制約ソルバー
扱える集合制約は以下の言語によって表されるすべての制約
- ・集合変数 扱える変数の数に制限は無い
- ・要素変数 扱える変数の数に制限は無い
- ・要素定数 ユーザーが任意に設定できる、扱える定数の数に制限は無い
- ・集合定数 空集合、全体集合
- ・集合記号 \in、 \notin、 \subseteq、 \cap、 \cup、 ~(補集合)、[、]
- ・等号 =
- ・非等号 \=
- ・論理記号 \wedge
- (***)GDCCの集合制約解消系
役割:
- (*) によってユーザーは、comprehensive グレブナ基底の計算をしたり、
単項順序がグレブナ基底の計算にどのような影響をおよぼすか等の実験を行っ
たりすることが可能になる。
- (**) は さまざまな高度知識処理を実現するために、集合に関する制約を
解くことを必要とするユーザーにたいして、そのための推論エンジンとして、
計算機代数に基づく洗練された集合制約ソルバーを提供する。
- (***) の目的は (**)と同じであるが、それをGDCCの制約解消系として提
供する。
特徴:
- 提案者らがICOT在籍中に研究開発したブール多項式環上のグレブナ基底が
本ソフトウェアの核である。このグレブナ基底はわれわれのオリジナルであり、
従って本ソフトウェアはわれわれ独自のユニークなソルバーを提供する。
- (3)ソフトウェアの構成/構造
グレブナ基底に関する数学的計算の部分と、それらをベースとした集合制約ソ
ルバーの部分、にわけられる。
前者においては、グレブナ基底の計算、イデアルの変数消去、剰余類の代表元
の計算、comprehensive グレブナ基底の計算等を実行するコマンド、および、
このソフトウェアの外部からこれらの計算を利用するためのインターフェース
を用意する。
後者においては、与えられた集合制約にたいし、ユーザーの要望(例えば、ど
の変数について解きたいとか、この変数についての情報は必要ないとかいった
もの)を入力して、解の標準形を出力する形のものと、やはり外部からこのソ
ルバーを利用するためのインターフェースを用意する。さらにこのソルバーを
GDCCの制約解消系としても用意する。
- (4)参考とされたICOTフリーソフトウェアとの関連
GDCCあるいはCALのブール制約ソルバーの、より一般的ソルバーを提供する。
- (5)使用予定言語および動作環境/必要とされるソフトウェア・パッ
ケージ/ポータビリティなど
使用予定言語は klic、動作環境は unix、ソフトウェア・パッケージは利用
しない。
- (6)ソフトウェアの予想サイズ(新規作成分の行数)
klic で約 1000-1500 行、GDCC用制約ソルバーは klic で約500行
- (7)ソフトウェアの利用形態
- このソフトウェアがどういった形で利用されるのか
- 2通りの利用形態が考えられる。
- 一つは、主に計算機代数に興味を持つ利用者によるものである。ユーザー
は2つのブール多項式環(係数ブール環が、集合ブール環および集合ブール環
を係数環とする多項式ブール環)におけるグレブナ基底の計算パッケージが使
用できる。
このパッケージを使ってユーザーは、comprehensiveグレブナ
基底の計算や、イデアルの拡張定理等のわれわれの研究結果について、実際に
実行し確かめることが可能になる。また、きめの細かい単項順序の設定を可能
にしてあり、計算されるS-多項式の数や計算されないですんだ冗長なS-多項式
の数等の、計算内部の詳細情報も利用できるので、ユーザーは、いろいろな単
項順序を用いてグレブナ基底を計算し、それのおよぼす計算への影響について
の実験等をおこなうことも可能になる。
- もう一つは、グレブナ基底のような計算機代数のテーマには、あまり興味
はないのだけれど、高度知識処理の実現のために、集合に関する制約を扱う必
要がある利用者によるものである。本ソフトウェアは、そのための推論エンジ
ンとして、集合制約ソルバーのパッケージを提供する。このソルバーは、上述
のようにわれわれのグレブナ基底に基づいて作られているが、ユーザーが計算
機代数に関する知識を全く持たなくても、このパッケージを使用することが可
能になるように設計される。
- 利用者へのセールスポイント
- ブール多項式環上のグレブナ基底は、われわれのオリジナルであるため、
既存の数式処理システムでは利用することができない。このグレブナ基底がフ
リーソフトウェアとして利用でき、しかも計算の詳細に関する情報も提供され
るので、利用者はブール多項式環の一風変わったグレブナ基底について存分に
楽しむことができる。
- また、計算機代数の知識が全くないユーザーにたいしても、洗練された集
合制約ソルバーを、ブラックボックスとしてだれでも利用できる形で提供する。
- (8)添付予定資料
- ユーザマニュアル、グレブナ基底解説書
www-admin@icot.or.jp