fraSMT

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