複数のSATソルバを用いたジョブショップスケジューリング問題の解法(「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論、論理プログラム,プランニングetc.」及び一般)  [in Japanese] Solving Job Shop Scheduling Problems With Multiple SAT Solvers  [in Japanese]

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