Compilation and Fast Model Counting beyond CNF

1 Introduction

Knowledge compilation is a domain of computer sciences that studies the different ways to represent functions. Classes of representations, or languages, have been invented where specific problems become tractable. In particular, many Boolean languages have been created that support polynomial-time model counting, that is, determining the number of truth assignments on which a function f : {0, 1}n → {0, 1} evaluates to 1. In practice, several model counters for CNF formulas are transforming, or compiling, their inputs into the language d-DNNF of circuits in deterministic decomposable negation normal form, where model counting is feasible in linear time (in the size of the circuits). For instance, C2D [Darwiche, 2004], DSharp [Muise et al., 2012], miniC2D [Oztok and Darwiche, 2015], and D4 [Lagniez and Marquis, 2017] all compile CNF formulas into (sublanguages) of d-DNNF. Other model counters do not explicitly compile the CNF but can be seen as compilers in disguise [Kiesel and Eiter, 2023].

Compilation to d-DNNF is often hard in the sense that the d-DNNF circuit representations of many functions provably have exponential size, even for functions that belong to fragments where model counting is tractable such as systems of Boolean linear equations [de Colnet and Mengel, 2023]. On a more positive note, compiling from CNF to d-DNNF is fixedparameter tractable (FPT) when the parameter is the treewidth of the CNF's primal graph [Huang and Darwiche, 2007] and when it is the treewidth of its incidence graph [Bova et al., 2015]. To further understand when the input is easy to compile, one possibility is to find new CNF parameters that dominate treewidth and yet enable FPT compilation to d-DNNF, for instance, decision-width [Oztok and Darwiche, 2014b], CV-width [Oztok and Darwiche, 2014a] and PS-width [Bova et al., 2015]. Another direction is to part from the CNF input and study the parameterized compilability of functions given in a different format such as DNF or a general Boolean circuit [Amarilli et al., 2020]. In this paper, we follow the latter direction: we investigate the FPT compilation of systems (i.e., conjunctions) of Boolean constraints that are not just CNF. We see each CNF formula as a system of disjunctive clauses and identify other types of constraints that can be added to the system while ensuring an FPT compilation to d-DNNF parameterized by its incidence treewidth k. While compiling general systems of constraints to d-DNNF cannot be FPT parameterized k unless FPT = W[1] (since even satisfiability is W[1]-hard in this setting [Samer and Szeider, 2010]), we show that there is an FPT compilation algorithm for specific constraints. In a first approximation, these are the constraints that can only be in a constant number of states when assigning any subset of the variables in any way. Parity constraints (i.e., constraints of the form "the sum of the variables is odd/even") are a good example where there are only two possible states: given a parity constraint and a subset of its variables, assigning these variables in any way either results in the odd parity constraint or the even parity constraint on the remaining variables. Our main result is the following.

Theorem 1. Let w be a constant integer and C be a class of constraints such that, for every c ∈ C, and every subset Y of c's variables, at most w different constraints can be obtained from c by assigning variables in Y in any way. There is an algorithm that, given a system F of constraints from C, returns in time 2O(k)poly(|F | + |var(F )|)) a d-DNNF circuit for F , where k is the treewidth of the incidence graph of F.

The neatest proof we could find for this result on the compilation of non-CNF systems-which we present in this papergoes through constructing CNF encodings of the systems and then compiling these encodings to d-DNNF.

Theorem 1 includes a rather lengthy characterization of our constraints. For the proof, we use a "more advanced" characterization in knowledge compilation terms. The class C will be a class of constraints that are w-slim for the language OBDD or the language SDNNF. This notion is inspired by Wegener's book [2000, Section 5.3] and introduced in detail in Section 3. We are not the first to consider OBDD constraints to prove FPT results, for instance Chen and Grohe [2010] use similar constraints to prove FPT results for the constraint satisfaction problem. We prove our theorem in Section 4 with a more accurate running time where the exponential part also depends on w. Finally, in Section 5, we show that we can count models faster than by compilation if we put additional restrictions on the constraints. One of our results is based on bounded state-size (introduced in Section 3), which captures important constraints like XORs, modulo, and cardinality constraints.

Theorem 2. Let F be a system of constraints whose maximum state-size is w. There is an algorithm that, given F and a nice width-k tree decomposition of the incidence graph of F , counts the models of F in time O(w2k (|F |+|var(F )|)) in the unit-cost model.

2 Preliminaries

