抄録
本稿では,SATプランニングとSATスケジューリングを効率よく解くために補題再利用手法を提案し,その効果を実証する.一般的に,SATプランニングやSATスケジューリングなどのSAT符号化手法においては,徐々に大きくなるSAT問題の列を解く必要がある.多くの最新のSATソルバは,冗長な探索空間を狩り取るために補題を学習し利用している.しかし,あるSAT問題から生成された補題は,基本的に他のSAT問題を解くために利用することはできない.本稿では,SATプランニングとSATスケジューリングにおけるある特定のSAT符号化においては補題が再利用可能であることを証明し,補題を再利用することにより効率的に問題を解くことができることを実証する.
In this paper, we propose a new approach, called lemma-reusing, for accelerating SAT based planning and scheduling. Generally, SAT based approaches generate a sequence of SAT problems which become larger and larger. A SAT solver needs to solve the problems until it encounters a satisfiable SAT problem. Many state-of-the-art SAT solvers learn lemmas called conflict clauses to prune redundant search space, but lemmas deduced from a certain SAT problem can not apply to solve other SAT problems. However, in certain SAT encodings of planning and scheduling, we prove that lemmas generated from a SAT problem are reusable for solving larger SAT problems. We implemented the lemma-reusing planner (LRP) and the lemma-reusing job shop scheduling problem solver (LRS). The experimental results show that LRP and LRS are faster than lemma-no-reusing ones.
