複数のSATソルバを用いたジョブショップスケジューリング問題の解法 Solving Job-shop Scheduling Problems with Multiple SAT Solvers

この論文をさがす

著者

抄録

本論文では,ジョブショップ・スケジューリング問題(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.

収録刊行物

  • 電子情報通信学会技術研究報告. AI, 人工知能と知識処理

    電子情報通信学会技術研究報告. AI, 人工知能と知識処理 104(133), 19-24, 2004-06-14

    一般社団法人電子情報通信学会

参考文献:  17件中 1-17件 を表示

各種コード

  • NII論文ID(NAID)
    110003176997
  • NII書誌ID(NCID)
    AN10013061
  • 本文言語コード
    JPN
  • 資料種別
    ART
  • ISSN
    09135685
  • NDL 記事登録ID
    7036912
  • NDL 雑誌分類
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL 請求記号
    Z16-940
  • データ提供元
    CJP書誌  NDL  NII-ELS 
ページトップへ