key: cord-0046687-401tdbjo
authors: Hecher, Markus; Thier, Patrick; Woltran, Stefan
title: Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology
date: 2020-06-26
journal: Theory and Applications of Satisfiability Testing - SAT 2020
DOI: 10.1007/978-3-030-51825-7_25
sha: 6ae4dc493fd6e73b6b75da11e328dc3cf912dcdd
doc_id: 46687
cord_uid: 401tdbjo

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.

Treewidth [43] is a prominent structural parameter, originating from graph theory and is well-studied in the area of parameterized complexity [6, 18, 40] . For several problems hard for complexity class NP, there are results [12] showing socalled (fixed-parameter) tractability, which indicates a fixed-parameter tractable (FPT) algorithm running in polynomial time assuming that a given parameter (e.g., treewidth) is fixed. Practical implementations exploiting treewidth include generic frameworks [3, 5, 36] , but also dedicated solvers that deal with problems ranging from (counting variants of) Boolean satisfiability (Sat) [25] , over generalizations thereof [9, 10] based on Quantified Boolean Formulas (QBFs), to formalisms relevant to knowledge representation and reasoning [22] . For Sat, these solvers are of particular interest as there is a well-known correspondence between treewidth and resolution width [2] . QBFs extend Boolean logic by explicit universal and existential quantification over variables, which has applications in formal verification, synthesis, and AI problems such as planning [28] . Some of these parameterized solvers are particularly efficient for certain fragments [37] , and even successfully participated in problem-specific competitions [42] .

Most of these systems are based on dynamic programming (DP), where a tree decomposition (TD) is traversed in a post-order, i.e., from the leaves towards the root, and thereby for each TD node tables are computed. The size of these tables (and thus the computational efforts required) are bounded by a function in the treewidth of the instance. Although dedicated competitions [15] for treewidth advanced the state-of-the-art for efficiently computing treewidth and TDs [1, 47] , these DP approaches reach their limits when instances have higher treewidth; a situation which can even occur in structured real-world instances [38] . Nevertheless in the area of Boolean satisfiability, this approach proved to be successful for counting problems, such as, e.g., (weighted) model counting [24, 25, 44] and projected model counting [23] .

To further increase the applicability of this paradigm, novel techniques are required which (1) rely on different levels of abstraction of the instance at hand; (2) treat subproblems originating in the abstraction by standard solvers whenever widths appear too high; and (3) use highly sophisticated data management in order to store and process tables obtained by dynamic programming.

Contributions. Above aspects are treated as follows.

1. To tame the beast of high treewidth, we propose nested dynamic programming, where only parts of an abstraction of a graph are decomposed. Then, each TD node also needs to solve a subproblem residing in the graph, but may involve vertices outside the abstraction. In turn, for solving such subproblems, the idea of nested DP is to subsequently repeat decomposing and solving more fine-grained graph abstractions in a nested fashion. This results not only in elegant DP algorithms, but also allows to deal with high treewidth. While candidates for obtaining abstractions often originate naturally from the problem, nested DP may require non-obvious sub-abstractions, for which we present a generic solution. 2. To further improve the capability of handling high treewidth, we show how to apply nested DP in the context of hybrid solving, where established, standard solvers (e.g., Sat solvers) and caching are incorporated in nested DP such that the best of two worlds are combined. Thereby, structured solving is applied to parts of the problem instance subject to counting or enumeration, while depending on results of subproblems. These subproblems (subject to search) reside in the abstraction only, and are solved via standard solvers. 3. We implemented a system based on a recently published tool called dpdb [24] for using database management systems (DBMS) to efficiently perform table manipulation operations needed during DP. Our system uses and significantly extends this tool in order to perform hybrid solving, thereby combining nested DP and standard solvers. As a result, we use DBMS for efficiently implementing the handling of tables needed by nested DP. Preliminary experiments indicate that nested DP with hybrid solving can be fruitful.