A Boolean variable x takes a value in {0, 1}. Literals are denoted by x and ¯x. An assignment to a set X of Boolean variables is a mapping from X to {0, 1}, and a Boolean function f over X maps the assignments to X to {0, 1}. For us, constraints are just Boolean functions that appear in systems (conjunctions of constraints). CNF formulas are systems of constraints whose constraints are clauses (disjunctions of literals). We write |F| for the number of constraints in the system F. Boolean circuits are another way to represent functions. The size of a circuit D, denoted |D|, is its number of gates and connectors. We denote by gates(D) the set of gates of D. For g ∈ gates(D), Dg is the subcircuit of D whose output gate is g. We write f(X), D(X), and F(X) to indicate that the variable set of a function, circuit, or system is X, respectively. If this set is not explicit, we use var(f), var(D), var(F).

2.1 Treewidth and Tree Decompositions

A tree decomposition T of a graph G is a pair (T, b) with T a tree and b : V (T) → P(V (G)) a bag function such that (1) ⋃t∈V (T) b(t) = V (G), (2) for all uv ∈ E(G), there is t ∈ T such that {u, v} ⊆ b(t), and (3) for all v ∈ V (G), T [t | v ∈ b(t)] is connected. The width of T is maxt∈T |b(t)|. The treewidth of G is tw(G) := minT maxt∈T |b(t)| - 1 where T ranges over all tree decompositions of G. A tree decomposition is nice when it is rooted and when each node t ∈ V (T) is of one of the following three types: a join node, an introduce node, or a forget node. t is a join node if it has two children t1 and t2 and b(t) = b(t1) = b(t2). t is an introduce node for v ∈ V (G) if it has a single child t′

and v ̸∈ b(t′ ) and b(t) = b(t′ ) ∪ {v}. t is a forget node for v ∈ V (G) if it has a single child t′ and v ̸∈ b(t) and b(t′ ) = b(t) ∪ {v}. In addition, the bag of the root node is empty. Every tree decomposition can be made nice without increasing its width.

The incidence graph of a system F of constraints, denoted by GF , is the graph whose vertices are the constraints and the variables of F and such that there is an edge between a constraint c and a variable x if and only if x ∈ var(c). The incidence treewidth of F is twi(F) := tw(GF ).

2.2 OBDDs and SDNNF Circuits

(d-)SDNNF Circuits. A variable tree (vtree) τ over a set X of variables is a rooted binary tree whose leaves are in bijection with X. For every t ∈ V (τ), var(t) is the set of variables on the leaves below t. A circuit D in structureddecomposable negation normal form (SDNNF) [Pipatsrisawat and Darwiche, 2008] is a Boolean circuit with literal inputs, whose gates are binary ∨-gates and binary ∧-gates, and such that there exist a vtree τ over var(D) and a mapping λ : gates(D) → V (τ) verifying the following:

• For every g ∈ gates(D), var(Dg) ⊆ var(λ(g)).
• For every ∨-gate g = g1 ∨ g2, λ(g) = λ(g1) = λ(g2).
• For every ∧-gate g = g1 ∧ g2, λ(g) has two children t1 and t2 and λ(g1) is below t1 and λ(g2) is below t2.

We say that D is structured by (τ, λ) and sometimes omit λ. An example of an SDNNF circuit is shown in Figure 2b with the mapping λ given by the color code. An SDNNF circuit D is deterministic (d-SDNNF) when for all ∨-gates g = g1 ∨g2, we have D-1 g1 (1)∩D-1 g2 = ∅. Counting the models of D, i.e., finding |D-1 (1)|, is tractable when D is a d-SDNNF circuit.

OBDDs. A binary decision diagram (BDD) is a directed acyclic graph with a single source, two sinks labeled 0 and 1, whose internal nodes are decision nodes with two distinct children and labeled by variables. A node v labeled by variable x and with children v0 and v1 is recursively interpreted as a Boolean function v = (¯x ∧ v0) ∨ (x ∧ v1). Every assignment α corresponds to a path in the DAG. Starting from the root, assuming α's path reaches v follows v0 if α(x) = 0 and v1 otherwise. The assignments satisfying the BDD are exactly those whose paths reach the sink 1. For a total order π on the variables, a π-Ordered BDD (π-OBDD) is a BDD whose variables appear at most once along every path from the root to a sink and always in an order consistent with π. A π-OBDD is complete if every path contains all the variables. d-SDNNF circuits generalize OBDDs in the sense that there is a simple linear-time rewriting that transforms OBDDs into d-SDNNF circuits structured by linear vtrees (i.e., vtrees whose internal nodes all have a leaf child).

