29
$\begingroup$

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 of LLL, any other results along those lines?

There's sizable literature on easy regions for Belief Propagation, is there something along those lines for satisfiability?

Improve this question
$\endgroup$
2
  • 2
    $\begingroup$ are you also interested in the random SAT phase transition ? $\endgroup$
    – Suresh Venkat
    Jan 18, 2011 at 4:13
  • $\begingroup$ 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 $\endgroup$
    – Yaroslav Bulatov
    Jan 18, 2011 at 5:26

6 Answers 6

Reset to default
35
$\begingroup$

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

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

Improve this answer
$\endgroup$
3
  • 3
    $\begingroup$ 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 $\endgroup$
    – Vinicius dos Santos
    Jan 20, 2011 at 22:10
  • 1
    $\begingroup$ Thank you, here is the doi: dx.doi.org/10.1016/j.jcss.2008.11.001 $\endgroup$
    – Standa Zivny
    Jan 21, 2011 at 12:01
  • $\begingroup$ 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). $\endgroup$
    – Mahdi Cheraghchi
    Feb 2, 2013 at 2:38
15
$\begingroup$

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 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 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 for more of a discussion?).

A close cousin of belief propagation, Braunstein, Mezard and Zecchina have introduced survey propagation 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 on spin glasses (the theory of which he has used in analysis of random NP-Complete phase transitions) and Maneva has a lecture here on survey propagation.

From the other direction, it still looks like our best solvers take exponential amount of time to prove unsatisfiability. See here, here and here 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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ 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 $\endgroup$
    – Yaroslav Bulatov
    Jan 19, 2011 at 21:17
  • 3
    $\begingroup$ @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. $\endgroup$
    – user834
    Jan 19, 2011 at 21:22
  • $\begingroup$ @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? $\endgroup$
    – Giorgio Camerani
    Jan 20, 2011 at 13:09
6
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ 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 $\endgroup$
    – Yaroslav Bulatov
    Jan 18, 2011 at 7:44
3
$\begingroup$

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, Herwig 2006 (83pp)

Improve this answer
$\endgroup$
9
  • $\begingroup$ 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! $\endgroup$
    – Sasho Nikolov
    Feb 12, 2013 at 17:57
  • $\begingroup$ 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... $\endgroup$
    – vzn
    Feb 12, 2013 at 19:15
  • $\begingroup$ 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. disco.ethz.ch/lectures/fs11/seminar/paper/barbara-3.pdf $\endgroup$
    – Sasho Nikolov
    Feb 13, 2013 at 0:37
  • 1
    $\begingroup$ 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. $\endgroup$
    – Sasho Nikolov
    Feb 13, 2013 at 0:41
  • 1
    $\begingroup$ LLL 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 =) $\endgroup$
    – vzn
    Feb 13, 2013 at 3:46
1
$\begingroup$

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

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ can you elaborate, or do you have a ref for this? $\endgroup$
    – vzn
    Feb 10, 2013 at 16:04
1
$\begingroup$

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 self-similarity structure of hard instances wrt the constrainedess parameter such that as a DP(LL) 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 of SAT formulas & connection to hardness) in eg [2,3]

another somewhat interrelated line of inquiry here is the relationship of small world 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 proof, or that such a proof would (will?) be the best/near-final answer to the question.

[1] The constrainedness knife edge by Toby Walsh 1998

[2] SELF-SIMILARITY OF SATISFIABLE BOOLEAN EXPRESSIONS DECIPHERED IN TERMS OF GRAPH DIRECTED ITERATED FUNCTION SYSTEMS by Ni and Wen

[3] Visualizing the Internal Structure of SAT Instances (Preliminary Report) Sinz

[4] Search in a small world by Walsh 1999

[5] Modelling more realistic SAT problems by Slater 2002

Improve this answer
$\endgroup$
4
  • 3
    $\begingroup$ 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). $\endgroup$
    – Vijay D
    Feb 10, 2013 at 17:38
  • $\begingroup$ 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 $\endgroup$
    – vzn
    Feb 10, 2013 at 18:16
  • 1
    $\begingroup$ 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) $\endgroup$
    – Vijay D
    Feb 11, 2013 at 0:31
  • $\begingroup$ DP(LL) is what was meant as DP+DPLL $\endgroup$
    – vzn
    Feb 11, 2013 at 16:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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