We exemplify these ideas on the problem of Projected Model Counting (#∃Sat) and discuss adaptions for other problems. 

Projected Model Counting. We define Boolean formulas in the usual way, cf., [28] . A literal is a Boolean variable x or its negation ¬x. A (CNF) formula ϕ is a set of clauses interpreted as conjunction. A clause is a set of literals interpreted as disjunction. For a formula or clause X, we abbreviate by var(X) the variables that occur in X. (ϕ)). #∃Sat is #·NP-complete [19] and thus probably harder than #Sat (#P-complete).

Tree Decomposition and Treewidth. We assume familiarity with graph terminology, cf., [17] . A tree decomposition (TD) [43] of a given graph G is a pair T = (T, χ) where T is a rooted tree and χ assigns to each node

such that s lies on the path from r to t, we have χ(r) ∩ χ(t) ⊆ χ(s). We let width(T ) := max t∈V (T ) |χ(t)| − 1. The treewidth tw(G) of G is the minimum width(T ) over all TDs T of G. For a node t ∈ V (T ), we say that type(t) is leaf if t has no children and χ(t) = ∅; join if t has children t and t with t = t and χ(t) = χ(t ) = χ(t ); intr ("introduce") if t has a single child t , χ(t ) ⊆ χ(t) and |χ(t)| = |χ(t )| + 1; rem ("removal") if t has a single child t , χ(t ) ⊇ χ(t) and |χ(t )| = |χ(t)| + 1. If for every node t ∈ V (T ), type(t) ∈ {leaf, join, intr, rem}, the TD is called nice. A nice TD can be computed from a given TD T in linear time without increasing the width [31] , assuming the width of T is fixed. Figure 1 depicts a graph G and a (non-nice) TD T of G of width 2.

Relational Algebra. We formalize DP algorithms by means of relational algebra [11] , similar to related work [24] . A table τ is a finite set of rows r over a set att(τ ) of attributes. Each row r ∈ τ is a set of pairs (a, v) with a ∈ att(τ ) and v in domain dom(a) of a, s.t. for each a ∈ att(τ ) there is exactly one (a, v) ∈ r.

Notably, apart from counters we use mainly binary domains in this paper. Selection of rows in τ according to a Boolean formula ϕ is defined by σ ϕ (τ ) := {r | r ∈ τ, ϕ[ass(r)] = ∅}, assuming that ass(r) refers to the truth assignment over the attributes of binary domain of a given row r ∈ τ. Given a relation τ Listing 1: Table algorithm #Satt(χt, ϕt, τ1, . . . , τ ) for solving #Sat on node t of a nice tree decomposition, cf., [24] .

In: Bag χt, bag formula ϕt, child tables τ1, . . . τ of t. Out: Table τt . 1 if type(t) = leaf then τt := {{(cnt, 1)}} 2 else if type(t) = intr, and a ∈ χt is introduced then 3 τt := τ1 ϕ t {{(a, 0)}, {(a, 1)}} 4 else if type(t) = rem, and a ∈ χt is removed then

with att(τ )∩att(τ ) = ∅, we refer to the cross-join by τ ×τ := {r∪r | r ∈ τ, r ∈ τ }. Further, a join (using ϕ) corresponds to τ ϕ τ := σ ϕ (τ × τ ). We define renaming of τ , given a set A of attributes, and a bijective mapping m :

This is lifted to extended projectionΠ A,(a←f ) , assuming attribute a ∈ att(τ ) \ A and arithmetic

We use aggregation by grouping A G (a←g) , where we assume A ⊆ att(τ ), a ∈ att(τ ) \ A and an aggregate function g :

A solver based on dynamic programming (DP) evaluates a given input instance I in parts along a given TD of a graph representation G of the instance. Thereby, for each node t of the TD, intermediate results are stored in a table τ t . This is achieved by running a so-called table algorithm, which is designed for a certain graph representation, and stores in τ t results of problem parts of I, thereby considering tables τ t for child nodes t of t. DP works for many problems:

3. Traverse the nodes of T in post-order (bottom-up tree traversal of T ). At every node t of T during post-order traversal, execute a table algorithm that takes as input bag χ(t), a certain bag instance I t depending on the problem, as well as previously computed child tables of t. Then, the results of this execution are stored in table τ t . 4. Finally, interpret table τ n for the root node n of T in order to output the solution to the problem for instance I.

