Related papers: On Compiling Structured CNFs to OBDDs
We prove the existence of two thresholds regarding the compilability of random 2-CNF formulas to OBDDs. The formulas are drawn from $\mathcal{F}_2(n,\delta n)$, the uniform distribution over all 2-CNFs with $\delta n$ clauses and $n$…
In this paper we show that a CNF cannot be compiled into an Ordered Binary Decision Diagram (OBDD) of fixed-parameter size parameterized by the primal graph treewidth of the CNF. Thus we provide a parameterized separation between OBDDs and…
We introduce Tree Decision Diagrams (TDD) as a model for Boolean functions that generalizes OBDD. They can be seen as a restriction of structured d-DNNF; that is, d-DNNF that respect a vtree $T$. We show that TDDs enjoy the same…
We show unconditional parameterized lower bounds in the area of knowledge compilation, more specifically on the size of circuits in decomposable negation normal form (DNNF) that encode CNF-formulas restricted by several graph width…
In this paper we study complexity of an extension of ordered binary decision diagrams (OBDDs) called $c$-OBDDs on CNFs of bounded (primal graph) treewidth. In particular, we show that for each $k$ there is a class of CNFs of treewidth $k…
We give a non-FPT lower bound on the size of structured decision DNNF and OBDD with decomposable AND-nodes representing CNF-formulas of bounded incidence treewidth. Both models are known to be of FPT size for CNFs of bounded primal…
Two major considerations when encoding pseudo-Boolean (PB) constraints into SAT are the size of the encoding and its propagation strength, that is, the guarantee that it has a good behaviour under unit propagation. Several encodings with…
In this paper we provide an extended formulation for the class of constraint satisfaction problems and prove that its size is polynomial for instances whose constraint graph has bounded treewidth. This implies new upper bounds on extension…
Decision \textsc{dnnf} (a.k.a. $\wedge_d$-\textsc{fbdd}) is an important special case of Decomposable Negation Normal Form (\textsc{dnnf}), a landmark knowledge compilation model. Like other known \textsc{dnnf} restrictions, Decision…
We introduce a one-sided incidence tree decomposition of a CNF $\varphi$. This is a tree decomposition of the incidence graph of $\varphi$ where the underlying tree is rooted and the set of bags containing each clause induces a directed…
We introduce a new graph parameter called linear upper maximum induced matching width \textsc{lu-mim width}, denoted for a graph $G$ by $lu(G)$. We prove that the smallest size of the \textsc{obdd} for $\varphi$, the monotone 2-\textsc{cnf}…
It is known that any planar graph with diameter D has treewidth O(D), and this fact has been used as the basis for several planar graph algorithms. We investigate the extent to which similar relations hold in other graph families. We show…
We establish a list of characterizations of bounded twin-width for hereditary, totally ordered binary structures. This has several consequences. First, it allows us to show that a (hereditary) class of matrices over a finite alphabet either…
Treewidth and Hadwiger number are two of the most important parameters in structural graph theory. This paper studies graph classes in which large treewidth implies the existence of a large complete graph minor. To formalise this, we say…
The twin-width of a graph $G$ is the minimum integer $d$ such that $G$ has a $d$-contraction sequence, that is, a sequence of $|V(G)|-1$ iterated vertex identifications for which the overall maximum number of red edges incident to a single…
We show that many graphs with bounded treewidth can be described as subgraphs of the strong product of a graph with smaller treewidth and a bounded-size complete graph. To this end, define the "underlying treewidth" of a graph class…
In this paper we study syntactic branching programs of bounded repetition representing CNFs of bounded treewidth. For this purpose we introduce two new structural graph parameters $d$-pathwidth and clique preserving $d$-pathwidth denoted by…
We prove that a hereditary class of graphs is $(\mathsf{tw}, \omega)$-bounded if and only if the induced minors of the graphs from the class form a $(\mathsf{tw}, \omega)$-bounded class.
We consider bounded width CNF-formulas where the width is measured by popular graph width measures on graphs associated to CNF-formulas. Such restricted graph classes, in particular those of bounded treewidth, have been extensively studied…
We prove that a minor-closed class of graphs has bounded layered pathwidth if and only if some apex-forest is not in the class. This generalises a theorem of Robertson and Seymour, which says that a minor-closed class of graphs has bounded…