# What's the correlation between treewidth and instance hardness for random 3-SAT?

This recent paper from FOCS2013, Strong Backdoors to Bounded Treewidth SAT by Gaspers and Szeider talks about the link between the treewidth of the SAT clause graph and instance hardness.

For random 3-SAT, i.e. 3-SAT instances chosen at random, what is the correlation between treewidth of the clause graph and instance hardness?

"Instance hardness" can be taken as "hard for a typical SAT solver", i.e. running time.

I am looking for either theoretical or empirical style answers or references. To my knowledge, there do not seem to be empirical studies on this. I am aware there are somewhat different ways to build SAT clause graphs, but this question is not focused on the distinction.

Maybe a natural closely related question is how treewidth of the clause graph relates to the 3-SAT phase transition.

A random k-SAT instance on $n$ variables where each variable occurs in $3$ clauses will be an expander graph, and therefore have treewidth $\theta(n)$ with high probability. This holds in the model where we fix an n and an m (with 3n = km), and pick uniformly at random a formula with n variables and m clauses such that all variables are in exactly 3 clauses. It also holds in the Erdős–Rényi model with probability set so that variables have average degree $3$.
On the other hand this density is well below the k-SAT phase transition; by the Lovasz Local Lemma all $d$-regular $k$-SAT instances are satisfiable for $4 \cdot \frac{1}{2^k} \cdot dk \leq 1$, i.e when $d \leq \frac{2^k}{4k}$
For the other part of your question I'd expect (but I haven't tested this so I don't really know) that SAT solvers should be able to exploit at least some of the symmetries that occur because of all the balanced separators in a bounded treewidth graph: In a k-SAT instance of treewidth $t$ there is a set of variables of size $t$ so that after you branch on these variables the formula breaks up into connected components with less than $n/2$ variables in each.
• @vzn My point is more that in the most common random models the treewidth goes through the roof way before the instances become computationally hard. On the other hand real life'' instances probably have much smaller treewidth than random ones and I sort of expect SAT solvers to take (some) advantage of this. – daniello Oct 22 '14 at 18:40