Having relational algebra and this paradigm at hand, we exemplarily show how to solve #Sat, required for solving #∃Sat later. To this end, we need the following graph representation for a given formula ϕ. The primal graph G ϕ [44] of a formula ϕ has as vertices its variables, where two variables are joined by an edge if they occur together in a clause of ϕ. Given a TD T = (T, χ) of G ϕ and a node t of T . Then, we let bag instance ϕ t of ϕ, called bag formula, be the clauses { c | c ∈ ϕ, var(c) ⊆ χ(t) } entirely covered by the bag χ(t). Now, the only ingredient that is still missing for solving #Sat via dynamic programming along a given TD, is the table algorithm #Sat t . For brevity, table algorithm #Sat t as presented in Listing 1 shows the four cases corresponding to the four node types of a nice TD, as any TD node forms just an overlap of these four cases. Each table τ t consists of rows using attributes χ(t) ∪ {cnt}, representing an assignment of ϕ t and cnt is a counter. Then, the table τ t for a leaf node t, where type(t) = leaf, consists of the empty assignment and counter 1, cf., Line 1. For nodes t with introduced variable a ∈ χ(t), we guess in Line 3 for each assignment of the child table, whether a is set to true or to false, and ensure that ϕ t is satisfied. When an atom a is removed in a remove node t, we project assignments of child tables to χ(t), cf., Line 5, and sum up counters of the same assignments. For join nodes, counters of equal assignments are multiplied (Line 7). Fig. 1 is the primal graph G ϕ and that there are 6 satisfying assignments of ϕ. We discuss selected cases of running algorithm #Sat t on each node t of TD T nice of Fig. 2 in post-order, thereby evaluating ϕ in parts. Observe that type(t 1 ) = leaf. 1 )}} (two possible truth assignments for x), cf., Line 3, which is cross-joined with {{(a, 0)}, {(a, 1)}}, and then with {{(y, 0)}, {(y, 1)}}. Then, for node t 4 we additionally filter, cf., Line 3, those rows, where ϕ t4 = {c 1 , c 2 } is satisfied and obtain table τ 4 . Node t 5 is of type(t 5 ) = rem, where a is removed, i.e., by the properties of TDs, it is guaranteed that all clauses of ϕ using a are checked below t 5 and that no clause involving a will occur above t 4 . Consequently, τ 5 is obtained from τ 4 by projecting to {x, y} and summing up the counters cnt of rows of equal assignments correspondingly, cf., Line 5. Similarly, one proceeds with τ 6 and the right part of the tree, obtaining tables τ 7 − τ 10 . In node t 11 , we join common assignments of tables τ 6 and τ 10 , and multiply counters cnt accordingly. Finally, we obtain 6 satisfying assignments, as expected. In all the tables the corresponding parts of assignment I, where x, y, b are set to 1 and a is set to 0 are highlighted.

Although these tables obtained via table algorithms might be exponential in size, the size is bounded by the width of the given TD of the primal graph G ϕ . Still, practical results of such algorithms show competitive behaviour [3, 25] up to a certain width. As a result, instances with high (tree-)width seem out of reach. Even further, if we lift the table algorithm #Sat t in order to solve problem #∃Sat, we are double exponential in the treewidth [23] and suffer from a rather complicated algorithm. To mitigate these issues, we present a novel approach to deal with high treewidth, by nesting of DP on abstractions of G ϕ . As we will see, this not only works for #Sat, but also for #∃Sat with adaptions. 

Assume that a set U of variables of ϕ, called nesting variables, appears uniquely in one TD node t. Then, one could do DP on the TD as before, but no truth value for any variable in U is stored. Instead, clauses involving U could be evaluated by nested DP within node t, since variables U appear uniquely in t. Indeed, for DP on the other (non-nesting) variables, only the result of this evaluation is essential. Now, before we can apply nested DP, we need abstractions with room for choosing nesting variables between the empty set and the set of all the variables. Inspired by related work [16, 20, 26, 29] , we define the nested primal graph N A ϕ for a given formula ϕ and a given set A ⊆ var(ϕ) of abstraction variables. To this end, we say a path P in primal graph G ϕ is a nesting path (between u and v) using

