nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology

verfasst von : Markus Hecher, Patrick Thier, Stefan Woltran

Erschienen in: Theory and Applications of Satisfiability Testing – SAT 2020

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Treewidth is one of the most prominent structural parameters. While numerous theoretical results establish tractability under the assumption of fixed treewidth, the practical success of exploiting this parameter is far behind what theoretical runtime bounds have promised. In particular, a naive application of dynamic programming (DP) on tree decompositions (TDs) suffers already from instances of medium width. In this paper, we present several measures to advance this paradigm towards general applicability in practice: We present nested DP, where different levels of abstractions are used to (recursively) compute TDs of a given instance. Further, we integrate the concept of hybrid solving, where subproblems hidden by the abstraction are solved by classical search-based solvers, which leads to an interleaving of parameterized and classical solving. Finally, we provide nested DP algorithms and implementations relying on database technology for variants and extensions of Boolean satisfiability. Experiments indicate that the advancements are promising.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Reasoning About Strong Inconsistency in ASP

Nächstes Kapitel Reducing Bit-Vector Polynomials to SAT Using Gröbner Bases

Source code, instances, and detailed results are available at: tinyurl.com/nesthdb.

Sources: tinyurl.com/projmc;tinyurl.com/pmc-fremont-01-2020.

Abseher, M., Musliu, N., Woltran, S.: htd – a free, open-source framework for (customized) tree decompositions and beyond. In: Salvagnin, D., Lombardi, M. (eds.) CPAIOR 2017. LNCS, vol. 10335, pp. 376–386. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-59776-8_30CrossRefMATH

Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. 40, 353–373 (2011)MathSciNetMATH

Bannach, M., Berndt, S.: Practical access to dynamic programming on tree decompositions. Algorithms 12(8), 172 (2019)MathSciNet

Biere, A.: PicoSAT essentials. JSAT 4(2–4), 75–97 (2008)MATH

Bliem, B., Charwat, G., Hecher, M., Woltran, S.: D-FLAT\({}^{\text{2 }}\): subset minimization in dynamic programming on tree decompositions made easy. Fundam. Inform. 147(1), 27–61 (2016)MathSciNetMATH

Bodlaender, H., Koster, A.: Combinatorial optimization on graphs of bounded treewidth. Comput. J. 51(3), 255–269 (2008)

Burchard, J., Schubert, T., Becker, B.: Laissez-faire caching for parallel #SAT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 46–61. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_5CrossRefMATH

Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y.: Distribution-aware sampling and weighted model counting for SAT. In: AAAI 2014, pp. 1722–1730. The AAAI Press (2014)

Charwat, G., Woltran, S.: Expansion-based QBF solving on tree decompositions. Fundam. Inform. 167(1–2), 59–92 (2019)MathSciNetMATH

10.

Chen, H.: Quantified constraint satisfaction and bounded treewidth. In: ECAI 2004, pp. 161–170. IOS Press (2004)

11.

Codd, E.F.: A relational model of data for large shared data banks. Commun. ACM 13(6), 377–387 (1970)MATH

12.

Cygan, M., et al.: Parameterized Algorithms. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21275-3CrossRefMATH

13.

Darwiche, A.: New advances in compiling CNF to decomposable negation normal form. In: ECAI 2004, pp. 318–322. IOS Press (2004)

14.

Darwiche, A.: SDD: a new canonical representation of propositional knowledge bases. In: IJCAI 2011, pp. 819–826. AAAI Press/IJCAI (2011)

15.

Dell, H., Komusiewicz, C., Talmon, N., Weller, M.: The PACE 2017 parameterized algorithms and computational experiments challenge: the second iteration. In: IPEC 2017, pp. 30:1–30:13. LIPIcs, Dagstuhl Publishing (2017)

16.

Dell, H., Roth, M., Wellnitz, P.: Counting answers to existential questions. In: ICALP 2019. LIPIcs, vol. 132, pp. 113:1–113:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

17.

Diestel, R.: Graph Theory, Graduate Texts in Mathematics, vol. 173, 4th edn. Springer, Heidelberg (2012)

18.

Downey, R.G., Fellows, M.R.: Fundamentals of Parameterized Complexity. TCS. Springer, London (2013). https://doi.org/10.1007/978-1-4471-5559-1CrossRefMATH

19.

Durand, A., Hermann, M., Kolaitis, P.G.: Subtractive reductions and complete problems for counting complexity classes. Theoret. Comput. Sci. 340(3), 496–513 (2005). https://doi.org/10.1016/j.tcs.2005.03.012MathSciNetCrossRefMATH

20.

Eiben, E., Ganian, R., Hamm, T., Kwon, O.: Measuring what matters: a hybrid approach to dynamic programming with treewidth. In: MFCS 2019. LIPIcs, vol. 138, pp. 42:1–42:15. Dagstuhl Publishing (2019)

21.

Ermon, S., Gomes, C.P., Selman, B.: Uniform solution sampling using a constraint solver as an oracle. In: UAI 2012, pp. 255–264. AUAI Press (2012)

22.

Fichte, J.K., Hecher, M., Morak, M., Woltran, S.: Answer set solving with bounded treewidth revisited. In: Balduccini, M., Janhunen, T. (eds.) LPNMR 2017. LNCS (LNAI), vol. 10377, pp. 132–145. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-61660-5_13CrossRef

23.

Fichte, J.K., Hecher, M., Morak, M., Woltran, S.: Exploiting Treewidth for Projected Model Counting and Its Limits. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 165–184. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_11CrossRefMATH

24.

