<p>I'm not sure if this is what you're looking for but there's a sizable literature on the 3-SAT phase transition.</p>

<p><a href="http://www.math.ucla.edu/~percus/Teaching/RIPS/nature.pdf">Monasson, Zecchina, Kirkpatrcik, Selman and Troyansky</a> had a paper in nature that talks about the phase transition of random k-SAT.  They used a parameterization of the ratio of clauses to variables.  For random 3-SAT, they found numerically that the transition point is around 4.3.  Above this point random 3-SAT instances are over constrained and almost surely unsatsifiable and below this point problems are under constrained and satisfiable (with high probability).  <a href="http://arxiv.org/pdf/cs.CC/0309020">Mertens, Mezard and Zecchina</a> use cavity method procedures to estimate the phase transition point to a higher degree of accuracy.</p>

<p>Far away from the critical point, "dumb" algorithms work well for satisfiable instances (walk sat, etc.).  From what I understand, deterministic solver run times grow exponentially at or near the phase transition (see <a href="http://people.cs.ubc.ca/~hutter/previous-earg/EmpAlgReadingGroup/CoaEtAl03.pdf">here</a> for more of a discussion?).</p>

<p>A close cousin of belief propagation, Braunstein, Mezard and Zecchina have introduced <a href="http://arxiv.org/pdf/cs/0212002">survey propagation</a> that is reported to solve satisfiable 3-SAT instances in millions of variables, even extremely close to the phase transition.  Mezard has a lecture <a href="http://www.msri.org/web/msri/online-videos/-/video/showVideo/2297">here</a> on spin glasses (the theory of which he has used in analysis of random NP-Complete phase transitions) and Maneva has a lecture <a href="http://www.msri.org/web/msri/online-videos/-/video/showVideo/1919">here</a> on survey propagation.</p>

<p>From the other direction, it still looks like our best solvers take exponential amount of time to prove unsatisfiability.  See <a href="http://www.math.ias.edu/~avi/PUBLICATIONS/MYPAPERS/B-SW99/bw00journal.pdf">here</a>, <a href="http://www.cs.washington.edu/homes/beame/papers/stockcnf.pdf">here</a> and <a href="https://nats-www.informatik.uni-hamburg.de/intern/proceedings/2002/ECAI/ecai2000/pdf/p0098.pdf">here</a> for proofs/discussion of the exponential nature of some common methods in proving unsatisfiability (Davis-Putnam procedures and resolution methods).</p>

<p>One has to be very careful about claims of 'easiness' or 'hardness' for random NP-Complete problems.  Having an NP-Complete problem display a phase transition gives no guarantee as to where the hard problems are or whether there even are any.  For example, the Hamiltoniain Cycle problem on Erdos-Renyi random graphs is provably easy even at or near the critical transition point.  The Number Partition Problem doesn't seem to have any algorithms that solve it well into the probability 1 or 0 range, let alone near the critical threshold.  From what I understand, random 3-SAT problems have algorithms that work well for satisfiable instances nearly at or below the critical threshold (survey propagation, walk sat, etc.) but no efficient algorithms above the critical threshold to prove unsatisfiability.  This is just state of the art right now and could of course change in the future.</p>

CC BY-SA 2.5
2011-01-19T21:17:13.140Z
I wonder if those any of those "random k-SAT" results transfer to real life SAT instances, in other words if ratio of clauses to variables is still a useful indicator of hardness
Yaroslav Bulatov
CC BY-SA 2.5
2011-01-19T21:22:54.577Z
@Yaroslav, from my experience, no.  Many real world problems (even reductions) have (or introduce) so much structure so as to destroy the randomness that many solvers have been optimized for.  It seems like at some point we might be able to account for that structure somehow and be able to focus only on the randomness portion (or the 'essence' of the random problem) but I don't see any general way of doing that nor do I really know of any examples that employ that strategy.
user834
CC BY-SA 2.5
2011-01-20T13:09:05.707Z
@user834: From my experience, I agree with you. Moreover, as far as I know, nobody has ever invented even some sort of randomness measure, i.e. a function $R(F)$ that, given a CNF formula $F$, returns a value $r \in [0,1]$ which is representative of the degree of randomness $F$ has. Of course such measure would be just an approximation according to some reasonable criteria; however, I'm unaware of anything like that: do you know if anyone has dealt with this before?
Giorgio Camerani
CC BY-SA 2.5
2011-01-19T21:03:57.667Z
2011-01-19T22:48:13.627Z
2011-01-19T22:48:13.627Z
user834
<p>There are lots of sufficient conditions. In some sense, much of theoretical CS has been devoted to the collection of these conditions - fixed parameter tractability, 2-SAT, random 3-SAT of different densities, etc. </p>

