One way to automate planning is with Satplan, also known as Planning as Satisfiability. This step changes the planning problem into a Boolean satisfiability problem. It can then be solved using a satisfiability method, like the DPLL algorithm or WalkSAT.

A planning problem is given a starting state, a set of actions, a goal, and a horizon length. The problem is then turned into a formula that can only be satisfied if there is a plan with the given horizon length. 

The satisfiability problem in the proof of Cook's theorem is like this when you simulate Turing machines. One way to find a plan is to see if the formulas can satisfy different horizon lengths. Going through the horizon lengths in order, 0, 1, 2, and so on, is the easiest way.

SAT-based planners

The most recent SAT-based planners compete with (and frequently surpass) those based on alternative search paradigms. Furthermore, this efficiency is achieved almost exclusively by utilizing general-purpose SAT-solving algorithms, eliminating the requirement for specialized techniques prevalent in contemporary state-space search planners. The disparity between the preferred algorithms for planning and closely related forms of state-space searches, such as model-checking in computer-aided verification (CAV), can be partially elucidated by these advancements: Explicit state-space search dominated CAV until the early 1990s when it was largely supplanted by (symbolic) logic-based methods (first binary decision diagrams (BDD) and later SAT). 

In contrast, explicit state-space search was "discovered" in AI planning in the late 1990s and has been considered the most effective search method by planning researchers on occasion for somewhat arbitrary reasons.

GraphPlan

In recent years, the introduction of asymptotically optimal, linear-size encodings for the primary classes of plans, including the GraphPlan concept of parallel plans, has been a significant development in planning as SAT. Particularly for the action exclusion axioms, all previous encodings had a quadratic dimension, which resulted in formulas comprising hundreds or thousands of megabytes and rendered impracticable the application of efficient parallel search strategies.

STRIPS problems

Prior research has almost exclusively employed parallel plans predicated on interference: two actions can occur concurrently so long as they do not cause interference. In numerous situations where the no-interference condition is not met, parallelization of activities is feasible because a more relaxed asymmetric notion of interference in ∃-step semantics occasionally permits significantly more efficient planning. 

An additional expansion of the ∃-step semantics, which pertains to a more limited category of STRIPS problems, is documented in a paper titled "Planning as Satisfiability with Relaxed ∃-step Plans" by Wehrle and Rintanen. This paper further relaxes the requirements for parallel actions, which, in certain instances, results in additional enhancements in performance. These encodings in two steps are the most rapid encodings currently available.

Traditional SAT-based planners

Traditional SAT-based planners take much longer to find plans than planners who solve multiple SAT cases simultaneously. This idea and the best encodings make planners work well in many areas used for benchmarking in the planning community. Early SAT search strategies only used the sequential approach, also called exhaustive breadth-first (or iterative-deepening) search. This strategy could be better at scaling up than others, and it should only be used when trying to find the shortest answers. You don't have to use a strict breadth-first search order. There are much better methods out there.

Image source: Unsplash