<p>2-SAT is in P.</p>

<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)</p>

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

<p>What other classes of SAT-problems might such a generalization cover?</p>

CC BY-SA 3.0
2013-12-03T22:08:57.110Z
You might want to give this thread a look:
http://cstheory.stackexchange.com/questions/4375/which-sat-problems-are-easy
cody
CC BY-SA 3.0
2013-12-03T22:10:28.030Z
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
CC BY-SA 3.0
2013-12-04T01:32:37.433Z
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
CC BY-SA 3.0
2013-12-04T05:45:27.827Z
In [one precise sense](http://en.wikipedia.org/wiki/P-complete) the answer is [Horn-SAT](http://en.wikipedia.org/wiki/Horn-satisfiability).
Huck Bennett
CC BY-SA 3.0
2013-12-04T06:53:38.273Z
@dspyz - What about [Schaefer's dichotomy theorem](http://en.wikipedia.org/wiki/Schaefer's_dichotomy_theorem) ?
Xavier Labouze
CC BY-SA 3.0
2013-12-04T10:38:38.747Z
@cody  Thanks, that's just what I was looking for
dspyz
CC BY-SA 3.0
2013-12-04T10:40:22.023Z
@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
CC BY-SA 3.0
2013-12-04T10:40:38.743Z
@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
CC BY-SA 3.0
2013-12-04T10:44:45.877Z
@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
CC BY-SA 3.0
2013-12-04T17:02:02.130Z
@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
CC BY-SA 3.0
2013-12-06T22:40:19.427Z
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
CC BY-SA 3.0
2013-12-07T17:35:31.150Z
The Lovász Local Lemma and Moser's algorithm might be of interest.
Martin Schwarz
CC BY-SA 3.0
2013-12-19T23:42:38.470Z
@AndrásSalamon Thanks, I found it: http://eccc.hpi-web.de/report/2013/159/
dspyz
<sat><polynomial-time><resolution>
Most general form of SAT which is in P
dspyz
# Most general form of SAT which is in P

(Asked by: username_0 on 2013-12-03)

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?

**Tags:** sat, polynomial-time, resolution

> **Comments:**
> **username_1**: You might want to give this thread a look: http://cstheory.stackexchange.com/questions/4375/which-sat-problems-are-easy  
> **username_0**: 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.  
> **username_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.  
> **username_3**: In [one precise sense](http://en.wikipedia.org/wiki/P-complete) the answer is [Horn-SAT](http://en.wikipedia.org/wiki/Horn-satisfiability).  
> **username_4**: @username_0 - What about [Schaefer's dichotomy theorem](http://en.wikipedia.org/wiki/Schaefer's_dichotomy_theorem) ?  
> **username_0**: @username_1  Thanks, that's just what I was looking for  
> **username_0**: @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.  
> **username_0**: @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.  
> **username_0**: @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.  
> **username_2**: @username_0, 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.  
> **username_5**: Note also the recent result of Austrin/Guruswami/Håstad that shows that $(2+\epsilon)$-SAT is NP-hard (ECCC TR13-159).  
> **username_6**: The Lovász Local Lemma and Moser's algorithm might be of interest.  
> **username_0**: @AndrásSalamon Thanks, I found it: http://eccc.hpi-web.de/report/2013/159/  

---

## 0 answers