Width measures. The width of an OBDD is the maximum number of nodes labeled by the same variable. Note that making an OBDD complete, while feasible in linear time, can also increase the width by a linear factor [Bollig and Wegener, 2000]. The width of an SDNNF circuit structured by (T, λ) is defined as maxt∈V (T) |λ-1 (t)|. This definition differs from that of Capelli and Mengel [2019] but is more convenient for stating our results.

3 SlimFunctions and STS

In this paper, constraints are global constraints [van Hoeve and Katriel, 2006]. So we know the type (e.g., clauses, parity constraints, cardinality constraints) of every constraint we manipulate.

CNF formulas are known to be FPT compilable to dSDNNF parameterized by their incidence treewidth.

Theorem 3 (Bova et al., 2015). There is an algorithm that transforms any CNF formula F into an equivalent d-SDNNF circuit in time 2O(twi(F))poly(|F| + |var(F)|).

The result leans on the fact that for every clause c, every subset Y ⊆ var(c), and every assignment α to Y , the clause c|α where variables are assigned as in α can be in only two states: either it is satisfied, or it is the projection of c onto the complement of Y . Note that α falsifying c falls into the second case (Y = var(c) and c|α is the empty clause). Our intuition is that FPT compilation to d-SDNNF should be possible for systems of constraints with a similar property: when subject to any assignment to any fixed set Y , every constraint of the system can only be in a few states. For example, consider an XOR constraint c : x1 ⊕ x2 ⊕ x3 ⊕ x4 ⊕ x5 = 0 and Y = {x1, x2, x3}. Then c|α is either the odd parity constraint x4 ⊕ x5 = 1, or the even parity constraint x4 ⊕ x5 = 0.

3.1 SlimFunctions for Complete OBDDs and SDNNFs

One can consider a complete OBDD is as state diagram where the values of the variables are read in a predefined order. The width of the complete OBDD is then the maximum number of states reachable after having set any number of variables in that order. The property we want for our constraints translates into the requirement that the smallest possible width in one of their π-OBDD representations is bounded for all the variable orders π. In the following, h : N→R is a real function.

Definition 4. A class F of Boolean functions is h-slim for complete OBDDs when, for every n-variables function f ∈ F and every total order π of var(f), there is a complete πOBDD of width at most h(n) computing f .

The notions of O(1)-slim functions, O(n)-slim functions, etc. should be self-explanatory. Given a fixed constant w, we talk of w-slim functions when h is the constant w function. When h is an unknown polynomial, the h-slim functions for complete OBDDs coincide with the nice functions from Wegener's book [2000, Section 5.3]. Our proofs below rely on SDNNF representations rather than OBDD representations. The concept of h-slim functions generalizes to SDNNF.

Definition 5. A class F of Boolean functions is h-slim for complete SDNNFs when, for every n-variables function f ∈ F and vtree T over var(f), there is a complete SDNNF of width at most h(n) and with vtree T that computes f .

Given the rewriting of complete OBDDs into complete dSDNNFs, it is immediate that having a small OBDD-width for every variable ordering implies having a small SDNNFwidth for every linear vtree. However, generalizing to all possible vtrees is not straightforward.

Lemma 6. Let F be a class of functions.

• If F is h-slim for complete OBDDs, then it is O(h3 )-slim for complete SDNNFs.
• If F is h-slim for complete SDNNFs, then it is 22O(h) -slim for complete OBDDs.

The doubly exponential upper bound could be a bit loose but cannot be decreased below exponential due to the following.

Lemma 7. There are functions computed by complete SDNNFs of width O(n) for every vtree, but that are only computed by OBDDs and d-SDNNFs of width 2Ω(n) /n.

Let us now restate our main result, i.e., Theorem 1, using constraints that belong to families of functions O(1)-slim for complete SDNNFs. Recall that our constraints are global. We will need the following assumption.

Assumption 8. For every type of constraint appearing in our system, we have a polynomial-time algorithm to compile every constraint of this type into a minimal-width complete SDNNF for any given vtree.

Theorem 9. Let w ∈ N be a fixed constant. Under assumption 8, there is an algorithm that, given a system F of constraints that are all w-slim for complete SDNNFs, constructs in time 2O(w·twi(F)) poly(|F| + |var(F)| + w) a circuit in d-SDNNF that computes F .

