| 講演名 | 2004-06-21 複数のSATソルバを用いたジョブショップスケジューリング問題の解法(「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論、論理プログラム,プランニングetc.」及び一般) 宋 剛秀, 井上 克巳, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本論文では,ジョブショップ・スケジューリング問題(JSSP)に関して,JSSPを充足可能性判定問題(SAT)に変換することによる解法について考察する.JSSPをSATに変換する変換方法として,CrawfordとBakerによる変換を採用し,Javaにより実装した.この変換においてJSSPの期限が,変換後のSAT問題の変数と節数にどのように影響するかについて考察する.この変換の特徴として,期限が最適値に近いほど充足される変数の組み合わせが少なくなり,SAT問題として難しいものになるということが挙げられる.次に計算機実験により,期限を最適値を含む範囲で変化させたSAT問題を複数用意し,複数異種のSATソルバを並列に実行することができるMultisatにより解かせた.これにより,計算速度や有効に働くSATソルバの種類などのMultisatの特性を観察し,問題の難易度との関係を考察する.さらにMultisatと単体ソルバとの性能比較も行う. |
| 抄録(英) | Many algorithms have recently been proposed for solving propositional satisfiability(SAT). This paper is concerned with a method to solve a job-shop scheduling problem(JSSP) by SAT solvers. Here, JSSP is translated into SAT using Crawford and Baker's method. We consider how due time affect the number of translated clauses. It turns out that due time heavily affects the difficulty of SAT problems. Next, to solve JSSP efficiently, we perform parallel execution of SAT solvers through Multisat, which competitively solves SAT problems by both systematic and stochastic SAT solvers. We also compare Multisat with single SAT solvers for JSSP. |
| キーワード(和) | ジョブショップ・スケジューリング問題 / 充足可能性判定問題 / SATソルバ |
| キーワード(英) | job-shop scheduling problems / propositional satisfiability / SAT solvers |
| 資料番号 | AI2004-4 |
| 発行日 |
| 研究会情報 | |
| 研究会 | AI |
|---|---|
| 開催期間 | 2004/6/14(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 複数のSATソルバを用いたジョブショップスケジューリング問題の解法(「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論、論理プログラム,プランニングetc.」及び一般) |
| サブタイトル（和） | |
| タイトル（英） | Solving Job Shop Scheduling Problems With Multiple SAT Solvers |
| サブタイトル（和） | |
| キーワード(1)（和/英） | ジョブショップ・スケジューリング問題 / job-shop scheduling problems |
| キーワード(2)（和/英） | 充足可能性判定問題 / propositional satisfiability |
| キーワード(3)（和/英） | SATソルバ / SAT solvers |
| 第 1 著者 氏名（和/英） | 宋 剛秀 / Takehide SOH |
| 第 1 著者 所属（和/英） | 神戸大学大学院自然科学研究科 Graduate School of Science and Technology, Kobe University |
| 第 2 著者 氏名（和/英） | 井上 克巳 / Katsumi INOUE |
| 第 2 著者 所属（和/英） | 国立情報学研究所 National Institute of Informatics |
| 発表年月日 | 2004-06-21 |
| 資料番号 | AI2004-4 |
| 巻番号（vol） | vol.104 |
| 号番号（no） | 133 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |