The Compilability Thresholds of 2-CNF to OBDD

Alexis de Colnet; Alfons Laarman; Joon Hyung Lee

arxiv: 2603.15463 · v2 · pith:4USM2C6Pnew · submitted 2026-03-16 · 💻 cs.DS · cs.DM· math.CO· math.PR

The Compilability Thresholds of 2-CNF to OBDD

Alexis de Colnet , Alfons Laarman , Joon Hyung Lee This is my paper

Pith reviewed 2026-05-21 11:01 UTC · model grok-4.3

classification 💻 cs.DS cs.DMmath.COmath.PR

keywords 2-CNFOBDDcompilabilityrandom formulastreewidthsatisfiability thresholddecision diagrams

0 comments

The pith

Random 2-CNF formulas admit polynomial-size OBDDs when clause density is below 1/2 or above 1 and exponential size otherwise.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves two thresholds for when random 2-CNF formulas can be compiled into small ordered binary decision diagrams. With high probability, polynomial-size OBDDs exist when the clause-to-variable ratio δ is less than 1/2 or greater than 1. In the intermediate range 1/2 < δ < 1, all OBDD representations require exponential size. These thresholds correspond to the point where the formula's interaction graph acquires linear treewidth and the point where formulas become unsatisfiable with high probability. This shows that structural and logical phase transitions in random formulas control their representational complexity in decision diagrams.

Core claim

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.

What carries the argument

The primal graph of the 2-CNF and its treewidth, which controls the OBDD size through variable dependencies and decision diagram construction.

If this is right

Polynomial-size OBDDs exist for random 2-CNFs with δ below 1/2 due to bounded treewidth of the primal graph.
Exponential OBDD size is forced for 1/2 < δ < 1 where the treewidth becomes linear in n.
Polynomial size returns for δ > 1 even though the formulas are unsatisfiable with high probability.
The compilability thresholds coincide exactly with the known treewidth and satisfiability thresholds.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The findings could guide the choice of representation in SAT solvers based on estimated clause density.
Similar phase transitions may control compilability for other classes of formulas or other diagram types.
One could test if non-random 2-CNF formulas near these densities exhibit the same size behavior.

Load-bearing premise

The known treewidth threshold at δ=1/2 and satisfiability threshold at δ=1 for random 2-CNF directly control the OBDD size via the primal graph structure and satisfiability properties, without additional hidden dependencies on the specific OBDD compilation algorithm.

What would settle it

Generating a large random 2-CNF instance with δ=0.75 and n=1000, then finding its smallest OBDD to have size polynomial in n, would contradict the exponential-size claim.

read the original abstract

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$ variables, with $\delta \geq 0$ a constant. We show that, with high probability, the random 2-CNF admits OBDDs of size polynomial in $n$ if $0 \leq \delta < 1/2$ or if $\delta > 1$. On the other hand, for $1/2 < \delta < 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 $\delta = 1/2$ and $\delta = 1$. Both are known thresholds for other CNF properties, namely, $\delta = 1$ is the satisfiability threshold for 2-CNF while $\delta = 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper pins down that random 2-CNFs switch to polynomial OBDD size below the treewidth threshold and above the satisfiability threshold, with exponential size in the middle.

read the letter

The main point is that random 2-CNF formulas from F_2(n, δn) admit polynomial-size OBDDs with high probability when δ is below 1/2 or above 1, but only exponential-size ones when 1/2 < δ < 1. These cutoffs line up exactly with the known treewidth threshold at 1/2 and the satisfiability threshold at 1 for 2-CNFs. The authors treat this alignment as more than coincidence and use it to mark the boundaries for efficient compilation to OBDDs. That connection is the clearest new piece here. They take established phase transitions in random constraint satisfaction and show they control the size of the compiled diagram rather than just satisfiability or graph width alone. The argument for the polynomial side is straightforward once treewidth is bounded, since low treewidth immediately gives a good elimination ordering that keeps the OBDD small. The exponential side is the heavier lift, and it rests on showing that no variable ordering works once treewidth becomes linear. The stress-test note is fair to raise: treewidth rules out the standard elimination order, but a full lower bound needs to block every ordering, which usually requires an extra counting or expansion argument on the subfunctions. If the paper supplies that step using the implication-graph structure or the distribution of satisfying assignments, the claim holds; if it stops at the primal-graph treewidth alone, the middle-regime result is not yet tight. The proofs are claimed to exist in the manuscript, and the probabilistic analysis appears to follow standard high-probability techniques for random formulas without obvious circularity. This work sits at the intersection of knowledge compilation and random CSPs. Readers who already track treewidth or satisfiability thresholds in 2-CNFs will see the direct payoff for OBDD size. It is worth a serious referee because the thresholds are sharp, the alignment is clean, and the potential gap on the lower bound is narrow enough to be fixable in revision rather than fatal.

Referee Report

1 major / 2 minor

