<p>In general one would not expect <em>random</em> instances of SAT to have bounded treewidth, even if they are easy. Here is an example: </p>

<p>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 <a href="http://arxiv.org/abs/1001.0461" rel="nofollow">Erdős–Rényi model</a> with probability set so that variables have average degree $3$.</p>

<p>On the other hand this density is well below the k-SAT phase transition; by the <a href="http://en.wikipedia.org/wiki/Lov%C3%A1sz_local_lemma" rel="nofollow">Lovasz Local Lemma</a> <em>all</em> $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}$ </p>

<p>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. </p>

CC BY-SA 3.0
2014-10-22T15:51:10.860Z
thx for ideas. ofc was not expecting that random instances would have bounded treewidth; the opposite is presumably provable without much difficulty. but its a numeric parameter that can be compared/ correlated with hardness similarly to many other parameters studied in SAT empirical transition point research and some relationship or correlation seems to be expected based on existing research.
vzn
CC BY-SA 3.0
2014-10-22T18:40:45.373Z
@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
CC BY-SA 3.0
2014-10-22T14:53:38.607Z
2014-10-22T18:59:40.383Z
2014-10-22T18:59:40.383Z
daniello
<p>Not really an answer but the closest references I am aware of. There are results available for branch-width. Also, there is at least one empirical study of treewidth of industrial instances.</p>

<ul>
<li><a href="http://igitur-archive.library.uu.nl/math/2007-0725-201706/2005-018.pdf%E2%80%8E" rel="nofollow">Discovering treewidth</a>, H. Bodlaender, 2005. Gives algorithms to compute bounds on treewidth.</li>
<li><a href="http://research.microsoft.com/pubs/145390/MSR-TR-2011-22.pdf" rel="nofollow">Treewidth in Industrial SAT Benchmarks</a>, R. Mateescu, 2011. Uses variations of above algorithms to estimate treewidth of SAT2009 competition benchmarks.</li>
<li><a href="http://www.cs.toronto.edu/~fbacchus/publications/BDPFOCS2004.pdf" rel="nofollow">Algorithms and complexity results for #SAT and Bayesian inference</a>, F. Bacchus S. Dalmao, T. Pitassi, 2003. Relates branch-width to complexity of #SAT, 2003.</li>
<li><a href="http://people.cs.uchicago.edu/~razborov/files/automat_pos.pdf%E2%80%8E" rel="nofollow">Satisfiability, branch-width and tseitin tautologies</a>, Alekhnovich, Razborov, 2002.</li>
</ul>

CC BY-SA 3.0
2013-08-10T02:39:38.430Z
2014-10-21T21:30:56.010Z
2014-10-21T21:30:56.010Z
Vijay D
<p>This recent paper from FOCS2013, <a href="http://arxiv.org/abs/1204.6233">Strong Backdoors to Bounded Treewidth SAT</a> by Gaspers and Szeider talks about the link between the <a href="http://en.wikipedia.org/wiki/Treewidth">treewidth</a> of the SAT clause graph and instance hardness.</p>

<blockquote>
  <p>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?</p>
</blockquote>

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

<p>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.</p>

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

<graph-algorithms><sat><treewidth><random-k-sat><hard-instances>
What's the correlation between treewidth and instance hardness for random 3-SAT?
vzn
# What's the correlation between treewidth and instance hardness for random 3-SAT?

(Asked by: username_0 on 2013-08-09)

This recent paper from FOCS2013, [Strong Backdoors to Bounded Treewidth SAT](http://arxiv.org/abs/1204.6233) by Gaspers and Szeider talks about the link between the [treewidth](http://en.wikipedia.org/wiki/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.

**Tags:** graph-algorithms, sat, treewidth, random-k-sat, hard-instances

---

## 2 answers

### Answer by username_2 on 2013-08-10. Score: 10 | Accepted answer

Not really an answer but the closest references I am aware of. There are results available for branch-width. Also, there is at least one empirical study of treewidth of industrial instances.

* [Discovering treewidth](http://igitur-archive.library.uu.nl/math/2007-0725-201706/2005-018.pdf%E2%80%8E), H. Bodlaender, 2005. Gives algorithms to compute bounds on treewidth.
* [Treewidth in Industrial SAT Benchmarks](http://research.microsoft.com/pubs/145390/MSR-TR-2011-22.pdf), R. Mateescu, 2011. Uses variations of above algorithms to estimate treewidth of SAT2009 competition benchmarks.
* [Algorithms and complexity results for #SAT and Bayesian inference](http://www.cs.toronto.edu/~fbacchus/publications/BDPFOCS2004.pdf), F. Bacchus S. Dalmao, T. Pitassi, 2003. Relates branch-width to complexity of #SAT, 2003.
* [Satisfiability, branch-width and tseitin tautologies](http://people.cs.uchicago.edu/~razborov/files/automat_pos.pdf%E2%80%8E), Alekhnovich, Razborov, 2002.


---

### Answer by username_1 on 2014-10-22. Score: 7

In general one would not expect *random* instances of SAT to have bounded treewidth, even if they are easy. Here is an example:

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](http://arxiv.org/abs/1001.0461) 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](http://en.wikipedia.org/wiki/Lov%C3%A1sz_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.

> **Comments:**
> **username_0**: thx for ideas. ofc was not expecting that random instances would have bounded treewidth; the opposite is presumably provable without much difficulty. but its a numeric parameter that can be compared/ correlated with hardness similarly to many other parameters studied in SAT empirical transition point research and some relationship or correlation seems to be expected based on existing research.  
> **username_1**: @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.  

---