Then, the vertices of nested primal graph N A ϕ correspond to A and there is an edge between two vertices u, v ∈ A if there is a nesting path between u and v. Observe that the nested primal graph only consists of abstraction variables and, intuitively, "hides" nesting variables in nesting paths of primal graph G ϕ .

Example 3. Recall formula ϕ and primal graph G ϕ of Example 2. Given abstraction variables A = {x, y}, nesting paths of G ϕ are, e.g.,

The nested primal graph provides abstractions of needed flexibility for nested DP. Indeed, if we set abstraction variables to A = var(ϕ), we end up with full DP and zero nesting, whereas setting A = ∅ results in full nesting, i.e., nesting of all variables. Intuitively, the nested primal graph ensures that clauses subject to nesting (containing nesting variables) can be safely evaluated in exactly one node of a TD of the nested primal graph. To formalize this, we let nestReach(U ) Listing 2: Algorithm HybDP #∃Sat (depth, ϕ, P , A ) for hybrid solving of #∃Sat by nested DP with abstraction variables A .

In: Nesting depth ≥ 0, formula ϕ, projection variables P ⊆ var(ϕ), and abstraction variables A ⊆ var(ϕ). Out: Number #∃Sat(ϕ, P ) of assignments.

cache ← cache ∪{(ϕ, #∃Sat(ϕ, P ))} By construction any nesting variable is in at least one compatible set. However, (1) a nesting variable could be even in several compatible sets, and (2) a compatible set could be compatible with several nodes of T . Hence, to allow nested evaluation, we need to ensure that each nesting variable is evaluated only in one unique node t. As a result, we formalize for every compatible set U that is 

) Function ass refers to the respective truth assignment I: χt → {0, 1} of a given row r ∈ τt.

subset-minimal, a unique node t compatible with U , denoted by comp(U ) := t. For simplicity of our algorithms, we assume these unique nodes for U are introduce nodes, i.e., type(t) = intr. We denote the union of all compatible sets U where comp(U ) = t, by nested bag variables χ A t . Then, the nested bag formula

where formula ϕ t is defined above. Observe that T is T , but restricted to A and that T is a TD of N A ϕ of width 1. Observe that only for compatible set U = {b, x} we have two nodes compatible with U , namely t 2 and t 3 . We assume comp(U ) = t 2 . Consequently, nested bag formulas are ϕ A t1 = {c 1 , c 2 }, ϕ A t2 = {c 3 , c 4 }, and ϕ A t3 = ∅. Assume any TD T of N A ϕ using any set A of abstraction variables. Observe that the definitions of nested primal graph and nested bag formula ensure that any set S of vertices connected via edges in G ϕ will "appear" among nested bag variables of some node of T . Even more stringent, each variable a ∈ var(ϕ) \ A appears only in nested bag formula ϕ A t of node t unique for a. These unique variable appearances allow to nest evaluating ϕ A t under some assignment to χ(t).

Now, we have definitions at hand to discuss nested DP in the context of hybrid solving, which combines using both standard solvers and parameterized solvers exploiting treewidth. We first illustrate the ideas for the problem #∃Sat and then discuss possible generalizations in Sect. 3.3; a concrete implementation is presented in Sect. 4. Listing 2 depicts our algorithm HybDP #∃Sat for solving #∃Sat. Note that the recursion is indirect in Line 18 through Line 4 of Listing 3 (discussed later). Block (1) spans Lines 1-3 and performs Boolean conflict propagation and preprocessing, thereby obtaining projection variables P ⊆ P (preserving satisfying assignments w.r.t. P ), sets A to A ∩ P in Line 2, and consolidates cache with the updated formula ϕ. If ϕ is not cached, we do standard solving if the width is out-of-reach for nested DP in Block (2), spanning Lines 4-10. More concretely, if ϕ does not contain projection variables, we employ a Sat solver returning integer 1 or 0. If ϕ contains projection variables and either the width obtained by heuristically decomposing G ϕ is above threshold hybrid , or the nesting depth exceeds threshold depth , we use a standard #Sat or #∃Sat solver depending on var(ϕ) ∩ P . Block (3) spans Lines 11-13 and is reached if no cache entry was found in Block (1) and standard solving was skipped in Block (2) . If the width of the computed decomposition is above threshold abstr , we need to use an abstraction in form of the nested primal graph. This is achieved by choosing suitable subsets E ⊆ A of abstraction variables and decomposing ϕ E t heuristically. Finally, Block (4) concerns nested DP, cf., Lines 14-20. This block relies on nested table algorithm #∃Sat t , which takes parameters similar to table algorithm #Sat t , but additionally requires the nested bag formula for current node t, projection variables P and abstraction variables. Nested table algorithm #∃Sat t is sketched in Listing 3 and recursively calls for each row r ∈ τ t , HybDP #∃Sat on nested bag formula ϕ A t simplified by the assignment ass(r) of the current row r. This is implemented in Line 4 by using extended projection, cf., Listing 1, where the count cnt of the respective row r is updated by multiplying the result of the recursive call HybDP #∃Sat . Notably, as the recursive call HybDP #∃Sat within extended projection of Line 4 implicitly takes a given current row r, the function occurrences ass in Line 4 implicitly take this row r as an argument. As a result, our approach deals with high treewidth by recursively finding and decomposing abstractions of the graph. If the treewidth is too high for some parts, TDs of abstractions are used to guide standard solvers. 

,A ) (τt) 5 else if type(t) = rem, and a ∈ χt is removed then 6 

) The cardinality of a table τ can be obtained via relational algebra (sub-expression):

