An SMT Approach to Fractional Hypertree Width

  • Johannes K. FichteEmail author
  • Markus HecherEmail author
  • Neha LodhaEmail author
  • Stefan SzeiderEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11008)


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

We propose, implement and test the first practical algorithm for computing the Open image in new window 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  Open image in new window . The encoding is further strengthened by preprocessing and symmetry breaking methods. Our experiments show (i) that  Open image in new window 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.


  1. 1.
    Alviano, M., Dodaro, C.: Anytime answer set optimization via unsatisfiable core shrinking. Theory Pract. Log. Program. 16(5–6), 533–551 (2016)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Arocena, P.C., Glavic, B., Ciucanu, R., Miller, R.J.: The iBench integration metadata generator. In: Li, C., Markl, V. (eds.) Proceedings of Very Large Data Bases (VLDB) Endowment, vol. 9:3, pp. 108–119. VLDB Endowment, November 2015. Scholar
  3. 3.
    Audemard, G., Boussemart, F., Lecoutre, C., Piette, C.: XCSP3: An XML-Based Format Designed to Represent Combinatorial Constrained Problems. (2016)
  4. 4.
    Bannach, M., Berndt, S., Ehlers, T.: Jdrasil: a modular library for computing tree decompositions. In: Iliopoulos, C.S., Pissis, S.P., Puglisi, S.J., Raman, R. (eds.) 16th International Symposium on Experimental Algorithms, SEA 2017, 21–23 June 2017, London, UK, LIPIcs, vol. 75, pp. 28:1–28:21. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)Google Scholar
  5. 5.
    Benedikt, M., Konstantinidis, G., Mecca, G., Motik, B., Papotti, P., Santoro, D., Tsamoura, E.: Benchmarking the chase. In: Geerts, F. (ed.) Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2017), pp. 37–52. Association for Computing Machinery, New York, Chicago (2017).
  6. 6.
    Berg, J., Lodha, N., Järvisalo, M., Szeider., S.: MaxSAT benchmarks based on determining generalized hypertree-width. Technical report, MaxSAT Evaluation 2017 (2017)Google Scholar
  7. 7.
    Berg, J., Järvisalo, M.: SAT-based approaches to treewidth computation: an evaluation. In: 26th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2014, Limassol, Cyprus, 10–12 November 2014, pp. 328–335. IEEE Computer Society (2014)Google Scholar
  8. 8.
    Bodlaender, H.L.: A partial \(k\)-arboretum of graphs with bounded treewidth. Theoret. Comput. Sci. 209(1–2), 1–45 (1998)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Bodlaender, H.L., Möhring, R.H.: The pathwidth and treewidth of cographs. SIAM J. Discrete Math. 6(2), 181–188 (1993)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Carbonnel, C., Cooper, M.C.: Tractability in constraint satisfaction problems: a survey. Constraints 21(2), 115–144 (2016)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Cohen, D., Jeavons, P., Gyssens, M.: A unified theory of structural tractability for constraint satisfaction problems. J. Comput. Syst. Sci. 74(5), 721–743 (2008)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Committee, M.S.: IEEE standard for floating-point arithmetic. IEEE Std 754-2008, pp. 1–70, August 2008Google Scholar
  13. 13.
    Dechter, R.: Tractable structures for constraint satisfaction problems. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, vol. I, chap. 7, pp. 209–244. Elsevier (2006)Google Scholar
  14. 14.
    Dell, H., Komusiewicz, C., Talmon, N., Weller, M.: The PACE 2017 parameterized algorithms and computational experiments challenge: the second iteration. In: Lokshtanov, D., Nishimura, N. (eds.) Proceedings of the 12th International Symposium on Parameterized and Exact Computation (IPEC 2017), pp. 30:1–30:13. LIPIcs (2017)Google Scholar
  15. 15.
    Durand, A., Mengel, S.: Structural tractability of counting of solutions to conjunctive queries. Theoret. Comput. Sci. 57(4), 1202–1249 (2015)MathSciNetzbMATHGoogle Scholar
  16. 16.
    Fichte, J.K., Hecher, M., Lodha, N., Szeider, S.: A Benchmark Collection of Hypergraphs, June 2018.
  17. 17.
    Fichte, J.K., Hecher, M., Lodha, N., Szeider, S.: Analyzed Benchmarks and Raw Data on Experiments for FraSMT, June 2018.
  18. 18.
    Fichte, J.K., Lodha, N., Szeider, S.: SAT-based local improvement for finding tree decompositions of small width. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 401–411. Springer, Cham (2017). Scholar
  19. 19.
    Fischl, W., Gottlob, G., Longo, D.M., Pichler, R.: HyperBench: A Benchmark of Hypergraphs (2017).
  20. 20.
    Fischl, W., Gottlob, G., Pichler, R.: Proceedings of the 37th ACM SIGMOD-SIGACT-SIGAI symposium on principles of database systems. In: den Bussche, J.V., Arenas, M. (eds.) Conference SIGMOD/PODS 2018 International Conference on Management of Data, Houston, TX, USA, 10–15 June 2018, pp. 17–32. ACM (2018)Google Scholar
  21. 21.
    Freuder, E.C.: A sufficient condition for backtrack-bounded search. J. ACM 29(1), 24–32 (1982)CrossRefGoogle Scholar
  22. 22.
    Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Multi-shot ASP Solving with Clingo. CoRR abs/1705.09811 (2017).
  23. 23.
    Geerts, F., Mecca, G., Papotti, P., Santoro, D.: Mapping and cleaning. In: Cruz, I., Ferrari, E., Tao, Y. (eds.) Proceedings of the IEEE 30th International Conference on Data Engineering (ICDE 2014), pp. 232–243, March 2014Google Scholar
  24. 24.
    Gottlob, G., Leone, N., Scarcello, F.: Hypertree decompositions and tractable queries. J. Comput. Syst. Sci. 64(3), 579–627 (2002)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Gottlob, G., Leone, N., Scarcello, F.: On tractable queries and constraints. In: Bench-Capon, T.J.M., Soda, G., Tjoa, A.M. (eds.) DEXA 1999. LNCS, vol. 1677, pp. 1–15. Springer, Heidelberg (1999). Scholar
  26. 26.
    Gottlob, G., Samer, M.: A backtracking-based algorithm for hypertree decomposition. J. Exp. Alg. 13, 1:1.1–1:1.19 (2009)MathSciNetCrossRefGoogle Scholar
  27. 27.
    Grohe, M., Marx, D.: Constraint solving via fractional edge covers. In: Proceedings of the of the 17th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 2006), pp. 289–298. ACM Press (2006)Google Scholar
  28. 28.
    Grohe, M., Marx, D.: Constraint solving via fractional edge covers. ACM Trans. Alg. 11(1) (2014). Article 4, 20Google Scholar
  29. 29.
    Guo, Y., Pan, Z., Heflin, J.: LUBM Benchmark OWL Knowl. Base Syst. Web semantics: science, services and agents on the world wide web 3(2), 158–182 (2005)CrossRefGoogle Scholar
  30. 30.
    Hagberg, A.A., Schult, D.A., Swart, P.J.: Exploring network structure, dynamics, and function using networkx. In: Gäel Varoquaux, T.V., Millman, J. (eds.) Proceedings of the 7th Python in Science Conference (SciPy 2008), Pasadena, CA, USA, pp. 11–15, August 2008Google Scholar
  31. 31.
    Kaminski, R., Schneider, M., Rabener, T., et al.: Benchmark-Tool (2017).
  32. 32.
    Khamis, M.A., Ngo, H.Q., Rudra, A.: FAQ: questions asked frequently. In: Milo, T., Tan, W. (eds.) Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS 2016, San Francisco, CA, USA, June 26–July 01 2016. pp. 13–28. Association for Computer Machinery, New York (2016)Google Scholar
  33. 33.
    Khamis, M.A., Ngo, H.Q., Rudra, A.: FAQ: questions asked frequently. CoRR abs/1504.04044 (2017). Full version of [32]
  34. 34.
    Leis, V., Gubichev, A., Mirchev, A., Boncz, P., Kemper, A., Neumann, T.: How good are query optimizers, really? Proc. Very Large Data Bases (VLDB) Endow. 9(3), 204–215 (2015)CrossRefGoogle Scholar
  35. 35.
    Lodha, N., Ordyniak, S., Szeider, S.: A SAT approach to branchwidth. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 179–195. Springer, Cham (2016). Scholar
  36. 36.
    Lodha, N., Ordyniak, S., Szeider, S.: SAT-encodings for special treewidth and pathwidth. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 429–445. Springer, Cham (2017). Scholar
  37. 37.
    Marx, D.: Approximating fractional hypertree width. TALG 6(2) (2010). Article 17, 29MathSciNetCrossRefGoogle Scholar
  38. 38.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). Scholar
  39. 39.
    Rose, D.J.: On simple characterizations of \(k\)-trees. Discrete Math. 7, 317–322 (1974)MathSciNetCrossRefGoogle Scholar
  40. 40.
    van Rossum, G.: Python tutorial. CS-R9526, Centrum voor Wiskunde en Informatica (CWI), Amsterdam, May 1995Google Scholar
  41. 41.
    Roussel, O.: Controlling a solver execution with the runsolver tool. J. Satisfiability Boolean Model. Comput. 7, 139–144 (2011)MathSciNetzbMATHGoogle Scholar
  42. 42.
    Samer, M., Veith, H.: Encoding treewidth into SAT. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 45–50. Springer, Heidelberg (2009). Scholar
  43. 43.
    Transaction Processing Performance Council (TPC): TPC-H decision support benchmark. Technical report, TPC (2014).

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.International Center of Computational LogicTU DresdenDresdenGermany
  2. 2.Database and Artificial Intelligence GroupTU WienViennaAustria
  3. 3.Algorithms and Complexity GroupTU WienViennaAustria

Personalised recommendations