When Both Grounding and Not Grounding Are Bad - A Partially Grounded Encoding of Planning into SAT

Sep 14, 2026

Uploaded by Rizky

Classical planning problems are usually expressed with lifted first-order representations, but planners often fully ground them to simplify reasoning, which can cause an exponential blowup in representation size. This work studies a compromise between fully lifted and fully grounded planning by proposing three SAT encodings that keep actions lifted while partially grounding predicates. The new encodings avoid quadratic scaling in plan length, showing linear growth. Experiments demonstrate that the best encoding improves length-optimal planning performance on domains that are hard to ground.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages11

Reading Time28 min

AccessFree to download

Abstract

Introduction

Preliminaries

Lifted Planning

Applicability

State Transition

When both Grounding and not Grounding are Bad – A Partially Grounded Encoding of Planning into SAT Joo Filipe 1 , Gregor Behnke 1 1University of Amsterdam, Institute for Logic Language and Computation, The Netherlands [j.sa@uva.nl](j.sa@uva.nl), [g.behnke@uva.nl](g.behnke@uva.nl) arXiv :2603 . 19429v1 [ cs .AI] 19 Mar 2026 Abstract Classical planning problems are typically defined using lifted first-order representations, which offer compactness and generality. While most planners ground these representations to simplify reasoning, this can cause an exponential blowup in size. Recent approaches instead operate directly on the lifted level to avoid full grounding. We explore a middle ground between fully lifted and fully grounded planning by introducing three SAT encodings that keep actions lifted while partially grounding predicates. Unlike previous SAT encodings, which scale quadratically with plan length, our approach scales linearly, enabling better performance on longer plans. Empirically, our best encoding outperforms the state of the art in length-optimal planning on hard-to-ground domains. Introduction Automated Planning aims to find a sequence of actions that transforms an initial state into one satisfying a given goal. While most research in the last decades focussed on solving planning problems that can be fully ground instantiated, the task of lifted planning - that is planning with actions described using a function-free first-order language - has made significant progress since the seminal work by Corra et al. (2020) . Using lifted planning, significantly larger problems than before could be tackled successfully. Current methods for lifted planning mainly fall into two categories: ones based on search and ones based on translation to logic. In this paper, we focus on the latter. Shaik and van de Pol (2022) proposed a translation of lifted planning into Quantified Boolean Formulae (QBF), in which lifting is encoded using universal quantification by iterating over possible objects as arguments for predicates. Atthe same time Hller and Behnke (2022) proposed an encoding into Boolean Satisfiability (SAT)–called LiSAT – which is until now the state-of-the-art for plan-length optimal planning, which is also optimal planning for unit-cost problems. Similar to grounded SAT-based planners, it views the plan asa sequence of time steps and generates SAT formulae ϕℓ that are satisfiable iff there is a plan of length up to ℓ . To generate an optimal plan, it iterates over ℓ until a plan is found. LiSAT Extended version of a paper under Copyright of © 2026, Association for the Advancement of Artificial Intelligence (www.aaai.org) . All rights reserved. Extensions under CC BY-SA. expresses lifting using variables at and (v = o)t denoting that action a is executed at time t and argument variable v of that action is the object o, respectively. To encode that preconditions of actions are met and that effects are applied, LiSAT uses the concept of causal links (Penberthy and Weld 1992), linking actions having a fact as a precondition to actions that make that fact true. As a consequence, the size of ϕℓ grows quadratically in ℓ – which is not desirable. We explore the middle ground between full grounding and full lifting for SAT-based planning. For this, we introduce three encodings that require only a partial grounding of the planning problem. In all three, actions are encoded fully lifted. For the state description, i.e., the problem’s predicates, we investigate both a full grounding approach, as well as two approaches that represent the current state using lifted representations that explicitly encode predicatesand their argument objects. For the latter two, we use lifted mutex groups (Helmert 2009), allowing for a compact lifted encoding of some of the problem’s predicates. We present two ways of encoding objects in this case: with a one-hot encoding or with a binary encoding. Although the full groun

FAQs

What problem does the paper identify with fully grounded lifted planning?

Fully grounding lifted first-order representations can simplify reasoning, but it may trigger an exponential blowup in the size of the resulting representation.

How does the proposed approach differ from fully lifted or fully grounded SAT encodings?

The paper introduces three SAT encodings that keep actions fully lifted while partially grounding predicates, aiming for a middle ground between the two extremes.

What scaling improvement and empirical result does the paper report?

The new encodings scale linearly with plan length instead of quadratically. Empirically, the best encoding outperforms the state of the art in length-optimal planning on hard-to-ground domains.

Sep 14, 2026

Uploaded by Rizky