Transforming and Encoding FTS for SAT Solving: What Helps, What Hurts

Filipe, João; Torralba, Álvaro; Behnke, Gregor

doi:10.24963/ijcai.2026/249

Transforming and Encoding FTS for SAT Solving: What Helps, What Hurts

João Filipe, Álvaro Torralba, Gregor Behnke

Download BibTeX Cite

Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence. Main Track. Pages 2236-2246.

https://doi.org/10.24963/ijcai.2026/249

Keywords

Constraint Satisfaction and Optimization: Satisfiabilty
Planning and Scheduling: Activity and plan recognition

Abstract

Factored tasks are a classical planning representation that extends SAS+ with limited forms of disjunctive preconditions, conditional effects, and angelic nondeterminism. This added expressiveness allows for a more compact representation of taks than traditional formalisms such as STRIPS or SAS+, and supports a wide range of task transformations. However, existing planning approaches for factored tasks have been limited to heuristic search methods.

In this work, we investigate how to encode factored tasks in SAT. We propose several ways to encode the tasks, focusing on different strategies for translating the factored transition relation into propositional logic. We also analyze how to exploit parallelism at various levels in this setting and study the impact of common task transformations on the performance of SAT-based planners.

João Filipe, Álvaro Torralba, and Gregor Behnke. 2026. Transforming and Encoding FTS for SAT Solving: What Helps, What Hurts. In Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26. IJCAI, 2236–2246. https://doi.org/10.24963/ijcai.2026/249

@inproceedings{ijcai2026p249,
  title     = {Transforming and Encoding FTS for SAT Solving: What Helps, What Hurts},
  author    = {Filipe, João and Torralba, Álvaro and Behnke, Gregor},
  booktitle = {Proceedings of the Thirty-Fifth International Joint Conference on
               Artificial Intelligence, {IJCAI-26}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Diego Calvanese},
  pages     = {2236--2246},
  year      = {2026},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2026/249},
  url       = {https://doi.org/10.24963/ijcai.2026/249},
}

TY  - CPAPER
TI  - Transforming and Encoding FTS for SAT Solving: What Helps, What Hurts
AU  - Filipe, João
AU  - Torralba, Álvaro
AU  - Behnke, Gregor
T2  - Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2026
SP  - 2236
EP  - 2246
DO  - 10.24963/ijcai.2026/249
UR  - https://doi.org/10.24963/ijcai.2026/249
ER  -