Computing optimal hypertree decompositions with SAT

Abstract

Hypertree width is a prominent hypergraph invariant with many algorithmic applications in constraint satisfaction and databases. We propose two novel characterisations for hypertree width in terms of linear orderings. We utilize these characterisations to obtain SAT, MaxSAT, and SMT encodings for computing the hypertree width exactly. We evaluate the encodings on an extensive set of benchmark instances and compare them to state-of-the-art exact methods for computing optimal hypertree width. Our results show that our approach outperforms these state-of-the-art algorithms.