(10) 集合制約ソルバー

1. 研究テーマ、研究代表者：

   （１）研究テーマ

   「集合制約ソルバー」

   （２）研究代表者（氏名、所属、役職）

   佐藤洋祐　立命館大学理工学部情報学科助教授

2. 記述項目：

   (１) 研究進捗状況

   集合制約ソルバーの主要エンジン部にあたる、集合ブール環を係数ブールとす るブール多項式環上のグレブナ基底、及び、集合ブール環上のブール多項式環 を係数ブールとするブール多項式環上のグレブナ基底を求めるKLICプログラム が一応完成した。GDCCに必要な集合制約機能については、引続き検討中である。

   (２) 現在までの主な成果

   ブール環上のブール多項式環におけるグレブナ基底の従来の正規形を用いた集 合制約ソルバーにおいて、要素変数の制約がかなり複雑になることが、前年度 の試作で判明したため、今年度は、以前研究者が理論的に考案していた、別の 正規形を用いるようグレブナー基底を改良した。

   これにより、集合制約の解法の途中で一端ユーザーに渡される、要素変数の制 約が、かなり見易くなるものと思われる。

   (３) 今後の研究概要

   集合制約ソルバーをGDCCにどのように組み込むかは、最重要課題の一つであり、 また理論的にも実装面においても難しい課題である。これが、今後の最重要か つ最難関テーマである。要素変数ソルバーはprolog版では、ユーザーに渡され ているが、これをどうするかも引続き検討が必要である。

   (４) 今年度目標成果ソフトウェアイメージ

   • より簡潔なグレブナ基底の正規形が実現され、ユーザーにとって解制約が いっそう見易いものになる。
   • 高速化されたグレブナ基底計算を利用した集合制約ソルバーがKLICで完成 されるので、ICOTのフリーソフトウェアのみを使ってプログラミング環境を構 築できる。
   • GDCCで使用するための、インターフェースが作成され、ユーザーは集合制 約の解法のための論理プログラミング環境を利用することができる。