Consequently, the solution to #∃Sat is 2. Figure 3 (left) shows TD T of N A ϕ and tables obtained by HybDP #∃Satt (ϕ, P, A) for solving projected model counting on ϕ and P . Note that the same example easily works for #Sat, where P = var(ϕ).

Algorithm #∃Sat t of Listing 3 works similar to algorithm #Sat t , but uses attribute "cnt" for storing (projected) counts accordingly. We briefly discuss executing #∃Sat t1 in the context of Line 18 of algorithm HybDP #∃Satt on node t 1 of T , resulting in table τ 1 as shown in Fig. 3 (3), in particular in Lines 11-13. The proof proceeds by structural induction on ϕ. By construction, we have (B): Every variable of var(ϕ) \ A occurs in some nested bag formula ϕ A t as used in the call to #∃Sat t in Line 18 for a unique node t of T . Observe that #∃Sat t corresponds to #Sat t , whose correctness is established via invariants, cf., [24, 44] , only Line 4 differs. In Line 4 of #∃Sat t , HybDP #∃Sat is called recursively on subformulas ϕ A t [ass(r)] for each r ∈ τ t . By induction hypothesis, we have (C): these calls result to #∃Sat(ϕ A t [ass(r)], P ∩ var(ϕ A t [ass(r)])) for each r ∈ τ t . By (A), #∃Sat t as called in Line 18 stores only table attributes in χ t ⊆ A ⊆ P . Thus, by (C), recursive calls can be subsequently multiplied to cnt for each r ∈ τ t .

Nested DP as proposed above is by far not restricted to (projected) model counting, or counting problems in general. In fact, one can easily generalize nested DP to other relevant formalisms, briefly sketched for the QBF formalism.

We assume QBFs of the form ϕ = ∃V 1 .∀V 2 . . . . ∃V .γ using quantifiers ∃, ∀, where γ is a CNF formula and var(ϕ) = var(γ) = V 1 ∪ V 2 · · · ∪ V . Given QBF ϕ = Q V.ψ with Q ∈ {∃, ∀}, we let qvar(ϕ) := V . For an assignment I :

