[Back]

J. Fichte, M. Hecher, N. Lodha, S. Szeider:
"An SMT Approach to Fractional Hypertree Width";
in: "Principles and Practice of Constraint Programming", issued by: Springer Verlag; Springer-Verlag, 2018, 109 - 127.

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.
We propose, implement and test the first practical algorithm for computing the fhtw and its associated structural decomposition. We provide an extensive empirical evaluation of our method on a large class of benchmark instances which also provides a comparison with known exact decomposition methods for hypertree width. Our approach 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. Our experiments show (i) that fhtw can indeed be computed exactly for a wide range of benchmark instances, and (ii) that state-of-the art SMT techniques can be successfully applied for structural decomposition.

FraSMT

https://publik.tuwien.ac.at/files/publik_272151.pdf