Modelling and Solving Problems Using SAT Techniques


Solving planning problems via translation to satisfiability (SAT) is one of the most successful approaches to automated planning. In this thesis we describe several ways of encoding a planning problem represented in the SAS+ formalism into SAT. We review and adapt existing encoding schemes as well as introduce new original encodings. We compare the encodings by calculating upper bounds on the size of the formulas they produce as well as by running extensive experiments on benchmark problems from the 2011 International Planning Competition (IPC). In the experimental section we also compare our encodings with the state-of-the-art encodings of the planner Madagascar. The experiments show, that our techniques can outperform these state-of-the-art encodings. In the presented thesis we also deal with a special case of post-planning optimization -- elimination of redundant actions. The elimination of all redundant actions is NP-complete. We review the existing polynomial heuristic approaches and propose our own heuristic approach which can eliminate a higher number and more costly redundant actions than the existing techniques. We also propose a SAT encoding for the problem of plan redundancy which together with MaxSAT solvers allows us to solve the problem of action elimination optimally. Experiments done with plans from state-of-the-art satisficing planners for IPC benchmark problems demonstrate, that all the proposed techniques work well in practice.


PhD Thesis Fulltext:
Abstract of Doctoral Thesis:
Resources (sourcecode + data):
Defense Presentaion Slides:
Review - Barták:
Review - Biere:
Review - Železný:

Curriculum Vitae

Academic CV:
Professional CV:
Publications by type:
DBLP Publications:

List of Publications By Time

  • 2014
    1. Tomas Balyo, Roman Bartak, Otakar Trunda: Reinforced Encoding for Planning as SAT, Student Conference on Planning in Artificial Intelligence and Robotics (PAIR) 2014, Paper, Slides
    2. Tomas Balyo, Lukas Chrpa, Asma Kilani: On Different Strategies for Eliminating Redundant Actions from Plans, The Seventh Annual Symposium on Combinatorial Search (SOCS) 2014, Paper, Slides
    3. Tomas Balyo, Andreas Froehlich, Marijn Heule and Armin Biere: Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask), 17th International Conference on Theory and Applications of Satisfiability Testing (SAT) 2014, Paper, Slides, Resources
    4. Tomas Balyo, Lukas Chrpa: Eliminating All Redundant Actions from Plans Using SAT and MaxSAT, Proceedings of the 5th Workshop on Knowledge Engineering for Planning and Scheduling (KEPS) 2014, pp. 16-22, Portsmouth, NH, USA, 2014 Paper, Poster, Slides
  • 2013
    1. Tomas Balyo: Relaxing the Relaxed Exist-Step Parallel Planning Semantics, Proceedings of ICTAI 2013, pp 865-871, Washington, DC, USA, 2013 Paper, Poster, Slides
    2. Martin Babka, Tomas Balyo, Jaroslav Keznikl: Solving SMT Problems with a Costly Decision Procedure by Finding Minimum Satisfying Assignments of Boolean Formulas, Studies in Computational Intelligence, volume 496, pp. 231-246, 2013 Paper
    3. Martin Babka, Tomas Balyo, Jaroslav Keznikl: Finding Minimum Satisfying Assignments of Boolean Formulas, Poster and abstract in Proceedings of The 26th International FLAIRS Conference 2013, St. Pete Beach, Florida, USA. AAAI, 2013 Abstract Link
    4. Martin Babka, Tomas Balyo, Ondrej Cepek, Stefan Gurský, Petr Kucera, Václav Vlcek: Complexity issues related to propagation completeness, Artificiall Intellingence, volume 206, pp. 19-34, 2013 Link, Paper
  • 2012
    1. Tomas Balyo, Roman Bartak, Pavel Surynek: Shortening Plans by Local Re-Planning, Proceedings of ICTAI 2012, Athens, Greece, 2012 Paper
    2. Tomas Balyo, Roman Bartak, Pavel Surynek: On Improving Plan Quality via Local Enhancements, Proceedings of SOCS 2012, Niagara Falls, Ontario, Canada, 2012 (short paper) Paper Poster
    3. Tomas Balyo, Stefan Gursky, Petr Kucera, Vaclav Vlcek: On Hierarchies over the SLUR Class1, Proceedings of ISAIM 2012, Fort Lauderdale, Florida, USA, 2012 Paper
  • 2011 - 2009
    1. Tomas Balyo, Dan Toropila, Roman Bartak: Two Semantics for Step-Parallel Planning: Which One to Choose?1, Proceedings of PLANSIG 2011, Huddersfield, United Kingdom, 2011 Paper
    2. Tomas Balyo: Decomposing Boolean formulas into connected components, Proceedings of the 20th Annual Conference of Doctoral Students - WDS 2011, Prague, Czech Republic, 2011 Paper
    3. Tomas Balyo: Solving Boolean satisfiability problems, Master thesis, Faculty of Mathematics and Physics, Charles University in Prague, 2010 Thesis
    4. Tomas Balyo, Pavel Surynek: Efektivni heuristika pro SAT zalozena znalosti komponent souvislosti grafu problemu (An Efficient Heuristic for SAT Exploiting Connected Components of the Problem) Proceedings of the Conference Znalosti 2009, Brno, Czech Republic, 2009 Paper

1 Also presented on the 14th Czech-Japan Seminar on Data Analysis and Decision Making 2011.