Tensor networks and circuits are widely used data structures to represent pseudo-Boolean functions. These two formalisms have been studied primarily in separate communities, and this paper aims to establish equivalences between them. We show that some classes of tensor networks that are appealing in practice correspond to classes of circuits with specific properties that have been studied in knowledge compilation as tractable circuits. In particular, we prove that matrix product states (tensor trains) coincide with nondeterministic edge-valued decision diagrams and that tree tensor networks exactly correspond to structured-decomposable circuits. These correspondences enable direct transfer of structural and algorithmic results; for example, canonicity and tractability guarantees known for circuits yield analogous guarantees for the associated tensor networks, and vice versa.

We prove the existence of two thresholds regarding the compilability of random 2-CNF formulas to OBDDs. The formulas are drawn from F₂(n,δn), the uniform distribution over all 2-CNFs with δ n clauses and n variables, with δ ≥ 0 a constant. We show that, with high probability, the random 2-CNF admits OBDDs of size polynomial in n if 0 ≤ δ < 1/2 or if δ > 1. On the other hand, for 1/2 < δ < 1, with high probability, the random 2-CNF admits only OBDDs of size exponential in n. It is no coincidence that the two "compilability thresholds" are δ = 1/2 and δ = 1. Both are known thresholds for other CNF properties, namely, δ = 1 is the satisfiability threshold for 2-CNF while δ = 1/2 is the treewidth threshold, i.e., the point where the treewidth of the primal graph jumps from constant to linear in n with high probability.

We provide the first fully polynomial-time randomized approximation scheme for the following two counting problems:1.Given a Context-Free Grammar \(G\) over alphabet \(\Sigma\), count the number of words of length exactly \(n\) generated by \(G\)2.Given a circuit \(\varphi\) in Decomposable Negation Normal Form (DNNF) over the set of Boolean variables \(X\), compute the number of assignments to \(X\) such that \(\varphi\) evaluates to 1.

Ordered Binary Decision Diagrams (OBDDs) are dynamic data structures with many application areas. The literature suggested that OBDDs of bounded width equate to Boolean circuits of bounded pathwidth. In this paper, we show that this relationship holds only for complete OBDDs. Additionally, we demonstrate that similar limitations affect the claimed equivalence between Sentential Decision Diagrams (SDDs) of bounded width and Boolean circuits of bounded treewidth.

In this work, we study the fundamental problems of counting and sampling traces that a regular language touches. Formally, one fixes the alphabet Σ and an independence relation 𝕀 ⊆ Σ × Σ . The computational problems we address take as input a regular language L over Σ, presented as a finite automaton with m states, together with a natural number n (presented in unary). For the counting problem, the output is the number of Mazurkiewicz traces (induced by 𝕀) that intersect the n th slice L n = L ∩ Σ n , i.e., traces that have at least one linearization in L n . For the sampling problem, the output is a trace drawn from a distribution that is approximately uniform over all such traces. These problems are motivated by applications such as bounded model checking based on partial-order reduction, where an a priori estimate of the size of the state space can significantly improve usability, as well as testing approaches for concurrent programs that use partial-order-aware random sampling, where uniform exploration is desirable for effective bug detection. We first show that the counting problem is #P-hard even when the automaton accepting the language L is deterministic, which is in sharp contrast to the corresponding problem for counting the words of a DFA, which is solvable in polynomial time. We then show that the counting problem remains in the class #P for both NFAs and DFAs, independent of whether L is trace-closed. Finally, our main contributions are a fully polynomial-time randomized approximation scheme (FPRAS) that, with high probability, estimates the desired count within a specified accuracy parameter, and a fully polynomial-time almost uniform sampler (FPAUS) that generates traces while ensuring that the distribution induced on them is approximately uniform with high probability.

Non-deterministic read-once branching programs, also known as non-deterministic free binary decision diagrams (nFBDD), are a fundamental data structure in computer science for representing Boolean functions. In this paper, we focus on #nFBDD, the problem of model counting for non-deterministic read-once branching programs. The #nFBDD problem is #P-hard, and it is known that there exists a quasi-polynomial randomized approximation scheme for #nFBDD. In this paper, we provide the first FPRAS for #nFBDD. Our result relies on the introduction of new analysis techniques that focus on bounding the dependence of samples.

