Planning as Satisfiability (SATPlan)

SATPlan's practical power derives from its use of highly optimized Conflict-Driven Clause Learning (CDCL) SAT solvers. These solvers, such as MiniSat or Glucose, can efficiently handle formulas with millions of variables and clauses. The planner's performance is directly tied to advances in SAT solving technology, benefiting from decades of research in Boolean satisfiability. The solver performs the heavy combinatorial search, while SATPlan's encoding ensures the solution maps to a valid plan.

To find an optimal plan (e.g., shortest makespan or lowest cost), SATPlan uses an iterative deepening strategy. It first checks for a plan of length k. If unsatisfiable (UNSAT), it increments k and tries again. Once a plan is found at length k, that plan is provably optimal in terms of the number of time steps (makespan). For cost-optimal planning, the encoding is extended with action cost variables and pseudo-Boolean constraints, and the solver is invoked to find a satisfying assignment with minimal total cost.

A key feature of the classic SATPlan encoding is the automatic derivation of mutual exclusion (mutex) constraints. During the graph-building phase (inspired by Graphplan), it identifies pairs of actions or facts that cannot occur concurrently in the same time step. These mutex relations are encoded into the CNF formula, which allows the SAT solver to efficiently reason about parallel action execution. This enables SATPlan to find plans with concurrent actions, minimizing the total makespan.

While powerful in theory, SATPlan has practical limitations:

• Grounding Bottleneck: The encoding requires propositional grounding of all possible actions and objects for each time step, which can lead to an exponential explosion in variables for problems with many objects.
• Fixed Horizon: The planning horizon k must be specified or iterated over; poor heuristics for the starting k can waste time.
• Deterministic Assumption: Classical SATPlan models fully observable, deterministic worlds. Modeling uncertainty, partial observability, or contingent effects requires extensions to Stochastic SAT or Quantified Boolean Formulas. Modern variants address these with lazy grounding, satisfiability modulo theories (SMT), and integration with PDDL parsers.

Graphplan is a seminal planning algorithm that constructs a planning graph, a layered structure representing state progression over time, before searching for a solution. It directly inspired the development of SATPlan.

• Planning Graph: Alternating layers of proposition nodes (facts that could be true) and action nodes (actions whose preconditions are possibly satisfied).
• Mutual Exclusion (Mutex): Tracks pairs of actions or propositions that cannot occur in the same layer due to interference or competing needs.
• Relationship to SATPlan: The planning graph provides a compact encoding of reachability and constraints. SATPlan can be viewed as converting the planning graph into a SAT formula, where solving it finds a valid plan within the graph's structure.

Bounded Model Checking (BMC) is a formal verification technique that translates the question "Does a finite-state system violate a property within k steps?" into a SAT problem. SATPlan is conceptually a form of BMC for planning domains.

• Encoding: The system's transition relation and initial states are unrolled for k time steps and combined with a negation of the safety property.
• SAT Solving: A SAT solver checks the formula. A satisfying assignment corresponds to a counterexample trace of length k.
• Parallel to SATPlan: In planning, the "system" is the domain dynamics, the "property" is the goal condition, and the satisfying assignment is the plan. Both techniques perform bounded search (planning for a fixed k steps).

Optimal planning seeks a plan that minimizes a defined cost function, typically the sum of the costs of its constituent actions. SATPlan can be adapted for optimal planning through iterative or encoded optimization.

• Cost-Aware Encoding: Extend the SAT formula to include action cost variables and constraints that sum them.
• Iterative Approach (SATPlan): 1. Find any plan of length k. 2. Add a constraint forbidding any plan with cost >= the found plan's cost. 3. Iterate. The last found plan is optimal for length k.
• Optimization Modulo Theories (OMT): A more modern approach uses OMT solvers, which extend SAT solvers to handle cost minimization natively within theories like linear integer arithmetic.

Heuristic search is the dominant alternative paradigm to SAT-based planning. Algorithms like A* and Greedy Best-First Search (GBFS) explicitly explore the state space graph using a heuristic function to estimate distance to the goal.

• State-Space Graph: Nodes are world states, edges are applicable actions.
• Heuristic Function h(s): Estimates the cost from state s to the goal (e.g., ignore-delete-lists heuristic).
• Key Difference: Heuristic search performs an explicit graph traversal, while SATPlan performs an implicit combinatorial search via logical constraints. Heuristic search often finds initial plans faster, but SATPlan can be superior for proving optimality or finding plans in highly constrained, "needle-in-a-haystack" problems.