@inproceedings{BergJ:ICTAI2014,
author = {Jeremias Berg and Matti J\"arvisalo},
title = {{SAT}-Based Approaches to Treewidth Computation: An Evaluation},
booktitle = {Proceedings of the 2014 IEEE 26th International Conference on 
             Tools with Artificial Intelligence (ICTAI 2014)},
pages = {328--335},
year = {2014},
publisher = {IEEE Computer Society}
}

Abstract:

Treewidth is an important structural property of graphs, tightly 
connected to computational tractability in eg various constraint 
satisfaction formalisms such as constraint programming, Boolean 
satisfiability, and answer set programming, as well as probabilistic 
inference, for instance. An obstacle to harnessing treewidth as a way to 
efficiently solving bounded treewidth instances of NP-hard problems is 
that deciding treewidth, and hence computing an optimal 
tree-decomposition, is in itself an NP-complete problem. In this paper, 
we study the applicability of Boolean satisfiability (SAT) based 
approaches to determining the treewidths of graphs, and at the same time 
obtaining an associated optimal tree-decomposition. Extending earlier 
studies, we evaluate various SAT and MaxSAT based strategies for 
treewidth computation, and compare these approaches to practical 
dedicated exact algorithms for the problem.