In Table 1, we give several families of constraints along with upper bounds on the smallest h functions for which they are h-slim for complete OBDDs and SDNNFs. The proof of the correctness of these values for h appear in the long version of the paper. Assumption 8 is reasonable for most constraint types of the table 1, in particular for clauses, XORs, sums modulo, cardinality and threshold constraints.

3.2 Commutative State Transitions Systems

Definition 10. A state transition system (STS) consists of a set of states S, two transition functions f0, f1 : S → S, a starting state s0 ∈ S and a set of accepting states T ⊆ S. The extended transition function δ : {0, 1}∗ → S is defined as:

The STS is finite if S is finite, and commutative if f0(f1(s)) = f1(f0(s)) for all s ∈ S. We write CSTS for commutative STS.

Note that the extended transition function δ for a CSTS has the following property: for any l1, l′1 , l2, l′2 ∈ {0, 1}∗ , if δ(l1) = δ(l′1 ) and δ(l2) = δ(l′2 ), then δ(l1l2) = δ(l′1 l′2 ). This is because δ(l1l2) = δ(l′1 l2) = δ(l2l′1 ) = δ(l′2 l′1 ) = δ(l′1 l′2 ). If we assume that for every s ∈ S there is l ∈ {0, 1}∗ such that δ(l) = s, that is, the CSTS is in a sense connected, we can then define a binary operation + : S ×S → S as follows: for any s1, s2, s ∈ S, s1 + s2 = s if there is l1, l2 ∈ {0, 1}∗ such that δ(l1) = s1, δ(l2) = s2, and δ(l1l2) = s. Note that for all s, s′ , s′′ ∈ S, we have s + s0 = s, s + s′ = s′ + s and (s + s′ ) + s′′ = s + (s′ + s′′ ). That is, (S,+, s0) forms a commutative monoid.

Given a function f : {0, 1}n → {0, 1}, we say an STS describes f if, for every l ∈ {0, 1}n , δ(l) ∈ T if and only if f(l) = 1. Let f, g : {0, 1}n → {0, 1} be two functions. We say that a CSTS describes f modulo literal-flipping if it describes g and there exists a literal-flipping function ϕ that sends xi to either xi or ¯xi such that f = g ◦ ϕ. We call the minimum number of states of a CSTS that describes f modulo literal-flipping the state size of f.

Lemma 11. Let f be a symmetric (resp. literal-symmetric) function. If f admits a complete OBDD representation of width w, then f is described (resp. described modulo literalflipping) by a CSTS with at most (w + 1)2 /4 states.

4 FPT Compilation of Systems of O(1)-Slim Constraints

In this section, we explain the proof of Theorem 9. The proof is in three steps: (1) find a CNF encoding H(X,Z) of F(X) whose incidence treewidth is at most O(w · twi(F)), (2) compile H(X,Z) to d-SDNNF using Theorem 3, and (3) existentially forget the auxiliary variables Z from the resulting d-SDNNF circuit. We do not have to take care of (2). For (3), forgetting the variables Z from a d-SDNNF circuit D(X, Z) means finding another d-SDNNF circuit computing ∃Z.D(X,Z). Forgetting many variables from a dSDNNF circuit is generally intractable [Pipatsrisawat and Darwiche, 2008]. However the operation is tractable when the Z-variables are completely defined in terms of the Xvariables. We make sure to be in this situation by using only Tseitin CNF encodings to generate H(X, Z).

4.1 The Tseitin CNF Encoding

Let D(X) be a Boolean circuit whose internal gates are binary ∨-gates and binary ∧-gates. Let gates∗ (D) be the set of its internal gates. Every gate g is associated with a variable zg. Let Z = {zg | g ∈ gates ∗ (D)}. The Tseitin encoding of D is the CNF

where, for every gate g, if g = g1 ∧ g2 then Tseitin(g) := (¯ zg ∨ zg1 ) ∧ (¯ zg ∨ zg2 ) ∧ (¯ zg1 ∨ ¯ zg2 ∨zg), if g = g1 ∨g2 then Tseitin(g) := (¯ zg ∨ zg1 ∨ zg2 ) ∧ (¯ zg1 ∨ zg) ∧ (¯ zg2 ∨ g), and if g is an input gate, so if g = x, ¯x, 0 or 1, then zg = g. The formula HTseitin D is a CNF encoding of D in the sense that