Hybrid solving by nested DP can be extended to problem QSat. To the end of using this approach for QBFs, we define the primal graph G ϕ for a QBF ϕ = ∃V 1 .∀V 2 . . . . ∃V .γ analogously to the primal graph of a Boolean formula, i.e., G ϕ := G γ . Consequently, also the nested primal graph is defined for a given set A ⊆ var(ϕ) by N A ϕ := N A γ . Now, let A ⊆ var(ϕ) be a set of abstraction variables, and T = (T, χ) be a TD of N A ϕ and t be a node of T . Then, the bag QBF ϕ t is given by ϕ t := ∃V 1 .∀V 2 . . . . ∃V .γ t and the nested bag QBF ϕ A t for a set A ⊆ var(ϕ) amounts to ϕ A t := ∃V 1 .∀V 2 . . . . ∃V .γ A t . Algorithm HybDP QSat is similar to HybDP #∃Sat of Listing 2, where the projection variables parameter P is removed since P constantly coincides with variables qvar(ϕ) of the outermost quantifier. Further, Line 4 is removed, Lines 8 and 9 are replaced by calling a QSat solver and nested table algorithm #∃Sat t of Line 18 is replaced by nested table algorithm QSat t as presented in Listing 4. Algorithm QSat t is of similar shape as algorithm #∃Sat t , cf., Listing 3, but does not maintain counts cnt. Further, Line 4 of algorithm QSat t intuitively filters τ t fulfilling the outer-most quantifier, and keeps those rows r of τ t , where the recursive call to HybDP QSat on nested bag formula simplified by the assignment ass(r) of r succeeds. For ensuring that the outer-most quantifier Q is fulfilled, we are either in the situation that Q = ∃, which immediately is fulfilled for every row r in τ t since r itself serves as a witness. If Q = ∀, we need to check that τ t contains 2 |χ(t)| many (all) rows. The cardinality of table τ t can be computed via a sub-expression of relational algebra as hinted in the footnote of Listing 4. Notably, if Q = ∀, we do not need to check in Line 8 of Listing 4, whether all rows sustain in table τ t since this is already ensured for both child tables τ 1 , τ 2 of t. Then, if in the end the table for the root node of T is not empty, it is guaranteed that either the table contains some (if Q = ∃) or all (if Q = ∀) rows and that ϕ is valid. Note that algorithm QSat t can be extended to also consider more fine-grained quantifier dependency schemes.

Compared to other algorithms for QSat using treewidth [9, 10] , hybrid solving based on nested DP is quite compact without the need of nested tables. Instead of rather involved data structures (nested tables), we use here plain tables that can be handled by modern database systems efficiently.

We implemented a hybrid solver nestHDB 1 based on nested DP in Python3 and using table manipulation techniques by means of SQL and the database management system (DBMS) Postgres. Our solver builds upon the recently published prototype dpdb [24] , which applied a DBMS for plain dynamic programming algorithms. However, we used the most-recent version 12 of Postgres and we let it operate on a tmpfs-ramdisk. In our solver, the DBMS serves the purpose of extremely efficient in-memory table manipulations and query optimization required by nested DP, and therefore nestHDB benefits from database technology.

Nested DP & Choice of Standard Solvers. We implemented dedicated nested DP algorithms for solving #Sat and #∃Sat, where we do (nested) DP up to threshold depth = 2. Further, we set threshold hybrid = 1000 and therefore we do not "fall back" to standard solvers based on the width (cf., Line 7 of Listing 2), but based on the nesting depth.

Also, the evaluation of the nested bag formula is "shifted" to the database if it uses at most 40 abstraction variables, since Postgres efficiently handles these small-sized Boolean formulas. Thereby, further nesting is saved by executing optimized SQL statements within the TD nodes. A value of 40 seems to be a nice balance between the overhead caused by standard solvers for small formulas and exponential growth counteracting the advantages of the DBMS. For hybrid solving, we use #Sat solver sharpSAT [48] and for #∃Sat we employ the recently published #∃Sat solver projMC [35] , solver sharpSAT and Sat solver picosat [4] . Observe that our solver immediately benefits from better standard solvers and further improvements of the solvers above.

TDs are computed by means of heuristics via decomposition library htd [1] . For finding good abstractions (crucial), i.e., abstraction variables for the nested primal graph, we use encodings for solver clingo [27] , which is based on logic programming (ASP) and therefore perfectly suited for solving reachability via nesting paths. There, among a reasonably sized subset of vertices of smallest degree, we aim for a preferably large (maximal) set A of abstraction variables such that at the same time the resulting graph N A ϕ is reasonably sparse, which is achieved by minimizing the number of edges of N A ϕ . To this end, we use built-in (cost) optimization, where we take the best results obtained by clingo after running at most 35 s. For the concrete encodings used in nestHDB, we refer to the online repository as stated above. We expect that this initial approach can be improved and that extending by problem-specific as well as domain-specific information might help in choosing promising abstraction variables A.