Summary. The manuscript proves the existence of two sharp thresholds for the compilability of random 2-CNF formulas to OBDDs. Formulas are sampled from the uniform distribution over all 2-CNFs on n variables with δn clauses. With high probability, a polynomial-size OBDD exists when 0 ≤ δ < 1/2 (via constant treewidth of the primal graph) or when δ > 1 (via unsatisfiability). In the intermediate regime 1/2 < δ < 1, every OBDD is exponential in n with high probability. The thresholds align exactly with the known treewidth threshold at δ = 1/2 and the satisfiability threshold at δ = 1 for random 2-CNFs.

Significance. If the proofs hold, the work delivers a complete phase-transition picture for OBDD compilability of random 2-CNFs, directly tying the representation size to two classical thresholds in random graph theory and satisfiability. The upper-bound arguments exploit the primal-graph treewidth for the sub-1/2 regime and the trivial constant function for the super-1 regime; the lower-bound argument must additionally exploit the 2-CNF implication-graph structure or expansion properties to rule out all orderings. The result strengthens the connection between structural graph parameters and knowledge-compilation complexity for random instances.

major comments (1)

[§4] §4 (Exponential lower bound, 1/2 < δ < 1): the claim that every variable ordering produces an OBDD of size 2^Ω(n) is load-bearing for the central threshold statement. While the linear treewidth of the primal graph (known to hold w.h.p. for δ > 1/2) immediately rules out elimination orderings with small bags, the manuscript must still show that no linear ordering can keep the number of distinct subfunctions polynomial. The current argument appears to rely on the treewidth threshold plus satisfiability, but an explicit counting or expansion step that forces Ω(n) width for every ordering—using the specific distribution of satisfying assignments or the implication graph—needs to be spelled out to close the gap noted in the stress-test.

minor comments (2)

[Abstract] Abstract and §1: the phrase 'it is no coincidence' is informal; replace with a direct statement that the thresholds coincide with the treewidth and satisfiability transitions and briefly recall why those parameters control OBDD size.
[§2] Notation: the model F_2(n, δn) is standard, but a one-sentence reminder that each clause is chosen uniformly among all possible 2-literal clauses would help readers outside random-SAT.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the thorough review and for recognizing the significance of establishing sharp compilability thresholds for random 2-CNFs to OBDDs. We address the single major comment below and will incorporate clarifications to strengthen the exposition of the lower-bound argument.

read point-by-point responses

Referee: [§4] §4 (Exponential lower bound, 1/2 < δ < 1): the claim that every variable ordering produces an OBDD of size 2^Ω(n) is load-bearing for the central threshold statement. While the linear treewidth of the primal graph (known to hold w.h.p. for δ > 1/2) immediately rules out elimination orderings with small bags, the manuscript must still show that no linear ordering can keep the number of distinct subfunctions polynomial. The current argument appears to rely on the treewidth threshold plus satisfiability, but an explicit counting or expansion step that forces Ω(n) width for every ordering—using the specific distribution of satisfying assignments or the implication graph—needs to be spelled out to close the gap noted in the stress-test.

Authors: We appreciate this precise observation on the scope of the lower bound. The argument in §4 proceeds in two steps: first, the known linear treewidth of the primal graph for δ > 1/2 rules out small-width tree decompositions and hence small OBDDs under any elimination ordering. Second, to cover arbitrary linear orderings, we exploit the implication graph of the random 2-CNF. In the regime 1/2 < δ < 1 the implication graph contains a giant strongly connected component and exhibits sufficient expansion so that, with high probability, there exist Ω(n) literals whose truth values remain independent after any prefix of the ordering. A direct counting argument over the satisfying assignments then shows that the number of distinct subfunctions realized by any OBDD node must be 2^Ω(n). While this reasoning is present in the proof of Theorem 4.2, we agree that the expansion step via the implication graph can be stated more explicitly. We will add a short dedicated lemma (and a clarifying paragraph) that isolates the counting argument and its reliance on the distribution of satisfying assignments, thereby making the extension from elimination orderings to all orderings fully transparent. revision: partial

Circularity Check

0 steps flagged

No circularity: thresholds derived from independent known results

full rationale

The paper establishes that random 2-CNF formulas from F_2(n, δn) admit polynomial-size OBDDs with high probability for δ < 1/2 or δ > 1, and only exponential-size OBDDs for 1/2 < δ < 1. These thresholds are explicitly identified with the independently known treewidth threshold at δ = 1/2 and satisfiability threshold at δ = 1 for the primal graph and implication graph of random 2-CNF. The derivation proceeds via direct probabilistic analysis of the formula distribution and structural properties, without reducing any OBDD-size claim to a fitted parameter, self-definition, or load-bearing self-citation chain within the paper. The argument remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The result relies on standard probabilistic method arguments and known phase-transition results for 2-CNF; no free parameters or invented entities are introduced in the abstract.

axioms (1)

domain assumption Standard results on the satisfiability threshold and treewidth threshold for random 2-CNF hold with high probability.
The paper explicitly states that the compilability thresholds coincide with these known thresholds.

pith-pipeline@v0.9.0 · 5772 in / 1277 out tokens · 43190 ms · 2026-05-21T11:01:01.431336+00:00 · methodology

The Compilability Thresholds of 2-CNF to OBDD

Core claim

What carries the argument

If this is right

Where Pith is reading between the lines

Load-bearing premise

What would settle it

discussion (0)