Planning as Satisfiability (SATPlan)

The core mechanism of SATPlan is the propositional encoding of a planning problem into Conjunctive Normal Form (CNF). For a planning horizon of k steps, it creates variables representing:

• Action variables: A_t (Action a occurs at time step t).
• Fact variables: F_t (Proposition f is true at time step t). The CNF formula encodes the initial state, goal conditions, action preconditions and effects, and the frame axioms (which facts persist unchanged). A SAT solver's assignment of true/false to these variables decodes into a plan.

SATPlan operates on the principle of bounded plan existence. It does not search the state space directly. Instead, for a given planning horizon k (number of time steps), it asks: "Does a plan of length k exist?" The algorithm iteratively increases k (starting from 0 or 1) until it finds a satisfiable formula. This makes it a completeness-preserving algorithm; if an optimal plan of length k exists, SATPlan will find it for that k, though finding the minimal k requires iteration.

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.

The Boolean satisfiability problem (SAT) is the computational task of determining if there exists an assignment of truth values (TRUE/FALSE) to the variables of a given propositional logic formula that makes the entire formula evaluate to TRUE. SAT is the foundational NP-complete problem that SATPlan leverages.

• SAT Solvers: Modern, highly optimized algorithms (e.g., Conflict-Driven Clause Learning) that can solve large formulas with millions of variables.
• CNF Encoding: Problems are typically encoded in Conjunctive Normal Form, a conjunction of clauses, where each clause is a disjunction of literals.
• Applications: Beyond planning, SAT is fundamental to hardware verification, software testing, and cryptography.

PDDL is the standardized, first-order logic-based language used to formally define planning domains (actions, predicates, types) and planning problems (objects, initial state, goal). It is the primary input language for most classical planners, including those using SATPlan.

• Domain File: Declares predicates (e.g., (on ?x ?y)) and actions with :parameters, :precondition, and :effect.
• Problem File: Instantiates objects, defines the initial state as a set of grounded literals, and specifies the goal condition.
• Role in SATPlan: The SATPlan algorithm first translates a PDDL problem into a propositional formula, which is then solved by a SAT solver.

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.