Research


based on words from all my abstracts

Research interests

  • Boolean Satisfiability Solving (SAT) and friends (#SAT, MAX-SAT, PBO)
  • Boolean Function Theory
  • Classical A.I. Planning
  • Planning as Satisfiability (SATPlan)

Projects

  • HordeSat A massively parallel Satisfiability solver
  • FreeLunch An open-soruce Java planning library
  • AquaPlanning Another open-soruce (educational) Java planning library

Publications

Google Scholar, DBLP, Springer Link

  • 2019
    1. Dominik Schreiber, Damien Pellier, Humbert Fiorino, Tomas Balyo: Efficient SAT Encodings for Hierarchical Planning, ICAART 2019 Paper, Slides,
    2. Dominik Schreiber, Damien Pellier, Humbert Fiorino, Tomas Balyo: Tree-REX: SAT-Based Tree Exploration for Efficient and High-Quality HTN Planning, ICAPS 2019 Paper, Slides,
    3. Kai Fieger, Tomas Balyo, Christian Schulz, Dominik Schreiber: Finding Optimal Longest Paths by Dynamic Programming in Parallel, SoCS 2019 Paper, Slides,
    4. Nils Froleyks, Tomas Balyo, Dominik Schreiber: PASAR -- Planning as Satisfiability with Abstraction Refinement, SoCS 2019 Paper, Slides,
  • 2018
    1. Tomas Balyo, Lukas Chrpa: Using Algorithm Configuration Tools to Generate Hard SAT Benchmarks, SoCS 2018 Paper, Slides,
    2. Tomas Balyo, Carsten Sinz: Parallel Satisfiability, Chapter 1 in Handbook of Parallel Constraint Reasoning, Springer, 2018 Book,
  • 2017
    1. Tomas Balyo, Marijn J. H. Heule, Matti Järvisalo: SAT Competition 2016: Recent Developments, AAAI 2017 Paper, Slides,
    2. Tomas Balyo, Stephan Gocht: Accelerating SAT Based Planning with Incremental SAT Solving, ICAPS 2017 Paper, Slides, Poster
    3. Tomas Balyo, Nils Christian Froleyks: Using an Algorithm Portfolio to Solve Sokoban, SoCS 2017 Paper, Poster
    4. Tomas Balyo, Marijn J. H. Heule, and Matti Järvisalo (editors): Proceedings of SAT COMPETITION 2017 Solver and Benchmark Descriptions, University of Helsinki institutional repository Book, Homepage
  • 2016
    1. Tomas Balyo, Martin Suda: Reachlunch entering the Unsolvability IPC 2016, Unsolvability IPC 2016: planner abstracts, pages 3-6 Paper,
    2. Tomas Balyo, Marijn J. H. Heule, and Matti Järvisalo (editors): Proceedings of SAT COMPETITION 2016 Solver and Benchmark Descriptions, University of Helsinki institutional repository Book, Homepage
    3. Tomas Balyo, Florian Lonsing: HordeQBF: A Modular and Massively Parallel QBF Solver, 19th International Conference on Theory and Applications of Satisfiability Testing (SAT) 2016, Paper, Slides, Homepage
  • 2015
    1. Tomas Balyo, Peter Sanders, Carsten Sinz: HordeSat: A Massively Parallel Portfolio SAT Solver, 18th International Conference on Theory and Applications of Satisfiability Testing (SAT) 2015, Paper, Slides, Homepage
    2. Tomas Balyo, Armin Biere, Markus Iser, Carsten Sinz: SAT Race 2015, Artificial Intelligence, volume 241 Paper, Homepage
    3. Tomas Balyo, Roman Bartak: No One SATPlan Encoding To Rule Them All, The Eigth Annual Symposium on Combinatorial Search (SOCS) 2015, Paper, Poster, Slides
  • 2014
    1. Tomas Balyo: Modelling and Solving Problems Using SAT Techniques, PhD thesis, Faculty of Mathematics and Physics, Charles University in Prague, 2014 thesis website
    2. 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
    3. 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
    4. 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
    5. 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.
Design downloaded from free website templates.