Arrow Research search
Back to SAT

SAT 2020

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

Conference Paper Accepted Paper Logic in Computer Science ยท Satisfiability

Abstract

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.

Authors

Keywords

No keywords are indexed for this paper.

Context

Venue
International Conference on Theory and Applications of Satisfiability Testing
Archive span
2003-2025
Indexed papers
824
Paper id
451113366442777433