CC BY-SA 2.5
2011-01-18T07:44:00.167Z
That's true, one could take any problem X that's easy to solve and say that "any formula that corresponds to problem X is easy". I guess I'm looking for sufficient conditions that are more efficient at summarizing the easy region than "all problems known to be in P", more like what the constructive Lovasz Local Lemma does
Yaroslav Bulatov
CC BY-SA 2.5
2011-01-18T06:32:51.890Z
2011-01-18T06:32:51.890Z
Peter Boothe
<p>there is not a lot of widespread recognition of this concept so far in the literature, but the <em>clause graph</em> of the SAT problem (the graph with one node per clause, and nodes are connected if clauses share variables), as well as other related graphs of the SAT representation, seems to have many basic clues as to how hard the instance will be on average. </p>

<p>the clause graph can be analyzed via all kinds of graph theoretic algorithms, is an apparently natural measure of "structure" and with strong connections to measuring/estimating hardness, and it appears that research into this structure and its implications is still at the very early stages. it is not inconceivable that transition point research, a/the traditional and well-studied way to approach this question, might eventually be bridged into this clause graph structure (to some degree it already has). in other words the transition point in SAT may be seen to exist "because of" the structure of the clause graph.</p>

<p>here is one excellent reference along these lines, a Phd thesis by Herwig, there are many others.</p>

<p>[1] <a href="http://www.st.ewi.tudelft.nl/sat/theses/paul.pdf" rel="nofollow">Decomposing satisfiability problems
 or Using graphs to get a better insight into satisfiability problems</a>, Herwig 2006 (83pp)</p>

