2

2-SAT is in P.

Additionally, a (CNF) SAT-problem is trivially poly-time solvable if no two expressions can be resolved (via Robinson resolution, ie for every pair of disjunctive clauses, they either share no opposite literals or else two or more opposite literals)

I was wondering if there's a nice common generalization of these two classes of poly-time solvable SAT instance-types which is also poly-time solvable.

What other classes of SAT-problems might such a generalization cover?

dspyz
  • 916
  • 4
  • 13
  • 6
    You might want to give this thread a look: http://cstheory.stackexchange.com/questions/4375/which-sat-problems-are-easy – cody Dec 03 '13 at 22:08
  • 3
    I'm asking this because I'm working on an algorithm for pre-processing SAT instances. In some smaller cases my algorithm successfully reduces the instance to 2-SAT in which case I can claim my program "solved" the problem. But in the simplest possible 3-SAT program with only one clause: (A V B V C), that doesn't happen. So I want to know exactly when I can make the claim that the problem is "solved" by my pre-processing step. – dspyz Dec 03 '13 at 22:10
  • 2
    Have you looked at other questions on this site about SAT? I think you should look and clarify in your question if what you want to know has not already been answered. – Vijay D Dec 04 '13 at 01:32
  • 4
    In one precise sense the answer is Horn-SAT. – Huck Bennett Dec 04 '13 at 05:45
  • 3
    @dspyz - What about Schaefer's dichotomy theorem ? – Xavier Labouze Dec 04 '13 at 06:53
  • @cody Thanks, that's just what I was looking for – dspyz Dec 04 '13 at 10:38
  • @VijayD that's not very helpful. If you think this question is a duplicate, please refer to the question you think it's a duplicate of. – dspyz Dec 04 '13 at 10:40
  • 1
    @HuckBennett Horn-SAT doesn't seem to cover either of the two cases I mentioned (since both my examples are literal-sign agnostic whereas HORNSAT is not), but that is absolutely another standard class of Poly-time solvable SAT instances I should have thought to include. – dspyz Dec 04 '13 at 10:40
  • 2
    @XavierLabouze The question Cody referred to also had an answer regarding Schaefer's dichotomy theorem. But unless I'm missing something, that doesn't seem to cover the no-resolution case. – dspyz Dec 04 '13 at 10:44
  • @dspyz, I wasn't saying it was a duplicate. I was saying that it would be good to clarify more precisely -- for us readers -- in the text of your question, why your question is not answered by replies to other questions about tractable cases of SAT. As you can see, a lot of readers assumed HornSAT, Schaefer's theorem and related ideas answer your question. – Vijay D Dec 04 '13 at 17:02
  • 1
    Note also the recent result of Austrin/Guruswami/Håstad that shows that $(2+\epsilon)$-SAT is NP-hard (ECCC TR13-159). – András Salamon Dec 06 '13 at 22:40
  • 1
    The Lovász Local Lemma and Moser's algorithm might be of interest. – Martin Schwarz Dec 07 '13 at 17:35
  • @AndrásSalamon Thanks, I found it: http://eccc.hpi-web.de/report/2013/159/ – dspyz Dec 19 '13 at 23:42

0 Answers0