When both Grounding and not Grounding are Bad -- A Partially Grounded Encoding of Planning into SAT (Extended Version)

This paper introduces three novel SAT encodings for classical planning that achieve a middle ground by keeping actions lifted while partially grounding predicates, resulting in linear scaling with plan length and superior performance on hard-to-ground domains compared to state-of-the-art methods.

The Gist

Imagine you are trying to organize a massive, chaotic warehouse to get a specific package to a specific door. You have a list of rules (like "you can't put a box on top of a fragile item") and a list of workers (the actions) who can move things around.

This is the problem of Automated Planning. Computers need to figure out the exact sequence of moves to get from "Messy Warehouse" to "Perfectly Organized Warehouse."

The Old Problem: The "Grounding" Bottleneck

For a long time, computers tried to solve this by grounding everything. Think of this like making a giant, physical list of every single possible move for every single specific item.

• Instead of saying "Move any box," the computer writes down: "Move Box A," "Move Box B," "Move Box C"... all the way to "Move Box Zillion."
• The Issue: If you have 1,000 boxes and 100 locations, the list of moves becomes astronomically huge. It's like trying to read a phone book the size of a city just to find one number. This causes the computer to crash or take forever because the list is too big.

The New Approach: The "Partial Grounding" Middle Ground

The authors of this paper found a clever middle path. They realized you don't need to list every specific move, but you also don't need to keep everything abstract.

They introduced a method called Partially Grounded Encoding. Here is how it works using a simple analogy:

1. The "Universal Worker" (Lifted Actions)

Instead of naming every specific worker (Worker 1, Worker 2...), the computer keeps the workers as generic roles: "The Driver," "The Loader." It doesn't care which specific person is driving yet; it just knows the role exists. This keeps the action list small and manageable.

2. The "Smart Inventory" (Partial Grounding)

This is where the magic happens.

• The Old Way (Fully Grounded): The computer tries to track the exact location of every single box at every single second.
• The New Way (Partially Grounded): The computer uses Mutex Groups (a fancy term for "mutually exclusive groups").
  • Analogy: Imagine a set of lockers. You know for a fact that only one locker can be open at a time in a specific row. You don't need to check every single locker in the row to see if it's open. You just need to know which one is the "active" one.
  • The computer tracks these groups. It says, "Okay, for the 'Package Location' group, only one location is true right now." It doesn't list every impossible location; it just tracks the one that matters.

The "Binary" Shortcut

The paper also introduces a "Binary Encoding" trick.