CC BY-SA 3.0
2013-02-12T17:57:00.307Z
this is the dependency graph when applying the lovasz local lemma and variants to satisfiability. in that sense, the clause graph has been looked at *a lot*. Shearer characterizes the graphs for which the local lemma holds, and Kolipaka and Szegedy have made Schaefer's result constructive. When you don't know much, please don't infer that no one knows!
Sasho Nikolov
CC BY-SA 3.0
2013-02-12T19:15:58.613Z
shaefers breakdown into a few tractable classes is mentioned in the answer by Zivny but this clause graph analysis is relatively newer, deeper and more nuanced, and more with an empirical flavor. as for the citations you mention, dont seem to be mentioned often in SAT hardness papers/research... there are multiple/parallel intertwined lines of inquiry...
vzn
CC BY-SA 3.0
2013-02-13T00:37:44.453Z
Schaefer was a typo, I meant Shearer. LLL and its variants is *a main tool* in delimiting the hard instances of k-SAT, a google search will reveal tons of references. Shearer's theorem shows which clause graphs guarantee that any SAT instance with that graph is necessarily satisfiable. Look at this survey for detailed connections to hardness thresholds, difficulty of constructing hard instances, algorithms, etc. http://www.disco.ethz.ch/lectures/fs11/seminar/paper/barbara-3.pdf
Sasho Nikolov
CC BY-SA 3.0
2013-02-13T00:41:54.247Z
a general thought: each time you say something is terra incognita there is a strong possibility it is terra incognita *to you*. in any case this kind of comment is useless unless you are an established and published expert in the area. it would be better if you restrict your answers to what **you know** and leave out comments about what you think no one knows.
Sasho Nikolov
CC BY-SA 3.0
2013-02-13T03:46:04.777Z
[LLL](http://en.wikipedia.org/wiki/Lovász_local_lemma) is _one_ tool for analyzing SAT, invented in 1975 with maybe some refinements since then. its a recipe for _sufficient_ easy or hard instances but not _necessary_. other approaches since then do exist that increasingly fill in the gap in novel ways ie extend and bypass it. you must be confusing this answer with something else, there is no use of the term _"terra incognita"_ in the above question. & suggest _you_ confine yourself to the actual written answers & not speculate about what others know or dont know =)
vzn
CC BY-SA 3.0
2013-02-13T03:53:51.683Z
"there is not a lot of widespread recognition of this concept so far in the literature" - not true given the complete characterization of when the clause graph is sufficient for satisfiability. i *am* speaking about this answer. there has been a lot of work on LLL, including Shearer, asymmetric versions, and, crucially, constructive proofs. way more than "maybe some refinements". so i go back to suggesting  you keep your comments/answers to things you know at least a tiny bit about.
Sasho Nikolov
CC BY-SA 3.0
2013-02-13T04:36:19.887Z
sasho, instead of devaluing great new work, why dont you try actually reading something of the Phd thesis cited instead of pointing to decades old ideas? (which yes, it can coexist with & does not replace) it is novel, comprehensive, sometimes empirical, and massively expands on prior approaches, ie is _seminal and groundbreaking_, and imho is very likely to be a strong basis for further research. one might call it a _tour de force_ ... your insistent claim that the clause graph & _(many)_ other approaches from the paper are identical to earlier ideas is unfounded and unsupportable at best...
vzn
CC BY-SA 3.0
2013-02-13T05:32:42.997Z
all I am saying: **your first sentence is wrong**. there is TONS of theoretical and applied research that looks at the clause graph. for another, this *masters* thesis is far from a tour de force, it's barely more than an empirical study of old algorithmic ideas. tree width decompositions and cut decompositions have appeared in many papers before this thesis, some of them referenced.
Sasho Nikolov
CC BY-SA 3.0
2013-02-13T05:51:27.723Z
ok, fine, it might be more accurate to say the clause graph & some of Herwigs other graph-based analytics are maybe not a foremost or prominent method of analyzing hardness esp in the empirically-focused literature. the last sentence is wrong, _masters_ thesis, not Phd thesis, _mea culpa_. however, there seem to be novel/creative approaches in the paper not seen in prior work, and abstract analysis cannot likely uncover all interesting heuristics that are uncovered via empirical approaches... the two approaches intertwine & crosspollinate each other...
vzn
CC BY-SA 3.0
2013-01-30T17:44:23.107Z
2013-01-30T17:44:23.107Z
vzn
<p>this important paper [1] by Toby Walsh is related to the the SAT transition as measured in the clause/variable ratio. however it goes further in measuring a property called <em>constrainedness</em>, $\kappa$. its a rough or maybe natural measure of hardness such that overconstrained or underconstrained problems are easier than constrainedness at a critical intermediate point. </p>

<p>it finds an apparent <a href="http://en.wikipedia.org/wiki/Fractal" rel="nofollow">fractal</a> <a href="http://en.wikipedia.org/wiki/Self_similarity" rel="nofollow">self-similarity</a> structure of hard instances wrt the constrainedess parameter such that as a <a href="http://en.wikipedia.org/wiki/DPLL_algorithm" rel="nofollow">DP(LL)</a> solver during search tends to find subproblems with the same critical constrainedness no matter which variable is chosen next to branch on. there is some further analysis of fractal structure in SAT instances (such as <a href="http://en.wikipedia.org/wiki/Hausdorff_dimension" rel="nofollow">Hausdorff dimension</a> of SAT formulas &amp; connection to hardness) in eg [2,3]</p>

<p>another somewhat interrelated line of inquiry here is the relationship of <a href="http://en.wikipedia.org/wiki/Small-world_network" rel="nofollow">small world</a> graphs to (hard) SAT structure eg [4,5]</p>

<p>of course the standard point in this area applies that a very definitive answer to this question would be inherently close to a <a href="http://en.wikipedia.org/wiki/P_versus_NP_problem" rel="nofollow">P$\stackrel{?}{=}$NP</a> proof, or that such a proof would (will?) be the best/near-final answer to the question.</p>

<p>[1] <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.3267" rel="nofollow">The constrainedness knife edge</a> by Toby Walsh 1998</p>

<p>[2] <a href="http://tianjia.wikispaces.com/file/view/kSAT.pdf" rel="nofollow">SELF-SIMILARITY OF SATISFIABLE BOOLEAN EXPRESSIONS DECIPHERED IN TERMS OF GRAPH DIRECTED ITERATED FUNCTION SYSTEMS</a> by Ni and Wen</p>

<p>[3] <a href="http://www.satisfiability.org/SAT04/programme/117.pdf" rel="nofollow">Visualizing the Internal Structure of SAT Instances (Preliminary Report)</a> Sinz</p>

<p>[4] <a href="http://www.cse.unsw.edu.au/~twalsh/wijcai99.pdf" rel="nofollow">Search in a small world</a> by Walsh 1999</p>

<p>[5] <a href="http://users.cecs.anu.edu.au/~andrews/papers/slater_ai02.pdf" rel="nofollow">Modelling more realistic SAT problems</a> by Slater 2002</p>

CC BY-SA 3.0
2013-02-10T17:38:49.427Z
It's DPLL, not DP(LL) by the way. Also, there is significantly more recent work on the phase transition in SAT (see the work of Achlioptas, for example).
Vijay D
CC BY-SA 3.0
2013-02-10T18:16:50.863Z
there is a DP algorithm that precedes DPLL that has similar behavior. the other answer by user834 mainly mentioned SAT transition point research with many refs but this answer emphasizes a different (but interrelated) angle
vzn
CC BY-SA 3.0
2013-02-11T00:31:53.933Z
I am aware of these algorithms. I was only pointing out the standard typographical convention, which is to write DP, or DPLL, or DPLL(T), or DPLL(Join), for the quantifier-free first order case. No one writes DP(LL) and it adds confusion with DPLL(T) and DPLL(Join)
Vijay D
CC BY-SA 3.0
2013-02-11T16:17:40.303Z
DP(LL) is what was meant as DP+DPLL
vzn
CC BY-SA 3.0
2013-02-10T16:44:13.643Z
2013-02-10T16:44:13.643Z
vzn
<p>It is easy to move all the instances near the "transition" point to as far from the "transition" point as one wishes. The movement involves a polynomial time/space effort.</p>

<p>If instances far from the "transition" point are easier to solve, then those near the transition point must be equally easy to solve. (Polynomial transformations and all.)</p>

CC BY-SA 3.0
2013-02-10T16:04:45.843Z
can you elaborate, or do you have a ref for this?
vzn
CC BY-SA 2.5
2011-01-20T20:58:20.307Z
2011-01-20T20:58:20.307Z
GHR
<p>I guess you know the classical result of Schaefer from STOC'78, but just in case.</p>

<p><a href="http://dx.doi.org/10.1145/800133.804350">10.1145/800133.804350</a></p>

<p>Schaefer proved that if SAT is parametrised by a set of relations allowed in any instance, then there are only 6 tractable cases: 2-SAT (i.e. every clause is binary), Horn-SAT, dual-Horn-SAT, affine-SAT (solutions to linear equations in GF(2)), 0-valid (relations satisfied by the all-0 assignment) and 1-valid (relations satisfied by the all-1 assignment).</p>

CC BY-SA 2.5
2011-01-20T22:10:17.680Z
There is a more recent paper that refine this result: 
The complexity of satisfiability problems: "Refining Schaefer's theorem" Eric Allender, Michael Bauland, Neil Immerman, Henning Schnoor and Heribert Vollmer
Vinicius dos Santos
CC BY-SA 2.5
2011-01-21T12:01:06.647Z
Thank you, here is the doi:  http://dx.doi.org/10.1016/j.jcss.2008.11.001
Standa Zivny
CC BY-SA 3.0
2013-02-02T02:38:48.093Z
Note that these are constraint satisfaction problems and not SAT (although they can be rewritten as SAT instances, but technically, SAT means CSP with OR predicates).
Mahdi Cheraghchi
CC BY-SA 2.5
2011-01-18T12:35:25.843Z
2011-01-18T12:35:25.843Z
Standa Zivny
<p>What are "easy regions" for satisfiability? In other words, sufficient conditions for some SAT solver to be able to find a satisfying assignment, assuming it exists.</p>

<p>One example is when each clause shares variables with few other clauses, due to <a href="http://arxiv.org/abs/0903.0544">constructive proof</a> of LLL, any other results along those lines?</p>

<p>There's <a href="http://www.google.com/search?hl=en&amp;safe=off&amp;q=sufficient+conditions+for+convergence+of+the+sum%E2%80%93product+algorithm&amp;aq=0&amp;aqi=g1g-m9&amp;aql=&amp;oq=%22sufficient+conditions%22+">sizable literature</a> on easy regions for Belief Propagation, is there something along those lines for satisfiability?</p>

CC BY-SA 2.5
2011-01-18T04:13:43.973Z
are you also interested in the random SAT phase transition ?
Suresh Venkat
CC BY-SA 2.5
2011-01-18T05:26:53.680Z
What does the sufficient condition look like? Peter Shor mentioned in another post that SAT instance needs to possess "random structure" to make ratio of clauses to variables relevant. I wonder if this is something that can be encoded into sufficient conditions
Yaroslav Bulatov
<cc.complexity-theory><sat>
Which SAT problems are easy?
Yaroslav Bulatov
# Which SAT problems are easy?

(Asked by: username_0 on 2011-01-18)

What are "easy regions" for satisfiability? In other words, sufficient conditions for some SAT solver to be able to find a satisfying assignment, assuming it exists.

One example is when each clause shares variables with few other clauses, due to [constructive proof](http://arxiv.org/abs/0903.0544) of LLL, any other results along those lines?

There's [sizable literature](http://www.google.com/search?hl=en&safe=off&q=sufficient+conditions+for+convergence+of+the+sum%E2%80%93product+algorithm&aq=0&aqi=g1g-m9&aql=&oq=%22sufficient+conditions%22+) on easy regions for Belief Propagation, is there something along those lines for satisfiability?

**Tags:** cc.complexity-theory, sat
> **Comments:**
> **username_1**: are you also interested in the random SAT phase transition ?  
> **username_0**: What does the sufficient condition look like? Peter Shor mentioned in another post that SAT instance needs to possess "random structure" to make ratio of clauses to variables relevant. I wonder if this is something that can be encoded into sufficient conditions  

---

## 6 answers

### Answer by username_9 on 2011-01-18. Score: 35 | Accepted answer

I guess you know the classical result of Schaefer from STOC'78, but just in case.

[10.1145/800133.804350](http://dx.doi.org/10.1145/800133.804350)

Schaefer proved that if SAT is parametrised by a set of relations allowed in any instance, then there are only 6 tractable cases: 2-SAT (i.e. every clause is binary), Horn-SAT, dual-Horn-SAT, affine-SAT (solutions to linear equations in GF(2)), 0-valid (relations satisfied by the all-0 assignment) and 1-valid (relations satisfied by the all-1 assignment).

> **Comments:**
> **username_10**: There is a more recent paper that refine this result:  The complexity of satisfiability problems: "Refining Schaefer's theorem" Eric Allender, Michael Bauland, Neil Immerman, Henning Schnoor and Heribert Vollmer  
> **username_9**: Thank you, here is the doi:  http://dx.doi.org/10.1016/j.jcss.2008.11.001  
> **username_11**: Note that these are constraint satisfaction problems and not SAT (although they can be rewritten as SAT instances, but technically, SAT means CSP with OR predicates).  

---

### Answer by username_2 on 2011-01-19. Score: 15

I'm not sure if this is what you're looking for but there's a sizable literature on the 3-SAT phase transition.

[Monasson, Zecchina, Kirkpatrcik, Selman and Troyansky](http://www.math.ucla.edu/~percus/Teaching/RIPS/nature.pdf) had a paper in nature that talks about the phase transition of random k-SAT. They used a parameterization of the ratio of clauses to variables. For random 3-SAT, they found numerically that the transition point is around 4.3. Above this point random 3-SAT instances are over constrained and almost surely unsatsifiable and below this point problems are under constrained and satisfiable (with high probability). [Mertens, Mezard and Zecchina](http://arxiv.org/pdf/cs.CC/0309020) use cavity method procedures to estimate the phase transition point to a higher degree of accuracy.

Far away from the critical point, "dumb" algorithms work well for satisfiable instances (walk sat, etc.). From what I understand, deterministic solver run times grow exponentially at or near the phase transition (see [here](http://people.cs.ubc.ca/~hutter/previous-earg/EmpAlgReadingGroup/CoaEtAl03.pdf) for more of a discussion?).

A close cousin of belief propagation, Braunstein, Mezard and Zecchina have introduced [survey propagation](http://arxiv.org/pdf/cs/0212002) that is reported to solve satisfiable 3-SAT instances in millions of variables, even extremely close to the phase transition. Mezard has a lecture [here](http://www.msri.org/web/msri/online-videos/-/video/showVideo/2297) on spin glasses (the theory of which he has used in analysis of random NP-Complete phase transitions) and Maneva has a lecture [here](http://www.msri.org/web/msri/online-videos/-/video/showVideo/1919) on survey propagation.

From the other direction, it still looks like our best solvers take exponential amount of time to prove unsatisfiability. See [here](http://www.math.ias.edu/~avi/PUBLICATIONS/MYPAPERS/B-SW99/bw00journal.pdf), [here](http://www.cs.washington.edu/homes/beame/papers/stockcnf.pdf) and [here](https://nats-www.informatik.uni-hamburg.de/intern/proceedings/2002/ECAI/ecai2000/pdf/p0098.pdf) for proofs/discussion of the exponential nature of some common methods in proving unsatisfiability (Davis-Putnam procedures and resolution methods).

One has to be very careful about claims of 'easiness' or 'hardness' for random NP-Complete problems. Having an NP-Complete problem display a phase transition gives no guarantee as to where the hard problems are or whether there even are any. For example, the Hamiltoniain Cycle problem on Erdos-Renyi random graphs is provably easy even at or near the critical transition point. The Number Partition Problem doesn't seem to have any algorithms that solve it well into the probability 1 or 0 range, let alone near the critical threshold. From what I understand, random 3-SAT problems have algorithms that work well for satisfiable instances nearly at or below the critical threshold (survey propagation, walk sat, etc.) but no efficient algorithms above the critical threshold to prove unsatisfiability. This is just state of the art right now and could of course change in the future.

> **Comments:**
> **username_0**: I wonder if those any of those "random k-SAT" results transfer to real life SAT instances, in other words if ratio of clauses to variables is still a useful indicator of hardness  
> **username_2**: @Yaroslav, from my experience, no.  Many real world problems (even reductions) have (or introduce) so much structure so as to destroy the randomness that many solvers have been optimized for.  It seems like at some point we might be able to account for that structure somehow and be able to focus only on the randomness portion (or the 'essence' of the random problem) but I don't see any general way of doing that nor do I really know of any examples that employ that strategy.  
> **username_3**: @user834: From my experience, I agree with you. Moreover, as far as I know, nobody has ever invented even some sort of randomness measure, i.e. a function $R(F)$ that, given a CNF formula $F$, returns a value $r \in [0,1]$ which is representative of the degree of randomness $F$ has. Of course such measure would be just an approximation according to some reasonable criteria; however, I'm unaware of anything like that: do you know if anyone has dealt with this before?  

---

### Answer by username_4 on 2011-01-18. Score: 6

There are lots of sufficient conditions. In some sense, much of theoretical CS has been devoted to the collection of these conditions - fixed parameter tractability, 2-SAT, random 3-SAT of different densities, etc.

> **Comments:**
> **username_0**: That's true, one could take any problem X that's easy to solve and say that "any formula that corresponds to problem X is easy". I guess I'm looking for sufficient conditions that are more efficient at summarizing the easy region than "all problems known to be in P", more like what the constructive Lovasz Local Lemma does  

---

### Answer by username_5 on 2013-01-30. Score: 3

there is not a lot of widespread recognition of this concept so far in the literature, but the *clause graph* of the SAT problem (the graph with one node per clause, and nodes are connected if clauses share variables), as well as other related graphs of the SAT representation, seems to have many basic clues as to how hard the instance will be on average.

the clause graph can be analyzed via all kinds of graph theoretic algorithms, is an apparently natural measure of "structure" and with strong connections to measuring/estimating hardness, and it appears that research into this structure and its implications is still at the very early stages. it is not inconceivable that transition point research, a/the traditional and well-studied way to approach this question, might eventually be bridged into this clause graph structure (to some degree it already has). in other words the transition point in SAT may be seen to exist "because of" the structure of the clause graph.

here is one excellent reference along these lines, a Phd thesis by Herwig, there are many others.

[1] [Decomposing satisfiability problems
or Using graphs to get a better insight into satisfiability problems](http://www.st.ewi.tudelft.nl/sat/theses/paul.pdf), Herwig 2006 (83pp)

> **Comments:**
> **username_6**: this is the dependency graph when applying the lovasz local lemma and variants to satisfiability. in that sense, the clause graph has been looked at *a lot*. Shearer characterizes the graphs for which the local lemma holds, and Kolipaka and Szegedy have made Schaefer's result constructive. When you don't know much, please don't infer that no one knows!  
> **username_5**: shaefers breakdown into a few tractable classes is mentioned in the answer by Zivny but this clause graph analysis is relatively newer, deeper and more nuanced, and more with an empirical flavor. as for the citations you mention, dont seem to be mentioned often in SAT hardness papers/research... there are multiple/parallel intertwined lines of inquiry...  
> **username_6**: Schaefer was a typo, I meant Shearer. LLL and its variants is *a main tool* in delimiting the hard instances of k-SAT, a google search will reveal tons of references. Shearer's theorem shows which clause graphs guarantee that any SAT instance with that graph is necessarily satisfiable. Look at this survey for detailed connections to hardness thresholds, difficulty of constructing hard instances, algorithms, etc. http://www.disco.ethz.ch/lectures/fs11/seminar/paper/barbara-3.pdf  
> **username_6**: a general thought: each time you say something is terra incognita there is a strong possibility it is terra incognita *to you*. in any case this kind of comment is useless unless you are an established and published expert in the area. it would be better if you restrict your answers to what **you know** and leave out comments about what you think no one knows.  
> **username_5**: [LLL](http://en.wikipedia.org/wiki/Lovász_local_lemma) is _one_ tool for analyzing SAT, invented in 1975 with maybe some refinements since then. its a recipe for _sufficient_ easy or hard instances but not _necessary_. other approaches since then do exist that increasingly fill in the gap in novel ways ie extend and bypass it. you must be confusing this answer with something else, there is no use of the term _"terra incognita"_ in the above question. & suggest _you_ confine yourself to the actual written answers & not speculate about what others know or dont know =)  
> **username_6**: "there is not a lot of widespread recognition of this concept so far in the literature" - not true given the complete characterization of when the clause graph is sufficient for satisfiability. i *am* speaking about this answer. there has been a lot of work on LLL, including Shearer, asymmetric versions, and, crucially, constructive proofs. way more than "maybe some refinements". so i go back to suggesting  you keep your comments/answers to things you know at least a tiny bit about.  
> **username_5**: sasho, instead of devaluing great new work, why dont you try actually reading something of the Phd thesis cited instead of pointing to decades old ideas? (which yes, it can coexist with & does not replace) it is novel, comprehensive, sometimes empirical, and massively expands on prior approaches, ie is _seminal and groundbreaking_, and imho is very likely to be a strong basis for further research. one might call it a _tour de force_ ... your insistent claim that the clause graph & _(many)_ other approaches from the paper are identical to earlier ideas is unfounded and unsupportable at best...  
> **username_6**: all I am saying: **your first sentence is wrong**. there is TONS of theoretical and applied research that looks at the clause graph. for another, this *masters* thesis is far from a tour de force, it's barely more than an empirical study of old algorithmic ideas. tree width decompositions and cut decompositions have appeared in many papers before this thesis, some of them referenced.  
> **username_5**: ok, fine, it might be more accurate to say the clause graph & some of Herwigs other graph-based analytics are maybe not a foremost or prominent method of analyzing hardness esp in the empirically-focused literature. the last sentence is wrong, _masters_ thesis, not Phd thesis, _mea culpa_. however, there seem to be novel/creative approaches in the paper not seen in prior work, and abstract analysis cannot likely uncover all interesting heuristics that are uncovered via empirical approaches... the two approaches intertwine & crosspollinate each other...  

---

### Answer by username_5 on 2013-02-10. Score: 1

this important paper [1] by Toby Walsh is related to the the SAT transition as measured in the clause/variable ratio. however it goes further in measuring a property called *constrainedness*, $\kappa$. its a rough or maybe natural measure of hardness such that overconstrained or underconstrained problems are easier than constrainedness at a critical intermediate point.

it finds an apparent [fractal](http://en.wikipedia.org/wiki/Fractal) [self-similarity](http://en.wikipedia.org/wiki/Self_similarity) structure of hard instances wrt the constrainedess parameter such that as a [DP(LL)](http://en.wikipedia.org/wiki/DPLL_algorithm) solver during search tends to find subproblems with the same critical constrainedness no matter which variable is chosen next to branch on. there is some further analysis of fractal structure in SAT instances (such as [Hausdorff dimension](http://en.wikipedia.org/wiki/Hausdorff_dimension) of SAT formulas & connection to hardness) in eg [2,3]

another somewhat interrelated line of inquiry here is the relationship of [small world](http://en.wikipedia.org/wiki/Small-world_network) graphs to (hard) SAT structure eg [4,5]

of course the standard point in this area applies that a very definitive answer to this question would be inherently close to a [P$\stackrel{?}{=}$NP](http://en.wikipedia.org/wiki/P_versus_NP_problem) proof, or that such a proof would (will?) be the best/near-final answer to the question.

[1] [The constrainedness knife edge](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.3267) by Toby Walsh 1998

[2] [SELF-SIMILARITY OF SATISFIABLE BOOLEAN EXPRESSIONS DECIPHERED IN TERMS OF GRAPH DIRECTED ITERATED FUNCTION SYSTEMS](http://tianjia.wikispaces.com/file/view/kSAT.pdf) by Ni and Wen

[3] [Visualizing the Internal Structure of SAT Instances (Preliminary Report)](http://www.satisfiability.org/SAT04/programme/117.pdf) Sinz

[4] [Search in a small world](http://www.cse.unsw.edu.au/~twalsh/wijcai99.pdf) by Walsh 1999

[5] [Modelling more realistic SAT problems](http://users.cecs.anu.edu.au/~andrews/papers/slater_ai02.pdf) by Slater 2002

> **Comments:**
> **username_7**: It's DPLL, not DP(LL) by the way. Also, there is significantly more recent work on the phase transition in SAT (see the work of Achlioptas, for example).  
> **username_5**: there is a DP algorithm that precedes DPLL that has similar behavior. the other answer by user834 mainly mentioned SAT transition point research with many refs but this answer emphasizes a different (but interrelated) angle  
> **username_7**: I am aware of these algorithms. I was only pointing out the standard typographical convention, which is to write DP, or DPLL, or DPLL(T), or DPLL(Join), for the quantifier-free first order case. No one writes DP(LL) and it adds confusion with DPLL(T) and DPLL(Join)  
> **username_5**: DP(LL) is what was meant as DP+DPLL  

---

### Answer by username_8 on 2011-01-20. Score: 1

It is easy to move all the instances near the "transition" point to as far from the "transition" point as one wishes. The movement involves a polynomial time/space effort.

If instances far from the "transition" point are easier to solve, then those near the transition point must be equally easy to solve. (Polynomial transformations and all.)

> **Comments:**
> **username_5**: can you elaborate, or do you have a ref for this?  

---

