SATPlan¶
An automated-planning method that encodes the existence of a bounded-length action sequence as a Boolean satisfiability formula, calls a SAT solver, and decodes any satisfying assignment into a valid plan.
Core Idea¶
SATPlan treats a plan as a satisfying assignment to time-indexed facts and actions. Logic clauses make illegal transitions impossible, so a SAT solver becomes the search engine for bounded planning.
Correctness resides in the translation. Horizon, frame axioms, concurrency, mutex conditions, and decoder must preserve the original planning semantics; an impressive solver result cannot compensate for missing constraints.
Scope of Application¶
- Classical planning. Finds bounded action sequences.
- Plan optimality. Increases horizon to seek shortest makespan under conditions.
- Verification research. Relates transition systems and bounded logical encodings.
- Solver engineering. Uses incremental SAT, learned clauses, and domain invariants.
Clarity¶
Report planning formalism, state variables, action semantics, horizon meaning, sequential or parallel plan convention, frame and mutex encoding, goal clauses, SAT solver and settings, incremental reuse, decode rule, validation, and optimality claim. Inclusion test: Require a planning-to-SAT encoding parameterized by horizon, satisfiability solving, and decoding into a plan valid under the original planning semantics. Exclusion test: Exclude direct heuristic state-space search, SAT solving unrelated to planning, bounded model checking with no planning goal, and a constraint encoding that omits action transitions or plan extraction. Nearest boundary: Graphplan builds a planning graph and extracts plans through graph constraints; it influenced SAT encodings but is not identical to submitting a propositional formula to a SAT solver. Exit condition: The method fails semantically when concurrency, frame, mutex, action cost, or horizon meaning differs between encoding and original domain. Common misclassifications: Any use of a SAT solver is not planning as satisfiability. Unsatisfiable at horizon h does not rule out longer plans. A satisfying assignment is not a plan until decoded and validated. Parallel and sequential horizon semantics should not be mixed. Nearest named distinctions: Graphplan: Searches and extracts through a planning graph. Bounded model checking: Searches for counterexample paths to a property. SAT solving: Is the generic decision engine, not the planning reduction. Constraint programming: Can solve plans through other constraint domains.
Manages Complexity¶
The method replaces combinatorial action search with combinatorial Boolean inference. Its power comes from exposing planning structure to mature SAT propagation and learning while keeping the translation auditable.
Abstract Reasoning¶
- Normalize the planning instance into explicit states, actions, initial facts, and goals.
- Choose horizon and sequential or parallel semantics.
- Encode initial, transition, frame, compatibility, and goal constraints.
- Solve incrementally or independently under documented SAT settings.
- Decode and simulate the candidate plan; increase horizon when unsatisfiable and the search policy requires it.
Knowledge Transfer¶
Bounded transition encoding transfers to scheduling and verification, but SATPlan identity requires actions and goals under planning semantics. Domain-specific concurrency and costs need new clauses rather than analogy.
Relationships to Other Abstractions¶
Current abstraction SATPlan Domain-specific
Parents (1) — more general patterns this builds on
-
SATPlan is a kind of Planning Prime
SATPlan is a strict kind of Planning: its frozen identity entails the parent's defining structure while adding domain-specific restrictions.
Neighborhood in Abstraction Space¶
SATPlan sits in a crowded region of the domain-specific corpus (31st percentile for distinctiveness): several abstractions share nearly its structure, so a description that fits it tends to fit its neighbors too.
Family — Decision & System Modeling Frameworks (30 abstractions)
Nearest neighbors
- Generalized Büchi Automaton — 0.90
- Causal System — 0.88
- Time Reversibility — 0.88
- Logic Puzzle — 0.88
- Complex Affine Space — 0.88
Computed from structural-signature embeddings · 2026-10-08