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