FraSMT - A tool for computing the fractional hypertree width of hypergraphs

Bounded fractional hypertree width (fhtw) is the most general known structural property that guarantees polynomial-time solvability of the constraint satisfaction problem. Bounded fhtw generalizes other structural properties like bounded induced width and bounded hypertree width.

FraSMT is the first practical algorithm for computing the fhtw and its associated structural decomposition. FraSMT is based on an efficient encoding of the decomposition problem to SMT (SAT modulo Theory) with Linear Arithmetic as implemented in the SMT solver Z3. The encoding is further strengthened by preprocessing and symmetry breaking methods.

Downloads

The fraSMT tool can be downloaded from this GitHub page.

Benchmark instances can be downloaded from this Zendodo.org page.

Team

Markus Hecher, Johannes Fichte, Neha Lodha, Stefan Szeider

Publications

1 result
2018
[1]An SMT Approach to Fractional Hypertree Width
, , ,
Proceedings of CP 2018, the 24rd International Conference on Principles and Practice of Constraint Programming (John N. Hooker, ed.), volume 11008 of Lecture Notes in Computer Science, pages 109–127, 2018, Springer Verlag.
[bibtex] [pdf] [doi]