Research Project: Modeling and Solving Puzzle Games Using SAT Solving and/or AI Planning

Project still available?

To check whether I still supervise research projects, please check out my main page on research projects.

(I don't post this here so that I don't have to update all my project descriptions in case I don't accept more students.)

Requirements

  • This project can be carried out as 6 pt or as 12 pt project.
  • You don't need background on AI planning as learning that in the first two weeks should be easy. But since this is only a 12 pt or even a 6 pt project (meaning that time is limited) it'd be quite beneficial if you had at least a basic understanding of the respective technology that's being used (i.e., SAT or classical planning) before you start the project. (Still, not strictly required, but it would help if you could work on these foundations before the project formally starts.)
  • This is a project that can be taken by any student, whether your marks are primarily in the pass or in high HD range, it's fun for everybody!

Project Description

TLDR:

In this project we will first decide on a puzzle problem (a list of possible games is given below) as well as on a technology, i.e., SAT (i.e., propositional Logic) or planning. The chosen problem will then be modeled in said technology and solved with state-of-the-art solvers.

The slightly longer version:

Many real-world problems -- such as puzzle games -- are combinatorial problems, where the maximum number of required "actions" is known, it's just not clear which ones need to be taken and which order. (In some cases also the exact number of 'actions' is not known, but we might still have some information available, e.g., which steps must be taken or how many at the most.) Such problems are often NP-complete and can thereby be solved efficiently using AI techniques such as Constraint Satisfaction Problem (CSP) solvers, Integer Linear Programming (ILP) solvers, or Satisfiability (SAT) solvers. They are designed to solve problems that require to find a certain "configuration", or an "assignment" of values to a pre-defined number of variables. All these technologies are thus well-suited to solve a range of puzzle games. Other problems are more suitable to be solved by AI planning technology. Those are problems where one doesn't need to find the correct "configuration", but to find the right sequence of actions (e.g., in the Rubic's cube).

In this project, we will first decide on one or two interesting puzzles or games (feel free to propose something!). Depending on the puzzle(s) and/or game(s) we will decide on an adequate technology (i.e., CSP/ILP/SAT, or planning) and then first model the problem with said technology and then solve it with a state-of-the-art solver from the respective field.

Your task is:

  • Model these games/puzzles in an appropriate description language (CSP, ILP, or SAT) of the respective technology.
  • Translate this formal model into a text-file representation using standard languages used by the respective solvers. This would likely be Minizinc's language in case of SAT/CSP/ILP, and PDDL in case of planning.
  • Conduct an empirical evaluation for all your models with state-of-the-art solvers.
  • Report on the findings (using my LaTeX template for research projects).
  • Depending on how we go, we could write a workshop paper about the created domain.

Further Reading

This project is either on classical planning or SAT solving (or CSPs or ILPs, but they are closely related).

  • For classical planning, you may find my reading recommendations on my page with resources for students helpful. But please don't invest more than a few minutes (if any) before your application, since I don't want you to waste any time before I formally agree to supervise your project. I very strongly advise to listen to (and follow) my hands-on introduction on classical planning that's linked there as well. (If we choose planning to model one of the problems.)
  • For SAT/CSPs/ILPs, I don't have concrete recommendations as of now. (I might add some at time.)

There is a number of puzzle games we could use, and I have already purchased a collection of such games that I can borrow for the time this project is done. The following is a list of problems I already have available:

Note that you can also propose your own game/puzzle!