12
$\begingroup$

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.

Improve this question
$\endgroup$
0

2 Answers 2

Reset to default
10
$\begingroup$

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.

Improve this answer
$\endgroup$
7
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – vzn
    Oct 22, 2014 at 15:51
  • $\begingroup$ @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. $\endgroup$
    – daniello
    Oct 22, 2014 at 18:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.