• The Old Way: To say "The package is in Locker 500," the computer uses 500 different switches, flipping the 500th one on and keeping the rest off.
• The New Way: It uses a binary code (like a computer's 0s and 1s). To say "Locker 500," it only needs about 9 switches (because $2^9 = 512$).
• Why it matters: This shrinks the problem size massively, like compressing a 100-page document into a single sticky note.

The Result: Linear vs. Quadratic Growth

The most important finding is about how the problem gets bigger as the plan gets longer.

• Old Methods (LiSAT): If you double the length of the plan, the computer's work quadruples (it gets 4x harder). It's like trying to solve a puzzle where every new piece you add makes the whole board explode in size.
• This New Method: If you double the length of the plan, the work only doubles. It grows in a straight line. It's like adding a new page to a book; the book gets bigger, but it doesn't suddenly turn into a mountain.

Why Should You Care?

The authors tested this on some of the hardest planning puzzles (like moving packages, navigating robots, and organizing logistics).

• The Winner: Their new method solved more difficult problems than the current "best" methods, especially when the plans needed to be long.
• The Takeaway: By being smart about what to list and what to group, they made computers much better at solving complex "how do I get from A to B" puzzles without getting overwhelmed by the sheer number of possibilities.

In short: They stopped trying to write down every single specific detail of every single move. Instead, they wrote down the rules of the game and the groups of possibilities, allowing the computer to solve long, complex plans much faster and with less memory.

Technical Summary

1. Problem Statement

Classical automated planning problems are typically defined using lifted (first-order) representations to maintain compactness and generality. However, solving these problems often requires grounding (instantiating all variables with objects), which can lead to an exponential blowup in problem size, making it intractable for domains with many objects or high-arity predicates.

Recent approaches attempt to avoid full grounding by operating directly on the lifted level (e.g., LiSAT). While LiSAT is the state-of-the-art for length-optimal planning, it suffers from a critical scalability limitation: its SAT formula size grows quadratically with the plan length ($L$). This is because LiSAT uses a stateless encoding that relies on causal links to connect action preconditions to their achievers across time steps. As $L$ increases, the number of potential causal links explodes, hindering performance on long plans.

The authors identify a "middle ground" problem: fully grounding is too expensive, but fully lifting (as in LiSAT) creates quadratic scaling. The goal is to find an encoding that avoids the exponential blowup of full grounding while achieving linear scaling with respect to plan length.

2. Methodology

The authors propose a family of three SAT encodings that keep actions fully lifted but partially ground the state description (predicates).

Core Concepts

• Unified Arguments (UA): The encodings adopt LiSAT's method of handling action arguments. Instead of splitting arguments by position or overloading them, arguments are grouped by type. This allows different actions to share argument variables if they operate on the same object types, reducing variable redundancy.
• Partially Lifted Mutex Groups (PLMGs): The authors leverage Lifted Mutex Groups (LMGs)—sets of facts where at most one can be true in any reachable state (e.g., a package cannot be in two locations simultaneously). They use a discovery method (Fiˇser 2020) to find these groups and then instantiate them into PLMGs by fixing some variables.
  • Instead of explicitly representing every ground fact, the state of a PLMG is represented by a counted variable indicating which specific object (or "none") is currently true for that group.

The Three Encodings

The paper introduces three variations of the encoding, differing in how they represent the state:

1. Fully Grounded: A baseline approach where all predicates are fully grounded. It serves as a control but is not competitive due to size.
2. Partially Grounded (One-Hot): Uses PLMGs to represent state. For each PLMG, it uses a one-hot encoding (a boolean variable for every possible object in the group) to indicate which fact is true.
3. Partially Grounded (Binary): An optimization of the above. Instead of one-hot encoding, it uses binary encoding ($\lceil \log_2 |O| \rceil$ bits) to represent the object selected by a PLMG's counted variable. This significantly reduces the number of variables for domains with many objects.

Key Technical Innovations

• Explicit State Tracking: Unlike LiSAT, these encodings explicitly track the state at each time step ($t$). This removes the need for causal links between arbitrary time steps, which was the source of LiSAT's quadratic growth.
• Linear Scaling: By explicitly modeling state transitions ($\tau(t, t+1)$) and using PLMGs to compress state representation, the formula size scales linearly with the plan length ($L$), rather than quadratically.
• Predicate Pruning: The authors implement an optimization that removes predicates from the encoding if they do not appear in the goal or as preconditions of any action. This drastically reduces the number of facts that need to be encoded, especially in domains like Visitall.
• Frame Axioms: The encoding includes specific constraints to ensure that a counted variable's value only changes if an action explicitly sets it, maintaining the integrity of the state transition.

3. Key Contributions

1. Novel SAT Encodings: Introduction of three encodings that bridge the gap between fully lifted and fully grounded planning, specifically targeting the quadratic scaling issue of LiSAT.
2. Linear Complexity: Demonstration that by explicitly tracking state via PLMGs, the SAT formula size scales linearly with plan length, enabling the solution of longer plans.
3. Binary State Encoding: A novel application of binary encoding to PLMG counted variables, reducing variable count in large-object domains.
4. Predicate Pruning Strategy: A specific pruning technique for lifted planning that removes irrelevant predicates before grounding/encoding, further reducing formula size.
5. Empirical Validation: Comprehensive evaluation showing that the proposed methods outperform the state-of-the-art (LiSAT) in length-optimal planning on difficult-to-ground domains.

4. Experimental Results

The authors evaluated their encodings on standard lifted planning benchmarks (e.g., Blocksworld, Logistics, Rovers, Visitall) against:

• LiSAT (State-of-the-art lifted SAT planner).
• Powerlifted (PWL) and CPDDL (Search-based lifted planners).
• Madagascar (MpC) and Fast Downward (FD) (Grounded planners).

Key Findings:

• Optimal Planning: The Binary encoding with Predicate Pruning (Binary PP) outperformed LiSAT in 5 out of 9 domains. In domains like Logistics, Pipesworld, and Rover, it solved 20% more instances than LiSAT.
• Scalability: While Binary PP generated more clauses than LiSAT (due to the overhead of encoding PLMG semantics), it used significantly fewer variables (up to two orders of magnitude less in some cases). Crucially, the growth rate of variables and clauses was linear for the proposed method versus quadratic for LiSAT.
• Satisficing Planning: The proposed method was competitive with search-based lifted planners (PWL) and outperformed them in specific domains (Blocksworld, Visitall), suggesting that SAT-based and search-based approaches offer complementary strengths.
• Predicate Pruning Impact: In the Visitall domain, pruning a single predicate reduced the number of explicitly encoded facts by ~50%, significantly boosting performance.

5. Significance

This paper addresses a fundamental bottleneck in automated planning: the trade-off between the compactness of lifted representations and the tractability of grounded ones.

• Theoretical Impact: It proves that explicit state tracking combined with lifted mutex groups can break the quadratic barrier of previous lifted SAT encodings, offering a new path for scaling SAT-based planning.
• Practical Impact: The proposed encodings enable the solution of planning problems with long plans and large object sets that were previously intractable for LiSAT.
• Future Directions: The authors suggest that these encodings could be extended to support action parallelism, negative preconditions, and conditional effects, potentially making them a robust foundation for next-generation planning systems.

In summary, the paper successfully demonstrates that partial grounding of the state (using PLMGs) while keeping actions lifted is a superior strategy for length-optimal planning in complex domains, offering a scalable alternative to both full grounding and fully lifted causal-link encodings.