#NFA refers to the problem of counting the words of length n accepted by a non-deterministic finite automaton. #NFA is #P-hard, and although fully-polynomial-time randomized approximation schemes (FPRAS) exist, they are all impractical. The first FPRAS for #NFA had a running time of Õ(n 17 m 17 ε -14 łog(δ -1 )), where m is the number of states in the automaton, δ ∈ (0,1] is the confidence parameter, and ε > 0 is the tolerance parameter (typically smaller than 1). The current best FPRAS achieved a significant improvement in the time complexity relative to the first FPRAS and obtained FPRAS with time complexity Õ((n 10 m 2 + n 6 m 3 )ε -4 łog 2 (δ -1 )). The complexity of the improved FPRAS is still too intimidating to attempt any practical implementation. In this paper, we pursue the quest for practical FPRAS for #NFA by presenting a new algorithm with a time complexity of O(n 2 m 3 łog(nm)ε -2 łog(δ -1 )). Observe that evaluating whether a word of length n is accepted by an NFA has a time complexity of O(nm 2 ). Therefore, our proposed FPRAS achieves sub-quadratic complexity with respect to membership checks.

Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraints with different variable orders (Chew and Heule 2020). We provide an analytical explanation for their hardness by showing that they require exponential resolution refutations with high probability when the variable order is chosen at random. We obtain this result by proving that these formulas, which are known to be Tseitin formulas, have Tseitin graphs of linear treewidth with high probability. Since such Tseitin formulas require exponential resolution refutations, our result follows. We generalize this argument to a new class of formulas that capture a basic form of parity reasoning involving a sum of two random parity constraints with random orders. Even when the variable order for the sum is chosen favorably, these formulas remain hard for resolution. In contrast, we prove that they have short DRAT refutations. We show experimentally that the running time of CDCL SAT solvers on both classes of formulas grows exponentially with their treewidth.

Answer Set Programming (ASP) is a declarative programming approach that captures many problems in knowledge representation and reasoning. To certify an ASP solver's decision, whether the program is consistent or inconsistent, we need a certificate or proof that can be independently verified. This paper proposes the dual proof system ASP-QRAT that certifies both consistent and inconsistent ASPs. ASP-QRAT is based on a translation of ASP to QBF (Quantified Boolean Formus) and the QBF proof system QRAT as a checking format. We show that ASP-QRAT p-simulates ASP-DRUPE, an existing refutation system for inconsistent disjunctive ASPs. We show that ASP-QRAT is conditionally optimal for consistent and inconsistent ASPs, i.e., any super-polynomial lower bound on the shortest proof size of ASP-QRAT implies a major breakthrough in theoretical computer science. The case for consistent ASPs is remarkable because no analog exists in the QBF case.

Top-down compilers of CNF formulas to circuits in decision-DNNF (Decomposable Negation Normal Form) have proved to be useful for model counting. These compilers rely on a common set of techniques including DPLL-style exploration of the set of models, caching of residual formulas, and connected components detection. Differences between compilers lie in the variable selection heuristics and in the additional processing techniques they may use. We investigate, from a theoretical perspective, the ability of top-down compilation algorithms to find small decision-DNNF circuits for two different variable selection strategies. Both strategies are guided by a graph of the CNF formula and are inspired by what is done in practice. The first uses a dynamic graph-partitioning approach while the second works with a static tree decomposition. We show that the dynamic approach performs significantly better than the static approach for some formulas, and that the opposite also holds for other formulas. Our lower bounds are proved despite loose settings where the compilation algorithm is only forced to follow its designed variable selection strategy and where everything else, including the many opportunities for tie-breaking, can be handled non-deterministically.

In this paper, the succinctness of various ML models is studied. To be more precise, the existence of polynomial-time and polynomial-space translations between representation languages for classifiers is investigated. The languages that are considered include decision trees, random forests, several types of boosted trees, binary neural networks, Boolean multilayer perceptrons, and various logical representations of binary classifiers. We provide a complete map indicating for every pair of languages C, C' whether or not a polynomial-time / polynomial-space translation exists from C to C'. We also explain how to take advantage of the resulting map for XAI purposes.

