Computing Optimal Hypertree Decompositions with SAT

Computing Optimal Hypertree Decompositions with SAT

Andre Schidler, Stefan Szeider

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence
Main Track. Pages 1418-1424. https://doi.org/10.24963/ijcai.2021/196

Hypertree width is a prominent hypergraph invariant with many algorithmic applications in constraint satisfaction and databases. We propose a novel characterization for hypertree width in terms of linear elimination orderings. We utilize this characterization to generate a new SAT encoding that we evaluate on an extensive set of benchmark instances. We compare it to state-of-the-art exact methods for computing optimal hypertree width. Our results show that the encoding based on the new characterization is not only significantly more compact than known encodings but also outperforms the other methods.
Keywords:
Constraints and SAT: Constraint Satisfaction
Constraints and SAT: Constraints: Modeling, Solvers, Applications
Constraints and SAT: Satisfiability Modulo Theories