Computing Optimal Hypertree Decompositions with SAT

Andre Schidler; Stefan Szeider

IJCAI 2021poster19 citations

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 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.

Constraints and SAT: Constraint SatisfactionConstraints and SAT: Constraints: Modeling, Solvers, ApplicationsConstraints and SAT: Satisfiability Modulo Theories

BibTeX

@inproceedings{ijcai2021p196,
  title     = {Computing Optimal Hypertree Decompositions with SAT},
  author    = {Schidler, Andre and Szeider, Stefan},
  booktitle = {Proceedings of the Thirtieth International Joint Conference on
               Artificial Intelligence, {IJCAI-21}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Zhi-Hua Zhou},
  pages     = {1418--1424},
  year      = {2021},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2021/196},
  url       = {https://doi.org/10.24963/ijcai.2021/196},
}