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?

  • 6
    $\begingroup$ You might want to give this thread a look: cstheory.stackexchange.com/questions/4375/… $\endgroup$
    – cody
    Dec 3 '13 at 22:08
  • 3
    $\begingroup$ 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. $\endgroup$
    – dspyz
    Dec 3 '13 at 22:10
  • 2
    $\begingroup$ 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. $\endgroup$
    – Vijay D
    Dec 4 '13 at 1:32
  • 4
    $\begingroup$ In one precise sense the answer is Horn-SAT. $\endgroup$ Dec 4 '13 at 5:45
  • 3
    $\begingroup$ @dspyz - What about Schaefer's dichotomy theorem ? $\endgroup$ Dec 4 '13 at 6:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.