本年度も昨年度に引き続き、(A)実時間システムの最適スケジューリング、(B)推移関係を表すSAT節の削減手法、(C)Robust MaxSATの実装、に取り組み、3件の学術発表を行った。また、当初計画にはなかった(D)実用的解法アルゴリズムの開発のための演算不変性に関する計算機実験をSATを技術を利用して行った。 (A) 物流センター内の仕分け機のMaxSAT技術を利用した最適化スケジューリングの(荷物の戻り動作、入口階と目的階が一致している荷物の連続搬入ができるように)拡張を行い、実機の動きにより適したスケジューリングができるようにした。そして、搬送能力が向上することを確かめた。また、プロトタイプを特許出願した。 (B) 推移律を表現するSAT節の削減の手法を線形整数最適化問題(ILP)による解法にも適用した。クリーク分割問題(CPP:clique partitioning problem)を対象にしたILPにおける最新手法より削減率の点で優れていることを理論的に示し、最新のILPソルバーを使った実験でもその優位性を確かめた。 (C) 昨年度開発した解法が、QBF(Quantified Boolean Formula)ソルバーを使った手法に比べても優れていることをランダムインスタンスとCPPのインスタンスを使った実験により確かめた。 (D) 具体的な方程式をいくつか考え、定義域を狭めた問題設定で3項演算の不変演算数を全て列挙することに成功した。
|