Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Compilability Thresholds of 2-CNF to OBDD

Alexis de Colnet, Alfons Laarman, Joon Hyung Lee

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,δn)$, the uniform distribution over all 2-CNFs with $δn$ clauses and $n$ variables, with $δ\geq 0$ a constant. We show that, with high probability, the random 2-CNF admits OBDDs of size polynomial in $n$ if $0 \leq δ< 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.

The Compilability Thresholds of 2-CNF to OBDD

Abstract

We prove the existence of two thresholds regarding the compilability of random 2-CNF formulas to OBDDs. The formulas are drawn from , the uniform distribution over all 2-CNFs with clauses and variables, with a constant. We show that, with high probability, the random 2-CNF admits OBDDs of size polynomial in if or if . On the other hand, for , with high probability, the random -CNF admits only OBDDs of size exponential in . It is no coincidence that the two ``compilability thresholds'' are and . Both are known thresholds for other CNF properties, namely, is the satisfiability threshold for 2-CNF while is the treewidth threshold, i.e., the point where the treewidth of the primal graph jumps from constant to linear in with high probability.
Paper Structure (17 sections, 33 theorems, 21 equations, 2 figures)

This paper contains 17 sections, 33 theorems, 21 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Known Threshold Phenomena for CNF and Graphs
  3. Random CNF
  4. Random Graphs and Graph Parameters
  5. Compilability Thresholds
  6. Compilability Threshold for Monotone $k$-CNF
  7. Compilability Thresholds for $2$-CNF
  8. Random 2-CNF with Clause Replacement
  9. The Distribution $\mathcal{H}\xspace_2(n,m)$
  10. High Treewidth in $\mathcal{H}\xspace_2(n,\delta n)$
  11. From Large Treewidth to Large Matchings
  12. Large Matchings in $\mathcal{H}\xspace_2(n,\delta n)$
  13. Matching on the First $n^{1/3}$ Clauses
  14. Lower Bounds on the OBDD-Size
  15. Proof of Lemma \ref{['lemma:technical-lemma']}
  16. ...and 2 more sections

Key Result

Theorem 1

Let $\delta \geq 0$, $n \in \mathbb{N}$ and $F$ be a random formula following $\mathcal{F}\xspace_2(n,\delta n)$. There are constants $c,d > 0$ such that,

Figures (2)

  • Figure 1: The satisfiability and primal treewidth thresholds for $\mathcal{F}\xspace_2(n,\delta n)$.
  • Figure 2: The thresholds for the OBDD-size of formulas in $\mathcal{F}\xspace_2(n,\delta n)$.

Theorems & Definitions (36)

  • Theorem 1: Compilability Thresholds of 2-CNF to OBDD
  • Theorem 2: Satisfiability threshold for 2-CNF, ChvatalR92Goerdt96
  • Theorem 3: Treewidth threshold for graphs lee2012rank
  • Corollary 4
  • Corollary 4: Treewidth threshold for 2-CNF
  • Definition 5: OBDD-size
  • Theorem 6: amarilli2020connecting
  • Lemma 6
  • Theorem 7: Compilability Thresholds for monotone 2-CNF
  • Theorem 7: Compilability Thresholds of 2-CNF to OBDD
  • ...and 26 more