[comp.theory] question on restrictions of SAT

gottlob@vexpert.dbai.tuwien.ac.at (Georg Gottlob) (01/06/91)

The satisfiability problem (SAT) and many restricted versions of 
it (e.g. monotone SAT, planar SAT etc.) remain NP-complete 
even if |c|<=3 for each clause c in the problem instances.

I am looking for restricted versions of SAT (defined by 
additional syntactic conditions on the problem instances) 
such that:


  1) the restricted version is still NP-complete, and
  
  2) the restricted version is solvable in polynomial time 
     if the cardinality of clauses id bounded by a constant k,
     i.e., |c|<=k for each clause c in the problem instance.

Examples of such classes and/or pointers to relevant references
are welcome.

--------------------------
Georg Gottlob  
gottlob@vexpert.dbai.tuwien.ac.at