Hi guys,

e_lehman@... a écrit :
> > also have you heard of the "spine" or "backbone" in SAT
>

I may not have understood everything about this notion,
but in two words, the backbone of a formula is the
set of literals implied by the formula.

Some people are studying problems called 2+p-SAT,
p being the probability to generate a clause of size
3, 1-p the probability to generate a clause of
size 2. This idea is to study the transition from
2-SAT in P to 3-SAT in NP.

The notion of backbone has been introduced to
in this framework and has been used later to explain
the behavior of local search algorithms
on random 3-SAT instances.

Some instances with fixed backbone can be found
at SATLIB. They are trivial for complete algorithms
but difficult for local search.

http://www.satlib.org/benchm.html

For more information, see for instance:

http://www.satlive.org/satnews.jsp#_131
http://www.satlive.org/satnews.jsp#_132
http://www.satlive.org/satnews.jsp#_133

Daniel