As rows of tables during (nested) DP can be independently computed and parallelized [25] , hybrid solver nestHDB potentially calls standard solvers for solving subproblems in parallel using a thread pool. Thereby, the uniquely compatible node for relevant compatible sets U , as denoted in this paper by comp(U ), is decided during runtime among compatible nodes on a first-come-first-serve basis.

We benchmarked nestHDB and 16 other publicly available #Sat solvers on 1,494 instances recently considered [24] . Among those solvers are single-core solvers miniC2D [41] , d4 [34] , c2d [13] , ganak [46] , sharpSAT [48] , sdd [14] , sts [21] , dsharp [39] , cnf2eadt [32] , cachet [45] , sharpCDCL [30] , approxmc3 [8] , and bdd minisat [49] . We also included multi-core solvers dpdb [24] , gpusat2 [25] , as well as countAntom [7] . While nestHDB itself is a multi-core solver, we additionally included in our comparison nestHDB(sc), which is nestHDB, but restricted to a single core only. The instances [24] we took are already preprocessed by pmc [33] using recommended options -vivification -eliminateLit -litImplied -iterate=10 -equiv -orGate -affine for preserving model counts. However, nestHDB still uses pmc with these options also in Line 1 of Listing 2.

Further, we considered the problem #∃Sat, where we compare solvers pro-jMC [35] , clingo [27] , ganak [46] , nestHDB (see footnote 1), and nestHDB(sc) on 610 publicly available instances 2 from projMC (consisting of 15 planning, 60 circuit, and 100 random instances) and Fremont, with 170 symbolic-markov applications, and 265 misc instances. For preprocessing in Line 1 of Listing 2, nestHDB uses pmc as before, but without options -equiv -orGate -affine to ensure preservation of models (equivalence).

Benchmark Setup. Solvers ran on a cluster of 12 nodes. Each node of the cluster is equipped with two Intel Xeon E5-2650 CPUs consisting of 12 physical cores each at 2.2 GHz clock speed, 256 GB RAM. For dpdb and nestHDB, we used Postgres 12 on a tmpfs-ramdisk (/tmp) that could grow up to at most 1 GB per run. Results were gathered on Ubuntu 16.04.1 LTS machines with disabled hyperthreading on kernel 4.4.0-139. We mainly compare total wall clock time and number of timeouts. For parallel solvers (dpdb, countAntom, nestHDB) we allow 12 physical cores. Timeout is 900 s and RAM is limited to 16 GB per instance and solver. Results for gpusat2 are taken from [24] .

Benchmark Results. The results for #Sat showing the best 14 solvers are summarized in the cactus plot of Fig. 4 . Overall it shows nestHDB among the best solvers, solving 1,273 instances. The reason for this is, compared to dpdb, that nestHDB can solve instances using TDs of primal graphs of widths larger than 44, up to width 266. This limit is even slightly larger than the width of 264 that sharpSAT on its own can handle. We also tried using minic2d instead of sharpSAT as standard solver for solvers nestHDB and nestHDB(sc), but we could only solve one instance more. Notably, nestHDB(sc) has about the same performance as nestHDB, indicating that parallelism does not help much on the instances. Further, we observed that the employed simple cache as used in Listing 2, provides only a marginal improvement. Figure 5 (left) depicts a table of results on #∃Sat, where we observe that nestHDB does a good job on instances with low widths below threshold abstr = 8 (containing ideas of dpdb), but also on widths well above 8 (using nested DP). Notably, nestHDB is also competitive on widths well above 50. Indeed, nestHDB and nestHDB(sc) perform well on all benchmark sets, whereas on some sets the solvers projMC, clingo and ganak are faster. Overall, parallelism provides a significant improvement here, but still nestHDB(sc) shows competitive performance, which is also visualized in the cactus plot of Fig. 5 (right). Figure 6 shows scatter plots comparing nestHDB to projMC (left) and to ganak (right). Overall, both plots show that nestHDB solves more instances, since in both cases the y-axis shows more black dots at 900 s than the x-axis. Further, the bottom left of both plots shows that there are plenty easy instances that can be solved by projMC and ganak in well below 50 s, where nestHDB needs up to 200 s. Similarly, the cactus plot given in Fig. 5 (right) shows that nestHDB can have some overhead compared to the three standard solvers, which is not surprising. This indicates that there is still room for improvement if, e.g., easy instances are easily detected, and if standard solvers are used for those instances. Alternatively, one could also just run a standard solver for at most 50 s and if not solved within 50 s, the heavier machinery of nested dynamic programming is invoked. Apart from these instances, Fig. 6 shows that nestHDB solves harder instances faster, where standard solvers struggle.

