AI Planning as Satisfiability with Davis-Putnam Algorithm

This is yet another approach to improve the expressiveness and complexity of the classical planning approaches. In this technique what we do is convert our classical planning problems representation into a well-known representation called Propositional Satisfiability Problem, also called Boolean Satisfiability Problem, or simply SAT. If we can convert it to a well-known problem representation, we can use existing algorithms to solve the problems. If you are not familiar with classical planning approaches, please read the Introduction section in my previous post linked below. In this post, I'll explain the concept by going through examples step-by-step.