We often drop the Tseitin superscript in the rest of the paper. Lemma 12. Let f(X) be a Boolean function and D1(X1), . . . ,Dm(Xm) be Boolean circuits. There is a linear-time algorithm that, given a d-SDNNF circuit D computing f(X) ∧ HTseitin D1 (X1,Z1) ∧ · · · ∧ HTseitin Dm (X1,Zm), where the sets Z1, . . . , Zm are pairwise disjoint, returns a dSDNNF circuit computing f(X)∧D1(X1)∧· · ·∧Dm(Xm).

4.2 Proof Sketch of Theorem 9

The only real hurdle in the proof of Theorem 9 is (1), that is, encoding the system of constraints F(X) = c1(X1) ∧ · · · ∧ cm(Xm) into the CNF H(X, Z) while controlling the incidence treewidth. For every i ≤ m we do the following. First, using a certain tree decomposition of F's incidence graph, we construct a vtree τci over Xi. Second, we construct an SDNNF circuit Di(Xi) structured by τci that computes ci(Xi). Next, we encode Di into a CNF formula Hi(Xi,Zi) using the Tseitin encoding and a set Zi of fresh auxiliary variables. The CNF encoding of F is then H(X,Z) := H1(X1,Z1) ∧ · · · ∧Hm(Xm,Zm). Given the vtrees τci , it should be quite clear that H(X,Z) can be constructed in polynomial time under Assumption 8, and that the Z variables can be forgotten using Lemma 12. So we only need to justify that the τci can be found efficiently, and that the incidence treewidth of H(X, Z) can be controlled.

Constructing the vtrees. To construct the vtree τc for c ∈ F, we need a tree decomposition (t.d.) of GF with specific properties. We do not give the details here but, basically, we use nice t.d. in which a few bags are cloned. Roughly put, τc shows how the variables of c appear relative to each other in the t.d. For instance, in the t.d. shown Figure 2c (not of the type used in the proof, but sufficient for the example) for the incidence graph of Figure 2a, we have x2, x3 and x4, x5 are introduced in a different branches, and this yields the vtree τc2 shown Figure 2b. τc is found using the following lemma.

Lemma 13. Every tree decomposition (t.d.) of GF can be transformed in linear time into another t.d. (T, b) of GF , that has the same width, and that can be used to find in linear time a vtree τc over var(c) for every c ∈ F. Each vtree τc has a t.d. (T, bc) of width 2 such that, for all t ∈ V (T),

It may seem bizarre that Lemma 13 looks at t.d. for vtrees. The key point here is that the vtrees have width2 t.d. with the same underlying tree T as the t.d. of GF . For instance, a t.d. (T, bc2 ) for τc2 from Figure 2b using the same tree T as the t.d. from Figure 2c could use bc2 (t1) = { 1 }, bc2 (t2) = { 1 , 3 }, bc2 (t3) = { 3 , x4}, bc2 (t4) = { 3 , x5}, bc2 (t7) = { 1 , 2 }, bc2 (t8) = { 2 , x3}, bc2 (t9) = { 2 , x2} and all the other bags empty.

Controlling the treewidth of the encoding. Thanks to the properties stated in points i. and ii. of Lemma 13, we can merge the t.d. (T, bc) of τc with the t.d. (T, b) of GF with a simple bag-wise union to get a t.d. of GF ∪τc (the graph with vertex set V (GF )∪V (τc) and with edge set E(GF )∪E(τc)).

Lemma 14. Let G and G′ be two graphs and let Vs := V (G)∩V (G′ ). Let (T, b) and (T ′ , b′ ) tree decompositions of G and G′ , respectively. If T = T ′ and if for all t ∈ V (T) we have b(t) ∩ Vs ⊆ b′ (t) ∩ Vs then (T, b ∪ b′ ) is a tree decomposition of G ∪ G′ .

If we merge (T, b) with all the t.d. (T, bc1 ), . . . , (T, bcm ) obtained from Lemma 13 then we obtain a t.d. (T, b∗ ) of GF ∪ τc1 ∪ · · · ∪ τcm of width at most 2 · width(T, b) because, by property i., new elements are added to a bag b(t) only from the vtrees τc such that c ∈ b(t), and each vtree contributes at most 2 elements.

