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
