[comp.theory] wanted : tractable satisfiability

rachel@lanai.cs.ucla.edu (Rachel Ben-Eliyahu) (09/12/90)

It is known that to decide whether a set of sentences in propositional
logic is satisfiable is NP-complete. However, there are 
polynomial time algorithms for deciding the satisfiability of a set
of horn clauses and a set of clauses which do not contain
more then 2 literals.

Does anyone know of other subsets of propositional logic that
their satisfiability can be decided in polynomial time ??
References will be appreciated.

Thank You

Rachel.

gillies@m.cs.uiuc.edu (09/12/90)

Here is a paper with an exact characterization of the types of boolean
clauses that can be satisfied in polynomial time, and the types of
boolean clauses that are NP-complete to satisfy:

10th ACM STOC (Symposium on Theory of Computing)
Thomas J. Schaefer*
"The complexity of satisfiability problems"
pp 216-226

This paper is a bear to read (unless you're a logician, which I'm
not).  But I did get through it once, for a term project 8-)