Now suppose we have a complete DNNF circuit Di computing ci and respecting the vtree τci . Every gate of Di and, by extension, every clause and every auxiliary variable of its Tseitin encoding, is mapped to a node of τci . We claim that, if for every bag b∗ (t) and every node s of τci in this bag, one replaces s by the clauses clauses(Tseitin(g)) and the auxiliary variables used in these clauses for all gates g of Di mapped to s, then the result is a t.d. (T, b+) of GF ∪ GH1 ∪ · · · ∪ GHm = GF ∪ GH. One then just have to remove the initial constraints of F from every bag to obtain a t.d. of GH. Going back to our example, if D2 is the SDNNF circuit shown in Figure 2b, one would replace all occurrences of the vtree node 2 in b∗ (t) by the clauses and variables used in the Tseitin encoding of the nodes squared in red in Figure 2b: each such gate g with input g1 and g2 will contribute the clauses of Tseitin(g) plus the variables zg, zg1 and zg2 when they are not input variables of D2.

Since every ci is w-slim for complete SDNNFs, at most w gates of Di is mapped to s, and the Tseitin encoding generates a constant number of clauses and auxiliary variables per gate of Di. So we will have that |b+(t)| ∈ O(w|b∗ (t)|) ∈ O(w|b(t)|). So, if we started from a t.d. of GF of width O(twi(F)) (computable in time FPT parameterized by twi(F) [Bodlaender, 1996]), then we end up with an CNF encoding H whose incidence treewidth is O(w · twi(F)).

In the detailed proof, available in the long version of the paper, we directly merge the tree decompositions of the CNF encodings Hi, whose incidence treewidth we control using the following lemma for D = Di and τ = τci . This is equivalent to what we have just explained.

Lemma 15. Let D(Y ) be a complete SDNNF circuit whose respecting (τ, λ). Let T = (T, b) be a tree decomposition of τ and let ϕ be defined as ϕ(x) = {x} for every variable x and as ϕ(s) = ⋃g:λ(g)=s var(Tseitin(g)) ∪ clauses(Tseitin(g)) for every internal node s ∈ τ. Let b′ (t) = ⋃s∈b(t) ϕ(s). Then (T, b′ ) is a tree decomposition of HTseitin D 's incidence graph and has width O(width(D)width(T )).

4.3 Lower Bounds for Systems of SlimConstraints

Theorem 9 requires a compilation time with a 2O(w·k) component, with k = twi(F ) and w an upper bound on the width of complete SDNNF circuits representing the constraints. Can we get rid of w in the exponent? The answer is negative due to Lemma 7. One can use the hard functions from this lemma as constraints and show that w cannot be dropped from the exponent in the compilation time simply by considering systems made of a single constraint (so of incidence treewidth 1). The hard functions of Lemma 7 are specific monotone DNF formulas and the proof uses d-SDNNF lower bounds shown by Amarilli et al. [2020]. But DNF formulas can be converted in linear time in SDNNF circuits, so the hard functions for Lemma 7 admit SDNNF circuits of width polynomial in the number n of variables, whereas they only have OBDD representations of width exponential in n. Thus it could be possible that the best running time of an FPT compilation to d-SDNNF is of the form f(w+k)poly(n+w) when w is the SDNNF-width, but also of the form f(k)poly(n+w) when w is the OBDD-width. We can prove that, even for classes of functions that are w-slim for OBDDs, we cannot remove w from f 's argument.

Theorem 16. For every k, there exist systems of constraints

representable by one-sided STS of constant size when k = O(1)

over n variables and of incidence treewidth O(k) whose d-SDNNF representations all have size (n/k)Ω(k) , whereas these systems only comprise constraints that are O(nk)-slim for OBDDs.

The hard systems are CSP (constraints satisfaction problems) encodings of W[1]-hard problems. It seems unlikely that there exist FPT-reductions parameterized by incidence treewidth of W[1]-hard problems to CSP where all constraints are O(1)-slim for complete OBDDs. Indeed, using Theorem 9 plus the fact that deciding the satisfiability of a d-SDNNF circuit is straightforward, the existence of such reductions would imply FPT = W[1]. So, to find hard systems of constraints for the theorem, we started from a W[1]-hard problem with parameter k and reduced it to a CSP of incidence treewidth O(k) and whose constraints are all O(nk)-slim for OBDDs (and not O(1)-slim). We have used the problem k-CLIQUE. The reduction is inspired by that used by Samer and Szeider [2010, Theorem 6] for kINDEPENDENTSET.

5 Faster Model Counting

