Prolog処理系を用いた複数SATソルバ並列実行システム

2007 Fiscal Year Annual Research Report

• Project/Area Number: 19700025
• Research Institution: Kobe University
• Principal Investigator: 番原 睦則 Kobe University, 学術情報基盤センター, 准教授 (80290774)
• Keywords: 論理プログラミング / SAT / 並列計算 / Prolog

Research Abstract

本年度は,以下の研究成果を得た.
・PrologからJavaへのトランスレータ処理系Prolog Cafeの改良
PrologをJavaへ変換する手法として,節をメソッドに変換する新しいトランスレート方法を提案し,その実装を行ったまたインデキジング,組込み述語のインライン展開による最適化を実装し,Prolog Cafeの実行効率の改善を実現した.改良したシステムは,http://kaminari.istc.kobe-u.ac.jp/PrologCafe/に公開中である.
・SAT変換に基づいたCSPソルバーの開発・改良
制約最適化問題(COP)をSAT問題に変換する手法としてOrder Encodin法と呼ばれる新しいSAT変換手法を提案し,それに基づくCSPソルバーSugarの開発・改良を行った.
開発したシステムは,第2回国際CSPソルバー競技会において,N変数整数制約式部門で4位の成績をおさめた.

Research Products

• [Journal Article] Sugar: A CSP to SAT Translator Based on Order Encoding (2008)
  • Author(s): Naoyuki Tamura
  • Journal Title: Proceedings of the Second International CSP Solver Competition Pages: 65-59
  • Peer Reviewed
• [Journal Article] PrologからJavaへのトランスレータ処理系とその応用 (2007)
  • Author(s): 番原 睦則
  • Journal Title: コンピュータソフトウェア 第24巻・第3号 Pages: 75-86
  • Peer Reviewed
• [Presentation] グリッド計算環境上でのショップ・スケジューリング問題のSAT変換による解法 (2007)
  • Author(s): 多賀 明子
  • Organizer: スケジューリング・シンポジウム2007講演論文集
  • Place of Presentation: 京都大学
  • Year and Date: 2007-09-29
• [Presentation] Prolog Cafe: PrologからJavaへのトランスレータ処理系のデモ (2007)
  • Author(s): 丹生 智也
  • Organizer: 日本ソフトウェア科学会第24回大会
  • Place of Presentation: 奈良先端科学技術大学院大学
  • Year and Date: 2007-09-12
• [Remarks]
  • URL: http://kaminari.istc.kobe-u.ac.jp/PrologCafe/