Tseitin-formulas are systems of parity constraints whose structure is described by a graph. These formulas have been studied extensively in proof complexity as hard instances in many proof systems. In this paper, we prove that a class of unsatisfiable Tseitin-formulas of bounded degree has regular resolution refutations of polynomial length if and only if the treewidth of all underlying graphs G for that class is in O(log |V (G)|). It follows that unsatisfiable Tseitin-formulas with polynomial length of regular resolution refutations are completely determined by the treewidth of the underlying graphs when these graphs have bounded degree. To prove this, we show that any regular resolution refutation of an unsatisfiable Tseitin-formula with graph G of bounded degree has length 2Ω(tw(G))/|V (G)|, thus essentially matching the known 2O(tw(G))poly(|V (G)|) upper bound. Our proof first connects the length of regular resolution refutations of unsatisfiable Tseitin-formulas to the size of representations of satisfiable Tseitin-formulas in decomposable negation normal form (DNNF). Then we prove that for every graph G of bounded degree, every DNNF-representation of every satisfiable Tseitin-formula with graph G must have size 2Ω(tw(G)) which yields our lower bound for regular resolution.

We consider the problem Enum·IP of enumerating prime implicants of Boolean functions represented by decision decomposable negation normal form (dec-DNNF) circuits. We study Enum·IP from dec-DNNF within the framework of enumeration complexity and prove that it is in OutputP, the class of output polynomial enumeration problems, and more precisely in IncP, the class of polynomial incremental time enumeration problems. We then focus on two closely related, but seemingly harder, enumeration problems where further restrictions are put on the prime implicants to be generated. In the first problem, one is only interested in prime implicants representing subset-minimal abductive explanations, a notion much investigated in AI for more than thirty years. In the second problem, the target is prime implicants representing sufficient reasons, a recent yet important notion in the emerging field of eXplainable AI, since they aim to explain predictions achieved by machine learning classifiers. We provide evidence showing that enumerating specific prime implicants corresponding to subset-minimal abductive explanations or to sufficient reasons is not in OutputP.

Arithmetic circuits (AC) are circuits over the real numbers with 0/1-valued input variables whose gates compute the sum or the product of their inputs. Positive AC – that is, AC representing non-negative functions – subsume many interesting probabilistic models such as probabilistic sentential decision diagram (PSDD) or sum-product network (SPN) on indicator variables. Efficient algorithms for many operations useful in probabilistic reasoning on these models critically depend on imposing structural restrictions to the underlying AC. Generally, adding structural restrictions yields new tractable operations but increases the size of the AC. In this paper we study the relative succinctness of classes of AC with different combinations of common restrictions. Building on existing results for Boolean circuits, we derive an unconditional succinctness map for classes of monotone AC – that is, AC whose constant labels are non-negative reals – respecting relevant combinations of the restrictions we consider. We extend a small part of the map to classes of positive AC. Those are known to generally be exponentially more succinct than their monotone counterparts, but we observe here that for so-called deterministic circuits there is no difference between the monotone and the positive setting which allows us to lift some of our results. We end the paper with some insights on the relative succinctness of positive AC by showing exponential lower bounds on the representations of certain functions in positive AC respecting structured decomposability.

Knowledge compilation studies the trade-off between succinctness and efficiency of different representation languages. For many languages, there are known strong lower bounds on the representation size, but recent work shows that, for some languages, one can bypass these bounds using approximate compilation. The idea is to compile an approximation of the knowledge for which the number of errors can be controlled. We focus on circuits in deterministic decomposable negation normal form (d-DNNF), a compilation language suitable in contexts such as probabilistic reasoning, as it supports efficient model counting and probabilistic inference. Moreover, there are known size lower bounds for d-DNNF which by relaxing to approximation one might be able to avoid. In this paper we formalize two notions of approximation: weak approximation which has been studied before in the decision diagram literature and strong approximation which has been used in recent algorithmic results. We then show lower bounds for approximation by d-DNNF, complementing the positive results from the literature.