SAT-Based Approaches to Treewidth Computation: An Evaluation

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 program-ming, as well as probabilistic inference, for instance. An ob-stacle 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 ap-proaches to practical dedicated exact algorithms for the problem. I