Effective SAT Planning by Lemma-Reusing

H. Nabeshima, H. Nozawa, and K. Iwanuma (Japan)


SAT planning, Satisfiablitiy, Lemma


In this paper, we propose a new approach, called lemma reusing planning, for accelerating SAT planning. Gener ally, lemmas deduced from a certain SAT problem can not apply to solve other SAT problems. However, in the SAT planning, we prove that lemmas are reusable for solving ev ery SAT problem generated from a certain planning prob lem. We implemented the lemma-reusing planner (LRP) based on Blackbox, which is one of the fastest SAT plan ning systems in the world. The experimental results show that LRP is 60% faster than Blackbox.

Important Links:

Go Back