Treewidth and its associated tree decompositions underpin efficient algorithms for many hard graph problems—but computing them exactly is NP‑complete, while practical heuristics often trade off accuracy for speed. This project will investigate SAT‑based methods for both exact treewidth computation/decomposition and heuristic, approximate tree decompositions. Building on the SAT/MaxSAT strategies of Berg & Järvisalo (2014), the student will:

Implement & extract:
- Encode the decision problem “tw(G) ≤ k” via incremental SAT and single‑call MaxSAT.
- From satisfying assignments, reconstruct explicit tree decompositions (bags and tree structure).

Develop SAT‑based heuristics:
- Design relaxed encodings to produce good‑quality decompositions in polynomial time.

Evaluation against SOTA solvers:
- Benchmark both exact and heuristic SAT approaches on the PACE 2017 Treewidth competition.

Reference:

Berg, J., Järvisalo, M. “SAT‑Based Approaches to Treewidth Computation: An Evaluation,” ICTAI 2014.

Skills :

• Programming in Python.
• Knowledge of NP-hard problems, their complexities, and their approximations.
• Knowledge of graph algorithms and heuristic optimization

How to Apply
Send your CV and transcript to Sepehr at sepehr.elahi@epfl.ch .