We presented nested dynamic programming (nested DP) using different levels of abstractions, which are subsequently refined and solved recursively. This approach is complemented with hybrid solving, where (search-intense) subproblems are solved by standard solvers. We provided nested DP algorithms for problems related to Boolean satisfiability, but the idea can be easily applied for other formalisms. We implemented some of these algorithms and our benchmark results are promising. For future work, we plan deeper studies of problemspecific abstractions, in particular for QSat. We want to further tune our solver parameters (e.g., thresholds, timeouts, sizes), deepen interleaving with solvers like projMC, and to use incremental solving for obtaining abstractions and evaluating nested bag formulas, where intermediate solver references are kept during dynamic programming and formulas are iteratively added and (re-)solved.

htd -a free, open-source framework for (customized) tree decompositions and beyond

Clause-learning algorithms with many restarts and bounded-width resolution

Practical access to dynamic programming on tree decompositions

PicoSAT essentials. JSAT

D-FLAT 2 : subset minimization in dynamic programming on tree decompositions made easy

Combinatorial optimization on graphs of bounded treewidth

Laissez-faire caching for parallel #SAT solving

Distributionaware sampling and weighted model counting for SAT

Expansion-based QBF solving on tree decompositions

Quantified constraint satisfaction and bounded treewidth

A relational model of data for large shared data banks

Parameterized Algorithms

New advances in compiling CNF to decomposable negation normal form

SDD: a new canonical representation of propositional knowledge bases

The PACE 2017 parameterized algorithms and computational experiments challenge: the second iteration

Counting answers to existential questions

Graph Theory, Graduate Texts in Mathematics

Fundamentals of Parameterized Complexity. TCS

Subtractive reductions and complete problems for counting complexity classes

Measuring what matters: a hybrid approach to dynamic programming with treewidth

Uniform solution sampling using a constraint solver as an oracle

Answer set solving with bounded treewidth revisited

Exploiting Treewidth for Projected Model Counting and Its Limits

Exploiting database management systems and treewidth for counting

An improved GPU-based SAT model counter

Combining treewidth and backdoors for CSP

Multi-shot ASP solving with clingo

Reasoning with quantified Boolean formulas

Structural decompositions of epistemic logic programs

SAT-based analysis and quantification of information flow in programs

Treewidth: Computations and Approximations

Knowledge compilation for model counting: affine decision trees

Preprocessing for propositional model counting

An improved decision-DDNF compiler

A recursive algorithm for projected model counting

Evaluation of an MSO-solver

Evaluating QBF solvers: quantifier alternations matter

An experimental study of the treewidth of realworld graph data (extended version)

Dsharp: fast d-DNNF compilation with sharpSAT

Invitation to Fixed-Parameter Algorithms

A top-down compiler for sentential decision diagrams

The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)

Graph minors II: algorithmic aspects of tree-width

Algorithms for propositional model counting

Combining component caching and clause learning for effective model counting

GANAK: a scalable probabilistic exact model counter

Positive-instance driven dynamic programming for treewidth

sharpSAT -counting models with advanced component caching and implicit BCP

Implementing efficient all solutions SAT solvers

The work has been supported by the Austrian Science Fund (FWF), Grants Y698, and P32830, as well as the Vienna Science and Technology Fund, Grant WWTF ICT19-065.