Fichte, J.K., Hecher, M., Thier, P., Woltran, S.: Exploiting database management systems and treewidth for counting. In: Komendantskaya, E., Liu, Y.A. (eds.) PADL 2020. LNCS, vol. 12007, pp. 151–167. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-39197-3_10CrossRef

25.

Fichte, J.K., Hecher, M., Zisser, M.: An improved GPU-based SAT model counter. In: Schiex, T., de Givry, S. (eds.) CP 2019. LNCS, vol. 11802, pp. 491–509. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30048-7_29CrossRef

26.

Ganian, R., Ramanujan, M.S., Szeider, S.: Combining treewidth and backdoors for CSP. In: STACS 2017, pp. 36:1–36:17 (2017). https://doi.org/10.4230/LIPIcs.STACS.2017.36

27.

Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Multi-shot ASP solving with clingo. TPLP 19(1), 27–82 (2019). https://doi.org/10.1017/S1471068418000054MathSciNetCrossRefMATH

28.

Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified Boolean formulas. In: Handbook of Satisfiability, FAIA, vol. 185, pp. 761–780. IOS Press (2009). https://doi.org/10.3233/978-1-58603-929-5-761

29.

Hecher, M., Morak, M., Woltran, S.: Structural decompositions of epistemic logic programs. CoRR abs/2001.04219 (2020). http://arxiv.org/abs/2001.04219

30.

Klebanov, V., Manthey, N., Muise, C.: SAT-based analysis and quantification of information flow in programs. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 177–192. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40196-1_16CrossRef

31.

Kloks, T. (ed.): Treewidth: Computations and Approximations. LNCS, vol. 842. Springer, Heidelberg (1994). https://doi.org/10.1007/BFb0045375CrossRefMATH

32.

Koriche, F., Lagniez, J.M., Marquis, P., Thomas, S.: Knowledge compilation for model counting: affine decision trees. In: IJCAI 2013. The AAAI Press (2013)

33.

Lagniez, J., Marquis, P.: Preprocessing for propositional model counting. In: AAAI 2014, pp. 2688–2694. AAAI Press (2014)

34.

Lagniez, J.M., Marquis, P.: An improved decision-DDNF compiler. In: IJCAI 2017, pp. 667–673. The AAAI Press (2017)

35.

Lagniez, J., Marquis, P.: A recursive algorithm for projected model counting. In: AAAI 2019, pp. 1536–1543. AAAI Press (2019)

36.

Langer, A., Reidl, F., Rossmanith, P., Sikdar, S.: Evaluation of an MSO-solver. In: ALENEX 2012, pp. 55–63. SIAM/Omnipress (2012)

37.

Lonsing, F., Egly, U.: Evaluating QBF solvers: quantifier alternations matter. In: Hooker, J. (ed.) CP 2018. LNCS, vol. 11008, pp. 276–294. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98334-9_19CrossRef

38.

Maniu, S., Senellart, P., Jog, S.: An experimental study of the treewidth of real-world graph data (extended version). CoRR abs/1901.06862 (2019). http://arxiv.org/abs/1901.06862

39.

Muise, C., McIlraith, S.A., Beck, J.C., Hsu, E.I.: Dsharp: fast d-DNNF compilation with sharpSAT. In: Kosseim, L., Inkpen, D. (eds.) AI 2012. LNCS (LNAI), vol. 7310, pp. 356–361. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30353-1_36CrossRef

40.

Niedermeier, R.: Invitation to Fixed-Parameter Algorithms. Oxford Lecture Series in Mathematics and Its Applications, vol. 31. OUP, Oxford (2006)MATH

41.

Oztok, U., Darwiche, A.: A top-down compiler for sentential decision diagrams. In: IJCAI 2015, pp. 3141–3148. The AAAI Press (2015)

42.

Pulina, L., Seidl, M.: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17). Artif. Intell. 274, 224–248 (2019). https://doi.org/10.1016/j.artint.2019.04.002MathSciNetCrossRefMATH

43.

Robertson, N., Seymour, P.D.: Graph minors II: algorithmic aspects of tree-width. J. Algorithms 7, 309–322 (1986)MathSciNetMATH

44.

Samer, M., Szeider, S.: Algorithms for propositional model counting. J. Discrete Algorithms 8(1), 50–64 (2010)MathSciNetMATH

45.

Sang, T., Bacchus, F., Beame, P., Kautz, H., Pitassi, T.: Combining component caching and clause learning for effective model counting. In: SAT 2004 (2004)

46.

Sharma, S., Roy, S., Soos, M., Meel, K.S.: GANAK: a scalable probabilistic exact model counter. In: IJCAI 2019, pp. 1169–1176. ijcai.org (2019)

47.

Tamaki, H.: Positive-instance driven dynamic programming for treewidth. J. Comb. Optim. 37(4), 1283–1311 (2018). https://doi.org/10.1007/s10878-018-0353-zMathSciNetCrossRefMATH

48.

Thurley, M.: sharpSAT – counting models with advanced component caching and implicit BCP. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 424–429. Springer, Heidelberg (2006). https://doi.org/10.1007/11814948_38 CrossRef

49.

Toda, T., Soh, T.: Implementing efficient all solutions SAT solvers. ACM J. Exp. Algorithmics 21(1.12) (2015). Special Issue SEA 2014

Titel: Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology
verfasst von: Markus Hecher
Patrick Thier
Stefan Woltran
Verlag: Springer International Publishing
Buch: Theory and Applications of Satisfiability Testing – SAT 2020
Print ISBN: 978-3-030-51824-0

Electronic ISBN: 978-3-030-51825-7

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-51825-7_25

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"