key: cord-0046695-qqwxt1se authors: Slivovsky, Friedrich; Szeider, Stefan title: A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth date: 2020-06-26 journal: Theory and Applications of Satisfiability Testing - SAT 2020 DOI: 10.1007/978-3-030-51825-7_19 sha: 6977d9ab9f285d22416373f41ada65b9dbe6bb3f doc_id: 46695 cord_uid: qqwxt1se The propositional model counting problem (#SAT) is known to be fixed-parameter-tractable (FPT) when parameterized by the width k of a given tree decomposition of the incidence graph. The running time of the fastest known FPT algorithm contains the exponential factor of [Formula: see text]. We improve this factor to [Formula: see text] by utilizing fast algorithms for computing the zeta transform and covering product of functions representing partial model counts, thereby achieving the same running time as FPT algorithms that are parameterized by the less general treewidth of the primal graph. Our new algorithm is asymptotically optimal unless the Strong Exponential Time Hypothesis (SETH) fails. Propositional model counting (#SAT) is the problem of determining the number of satisfying truth assignments of a given propositional formula. The problem arises in several areas of AI, in particular in the context of probabilistic reasoning [2, 15] . #SAT is #P-complete [18] , even for 2-CNF Horn formulas, and it is NP-hard to approximate the number of models of a formula with n variables within 2 n 1−ε , for any ε > 0 [15] . Since syntactic restrictions do not make the problem tractable, research generally focused on structural restrictions in terms of certain graphs associated with the input formula, which is often assumed to be in CNF. Popular graphical models are the primal graph (vertices are the variables, two variables are adjacent if they appear together in a clause), the dual graph (vertices are the clauses, two clauses are adjacent if they share a variable), and the incidence graph (vertices are variables and clauses, a variable and a clause are adjacent if the variable occurs in the clause). The structural complexity of a graph can be restricted in terms of the fundamental graph invariant treewidth [14] By taking the treewidth of the primal, dual, or incidence graph one obtains the primal treewidth, the dual treewidth, and the incidence treewidth of the formula, respectively. If we consider CNF formulas for which any of the three parameters is bounded by a constant, the number of models can be computed in polynomial time. Indeed, the order of the polynomial is independent of the treewidth bound, and so #SAT is fixed-parameter tractable (FPT) when parameterized by primal, dual or incidence treewidth. Incidence treewidth is considered the most general parameter among the three, as any formula of primal or dual treewidth k has incidence treewidth at most k + 1. However, one can easily construct formulas of constant incidence treewidth and arbitrarily large primal and dual treewidth. Known model counting algorithms based on incidence treewidth have to pay for this generality with a significant larger running time: Whereas the number of models for formulas of primal or dual treewidth k can be counted in time 1 O * (2 k ), the best know algorithm for formulas of incidence treewidth k takes time O * (4 k ). 2 This discrepancy cannot be accounted for by a loose worst-case analysis, but is caused by the actual size of the dynamic programming tables constructed by the algorithms. In this paper, we show that algebraic techniques can be used to bring down the running time to O * (2 k ). Specifically, we prove that the most time-consuming steps can be expressed as zeta transforms and covering products of functions obtained from partial model counts. Since there are fast algorithms for computing these operations [3] , we obtain the desired speedup. Treewidth. Let G = (V (G), E(G)) be a graph, T = (V (T ), E(T )) be a tree, and χ be a labeling of the vertices of T by sets of vertices of G. We refer to the vertices of T as "nodes" to avoid confusion with the vertices of G. The tuple (T, χ) is a tree decomposition of G if the following three conditions hold: 1. For every v ∈ V (G) there exists a node t ∈ V (T ) such that v ∈ χ(t). 2. For every vw ∈ E(G) there exists a node t ∈ V (T ) such that v, w ∈ χ(t). 3. For any three nodes t 1 , t 2 , t 3 ∈ V (T ), if t 2 lies on the path from t 1 to t 3 , then The width of a tree decomposition (T, χ) is defined by max t∈V (T ) |χ(t)| − 1. The treewidth tw (G) of a graph G is the minimum width over all its tree decompositions. For constant k, there exists a linear-time algorithm that checks whether a given graph has treewidth at most k and, if so, outputs a tree decomposition of minimum width [5] . However, the huge constant factor in the runtime of this algorithm makes it practically infeasible. For our purposes, it suffices to obtain tree decompositions of small but not necessarily minimal width. There exist several powerful tree decomposition heuristics that construct tree decompositions of small width for many cases that are relevant in practice [4, 12] , and the single-exponential FPT algorithm by Bodlander et al. [6] produces a factor-5 approximation of treewidth. In this paper we also consider a particular type of tree decompositions. The triple (T, χ, r) is a nice tree decomposition of G if (T, χ) is a tree decomposition, the tree T is rooted at node r, and the following three conditions hold [11] : 1. Every node of T has at most two children. 2. If a node t of T has two children t 1 and t 2 , then χ(t) = χ(t 1 ) = χ(t 2 ); in that case we call t a join node. 3. If a node t of T has exactly one child t , then one of the following holds: (a) |χ(t)| = |χ(t )| + 1 and χ(t ) ⊂ χ(t); in that case we call t an introduce node. It is known that one can transform efficiently any tree decomposition of width k of a graph with n vertices into a nice tree decomposition of width at most k and at most 4n nodes [11, Lemma 13 Propositional Formulas. We consider propositional formulas F in conjunctive normal form (CNF) represented as set of clauses. Each clause in F is a finite set of literals, and a literal is a negated or unnegated propositional variable. For a clause C we denote by var (C) the set of variables that occur (negated or unnegated) in C; for a formula F we put var (F ) = C∈F var (C). The size of a clause is its cardinality. A truth assignment is a mapping τ : X → {0, 1} defined on some set X of variables. We extend τ to literals by setting τ (¬x) = 1 − τ (x) for x ∈ X. A truth assignment τ : X → {0, 1} satisfies a clause C if for some variable x ∈ var (C) ∩ X we have x ∈ C and τ (x) = 1, or ¬x ∈ C and τ (x) = 0. An assignment satisfies a set F of clauses if it satisfies every clause in F . For a formula F , we call a truth assignment τ : var (F ) → {0, 1} a model of F if τ satisfies F . We denote the number of models of F by #(F ). The propositional model counting problem #SAT is the problem of computing #(F ) for a given propositional formula F in CNF. Incidence Treewidth. The incidence graph G * (F ) of a CNF formula F is the bipartite graph with vertex set F ∪var (F ); a variable x and a clause C are joined by an edge if and only if x ∈ var (C). The incidence treewidth tw * (F ) of a CNF formula F is the treewidth of its incidence graph, that is tw * (F ) = tw (G * (F )). and the Möbius transform μf of f is given by Theorem 1 (Kennes [10] ). Let V be an k-element set and let f : 2 V → Z be a function. All values of ζf and μf can be computed using O(2 k k) arithmetic operations. The covering product can be computed using zeta and Möbius transforms by applying the following two results (see Aigner [1] ). Given functions f, g : 2 V → Z, the zeta transform of the covering product of f and g is the pointwise product of the zeta-transformed arguments. f : 2 V → Z. Then for every X ⊆ V f (X) = (μζf )(X) = (ζμf)(X). Samer and Szeider presented an algorithm for #SAT with a running time of O * (4 k ) [16] , where k is the width of a given tree decomposition of the incidence graph. In this section, we are going to show how to improve this to O * (2 k ). Their algorithm proceeds by bottom-up dynamic programming on a nice tree decomposition, maintaining tables that contain partial solution counts for each node. For the remainder of this section, let F be an arbitrary but fixed CNF formula, and let (T, χ, r) be a nice tree-decomposition of the incidence graph G * (F ) that has width k. For each node t of T , let T t denote the subtree of T rooted at t, and let V t = t ∈V (Tt) χ(t ) denote the set of vertices appearing in bags of T t . Further, let F t denote the set of clauses in V t , and let X t denote the set of all variables in V t . We also use the shorthands χ c (t) = χ(t) ∩ F and χ v (t) = χ(t) ∩ var (F ) for the set of clauses and the set of variables in χ(t), respectively. Let t be a node of T . For each assignment α : N (t, α, A) as the set of assignments τ : X t → {0, 1} for which the following two conditions hold: x ∈ χ v (t), and membership of C in A for clauses C ∈ χ c (t). The last entry of each row contains the integer n(t, α, A). Samer and Szeider showed that the entries of the table M t can be efficiently computed for each node t. More specifically, they showed how M t can be obtained for leaf nodes t, and how M t can be computed from the tables for the child nodes of introduce, forget, and join nodes t. Since the running time for join and variable introduce nodes are the bottleneck of the algorithm, we summarize the results concerning correctness and running time for the remaining node types as follows. [16] ). If t ∈ T is a leaf node, or a forget or clause introduce node with child t such that M t has already been computed, the table M t can be obtained in time 2 k |ϕ| O (1) . The table entries for a join node can be computed as a sum of products from tables of its child nodes. [16] ). Let t ∈ T be a join node with children t 1 , t 2 . For each assignment α : A straight-forward algorithm for computing this sum requires an arithmetic operation for each pair ( , and thus 2 k 2 k = 4 k operations in the worst case. By using a fast algorithm for the covering product, we can significantly reduce the number of arithmetic operations and thus the running time. The key observation is that the sum of products in (4) can be readily expressed as a covering product (3). For variable introduce nodes the table entry for each assignment and subset of clauses can be computed as a sum over table entries of the child table. [16] ). Let t be an introduce node with child t such that χ(t) = χ(t ) ∪ {x} for a variable x. Then, for each truth assignment α : A simple approach is to go through all 2 k assignments α and subsets A and, if necessary, compute the sums in (5) and (6). Since there could be up to 2 k subsets to sum over, this again requires 4 k arithmetic operations in the worst case. The following lemma observes that we can instead use the zeta transform (1). Let t be an introduce node with child t such that Proof. We can rewrite the sums in (5) and (6) as By Theorem 1, the zeta and Möbius transform of a function f : 2 V → Z can be computed using O(2 k k) arithmetic operations, where k = |V | is the size of the underlying set. In conjunction with Lemma 1 and Lemma 2, this lets us compute the covering product of two functions f, g : How this translates into running time depends on the choice of computational model. Since the model count of a formula can be exponential in the number of variables, it is unrealistic to assume that arithmetic operations can be performed in constant time. Instead, we adopt a random access machine model where two nbit integers can be added, subtracted, and compared in time O(n), and multiplied in time O(n log n) [8] . For the purposes of proving a bound of O * (2 k ), it is sufficient to show that the bit size of integers obtained as intermediate results while computing the zeta and Möbius transforms is polynomially bounded by the number of variables in the input formula. To verify that this is the case, we present the dynamic programming algorithms used to efficiently compute these transforms [3] , following the presentation by Fomin and Kratsch [7] . Theorem 3. Let V be a k-element set and let f : 2 V → Z be a function that can be evaluated in time O(1) and whose range is contained in the interval (−2 N , 2 N ) . All values of ζf and μf can be computed in time 2 k (k + N ) O (1) . {j + 1, . . . , k}) ), for j = 0, . . . , k. Note that ζ k (X) = (ζf)(X). The values ζ j can be computed as For the Möbius transform, we compute intermediate values . . . , k}) ). Again we have μ k (X) = (μf )(X), and the values μ j can be computed as In both cases, this requires k arithmetic operations for each set X ⊆ V , and the intermediate values are contained in the interval (−2 k 2 N , 2 k 2 N ). Let V be an k-element set and let f, g : 2 V → Z be functions that can be evaluated in time O(1) and whose range is contained in the interval (−2 N , 2 N ) . All values of f * c g can be computed in time 2 k (k + N ) O (1) . Having obtained these bounds on the time required to compute the zeta transform and the covering product, we can now state improved time bounds for obtaining the entries of the tables M t of join and variable introduce nodes t. Proof. As before, let p = |χ v (t )| and q = |χ c (t )|. For each truth assignment α : χ v (t ) → {0, 1}, we proceed as follows. We compute the value of the zeta transform (ζf)(A) for all subsets A ⊆ χ c (t ). Again, each entry of M t represents a partial model count that is bounded by 2 n , so we can do this in time 2 q (q + n) O(1) by Theorem 1. Since q ≤ n this is in O * (2 q ). Then, we iterate over all A ⊆ χ c (t ) and set the entries M t (α, A) based on (7) and (8) Proof. Let (T, χ, r) be a nice tree decomposition of the incidence graph of F . We compute the tables M t for all nodes t of T , starting from the leaf nodes of T . By Lemmas 2, 7, and 8, each table can be computed in time O * (2 k ). We can compute #(F ) = α:χv(r)→{0,1} n(r, α, ∅) at the root r. The space requirements of the algorithm remain unchanged by the proposed improvements. Each table M t has at most 2 k+1 entries, and each entry requires up to n bits. By keeping as few tables in memory as possible and discarding tables whenever they are no longer needed, no more than 1 + log 2 (N + 1) tables need to be stored in memory at any point, where N is the number of nodes in the tree decomposition [16, Proposition 3] . Let s r := inf{ δ | there exists an O * (2 δn ) algorithm that decides the satisfiability of n-variable r-CNF formulas with parameter n } and let s ∞ := lim r→∞ s r . Impagliazzo et al. [9] introduced the Strong Exponential Time Hypothesis (SETH), which states that s ∞ = 1. SETH has served as a very useful hypothesis for establishing tight bounds on the running time for NP-hard problems [13] . For instance, an immediate consequence of the SETH is that the satisfiability of an n-variable CNF formula cannot be solved in time O * ((2 − ε)) n ) for any ε > 0. However, for the incidence graph of an n-variable CNF formula F = {C 1 , . . . , C m } we can always give a tree decomposition (T, χ) of width n (recall that the width of a tree decomposition is the size of its largest bag minus one) by taking as T a star with center t and leaves t 1 , . . . , t m , and by putting χ(t) = var (F ) and χ(t i ) = var (F ) ∪ {C i }, for 1 ≤ i ≤ n. Thus, if the bound in Theorem 4 could be improved from O * (2 k ) to O * ((2 − ε) k ), we would have an O * ((2 − ε) n ) SAT-algorithm, and hence a contradiction to the SETH. We can, therefore, conclude that Theorem 4 is tight under the SETH. Combinatorial Theory Algorithms and complexity results for #SAT and Bayesian inference Fourier meets Möbius: fast subset convolution Annual ACM Symposium on Theory of Computing Discovering treewidth A linear-time algorithm for finding tree-decompositions of small treewidth A c k n 5-approximation algorithm for treewidth Exact Exponential Algorithms Integer multiplication in time Which problems have strongly exponential complexity? Computational aspects of the mobius transformation of graphs Treewidth: Computations and Approximations Treewidth: Computational experiments Lower bounds based on the exponential time hypothesis Graph minors. II. Algorithmic aspects of tree-width On the hardness of approximate reasoning Algorithms for propositional model counting Constraint satisfaction with bounded treewidth revisited The complexity of computing the permanent Exact algorithms for NP-hard problems: a survey We thank Andreas Björklund for the suggestion of using covering products to improve the running time of SAT algorithms for instances of bounded incidence treewidth.