In this section, we show that model counting for three special cases of systems of constraints that are O(1)-slim for OBDDs can be done faster than by compiling the system as in Section 4 and counting from the compiled form. To this aim, we provide an FPT algorithm based on dynamic programming over a nice tree-decomposition of the incident graph of the system. We start with describing the algorithm for systems of literal-symmetric functions that are O(1)-slim for OBDDs, and then show that the speed of the algorithm can be improved when we consider even more particular cases, namely systems of one-sided constraints and systems of a mixture of CNF clauses and modulo constraints. All results in this section are stated in the unit-cost model, where every arithmetic operation is counted as an elementary operation.

5.1 Algorithm

In Section 3.2, we have shown that literal-symmetric functions that are O(1)-slim for OBDDs are precisely the functions described by a CSTS of constant size modulo literalflipping. We use the latter representation and provide an FPT algorithm for model counting for a system of such constraints. The algorithm is based on dynamic programming over a nice tree decomposition of the incident graph of the system and is parameterized by the treewidth k of the incident graph of the system and the maximum state size w of its constraints. Throughout the entire section, we assume w ≥ 2.

Theorem 17. Let F be a system of constraints whose maximum state size is w, and let T = (T, b) be a nice width-k tree decomposition of the incidence graph GF . Then, given F and T , one can count the number of models of F with O(w2k · |GF |) elementary operations.

The idea for the algorithm is to perform dynamic programming over the nice tree decomposition. Let F, T be as in Theorem 17. For each node t of T, let Tt denote the subtree of T rooted at t, let Ft and Vt be the set constraints and the set of variables that appear in the bags of Tt, respectively. We write bF (t) = b(t) ∩ F , and bV (t) = b(t) ∩ var(F) for the set of constraints and variables in b(t), respectively. For all t ∈ T, let ˜ Vt := Vt \ bV (t). For each c ∈ bF (t), let (Sc , f c 0 , f c 1 , sc0 , T c ) be a minimal CSTS that describes c modulo literal-flipping and let ϕc be the literal-flipping that witnesses this. We fix this choice of CSTS before the start of the algorithm. Let δc be the corresponding extended transition function. For each F ′ ⊆ F , let S(F ′ ) := {R ⊆ ⋃c∈F ′ {c} × Sc | for each c ∈ F ′ there is a unique s s.t. (c, s) ∈ R}. Given F ′ ⊆ F, c ∈ F ′ and ¯ s ∈ S(F ′ ), we use sc to denote the unique s such that (c, s) ∈ ¯ s. Define a binary operation + on S(F ′ ) by ¯ s1+¯ s2 := ¯ s where sc = sc1+sc2 . For each c ∈ F , we use c+ to denote the set of variables xi that occur in c with ϕc (xi) = xi, and c- the set of variables xi that occur in c with ϕc (xi) = ¯xi. For any partial assignment τ to the variables, let q0(τ, c) := |{v ∈ c+ | τ (v) = 0}| + |{v ∈ c- | τ (v) = 1}| and q1(τ, c) := |{v ∈ c+ | τ(v) = 1}| + |{v ∈ c- | τ(v) = 0}|. Finally let δc [τ] := δc (1q1(τ,c) 0q0(τ,c) ).

Definition 18. For each assignment α : bV (t) → {0, 1} and ¯ s ∈ S(bF (t)), we define N(t, α, ¯ s) as the set of assignments τ : Vt → {0, 1} for which the following conditions hold: (1.) τ(v) = α(v) for all variables v ∈ bV (t). (2.) For each c ∈ bF (t), δc [τ|˜ Vt ] = sc . (3.) For each c ∈ Ft \ bF (t), δc [τ ] ∈ T c .

We represent the values of n(t, α, ¯ s) = |N(t, α, ¯ s)| for all α : bV (t) → {0, 1} and ¯ s ∈ S(bF (t)) by a table Mt with |b(t)| + 1 columns and 2|bV (t)| · |S(bF (t))| ≤ 2|bV (t)| · w|bF (t)| ≤ wk rows. The first |bV (t)| columns of Mt contain Boolean values encoding α(v) for variables v ∈ bV (t), followed by |bF (t)| columns, one for each c ∈ bF (t) with the entry sc . The last column contains the integer n(t, α, ¯ s).

The following lemmas show how to compute the table Mt for a node t ∈ T depending on its type, assuming the tables of its children have already been computed.

Lemma 19. Let t be a join node with children t1, t2. For each assignment α : bV (t′ ) → {0, 1}, and ¯ s ∈ S(bF (t)), we have

Lemma 20. Let t be an introduce node with child t′ . For each truth assignment α : bV (t′ ) → {0, 1}, and ¯ s ∈ S(bF (t′ )), we have the following equalities depending on whether it is a variable or a constraint that is introduced at t.

1. A variable v is introduced. We have

1. A constraint c is introduced. We have

Lemma 21. Let t be a forget node with child t′ . For each truth assignment α : bV (t) → {0, 1}, and ¯ s ∈ S(bF (t)), we have the following two equalities depending on whether it is a variable or a constraint that is forgotten at t.

1. A variable v is forgotten. Let α0 and α1 denote the extension to α that sets v to 0 and 1, respectively. We have

where σ1(v, ¯ s′ ) is the set

and σ0 is defined similarly by exchanging f c 0 and f c 1 .

2. A constraint c is forgotten. We have

Lemma 22. Let t be a leaf node. For each truth assignment α : bV (t) → {0, 1} and ¯ s ∈ S(bF (t)), we have

5.2 One-Sided andModulo Constraints

A close inspection of the proof of Theorem 17 reveals that the bottleneck lies in the computation of the table Mt for a join node t. In fact, if we restrict ourselves to more particular cases of systems of constraints, namely systems of onesided constraints and systems of disjunctive clauses and modulo constraints, we can speed-up the algorithm by computing the tables for join nodes faster, using advanced techniques like the Convolution Theorem and fast Fourier transform (see, e.g., Bj¨orklund et al., 2007, Slivovsky and Szeider, 2020).

We call a constraint one-sided when there exists an STS that describes it where either f0(s) = s for every state s, or f1(s) = s for every state s. In the first case, we talk of 1-only constraints and STS, and in the second case, we talk of 0-only constraints and STS. Throughout this section, we assume that for each one-sided constraint c ∈ F, a minimal one-sided STS that describes it is known before the algorithm starts. Given a one-sided constraint c, if c is a 1-only (resp. 0-only) constraint, then let c(i) denote the state the STS is in after receiving i many 1's (resp. i many 0's).

Theorem 23. Let F be a system of one-sided constraints of maximal state size w. Given F and a width-k tree decomposition of GF , one can compute the number of models of F in O((2w)k k log(w) · |GF |) elementary operations.

Let m ∈ N, an m-modulo constraint c is a constraint such that, for all x1, . . . , xn, x′1 , . . . , x′n ∈ {0, 1} verifying ∑i∈[n] xi = ∑i∈[n] x′i mod m, we have c(x1, . . . , xn) = c(x′1 , . . . , x′n ). Note that every m-modulo constraint is 1only. We assume that the CSTS chosen for a disjunctive clause is always as shown in Figure 1, where c(0) = s0 and c(i) = s1 for all i > 0.

Theorem 24. Let w be a natural number. Let F be a system of constraints comprising only clauses and m-modulo constraints for possibly different m ≤ w. Given F and a width-k tree decomposition of GF , one can compute the model count of F in O(wk k log(w) · |GF |) elementary operations.

Since XOR constraints are 2-modulo constraints, we obtain the following corollary.

Corollary 25. Let F be a system of clauses and XOR constraints. Given F and a width-k tree decomposition of GF , one can compute the model count of F in O(2k k · |GF |) elementary operations.

6 Conclusion

We have shown that the compilation of systems of constraints parameterized by incidence treewidth to d-SDNNF is FPT for specific families of constraints, namely, constraints whose OBDD- and SDNNF-width are bounded by a constant for all variable orders and all vtrees. This generalizes known results for CNF, i.e., systems of disjunctive clauses, to many more constraints, including modulo and small-threshold constraints. Since compilation to d-SDNNF is often used in practice as a first step towards model counting, we have also shown that faster FPT model counting algorithms exist without compilation when we restrict the constraints considered. A natural question here is whether one can push our results further, that is, to constraints that do not belong to the families considered in this paper. It seems that positive compilation results can always be established by reduction to the compilation of CNF formulas (in this paper, CNF encodings of the constraints). We also ask if there are situations where encoding the problem to CNF before compiling is provably a worse strategy than reasoning on the original problem.

Acknowledgments

The research leading to this publication has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement No. 101034440, and was supported by the Vienna Science and Technology Fund (WWTF) within the project ICT19-065 and

from the Austrian Science Fund (FWF) within the projects

10.55776/ESP235, 10.55776/P36688, and 10.55776/P36420.