A dichotomy theorem for maximum generalized satisfiability problems

We study the complexity of an infinite class of optimization satisfiability problems. Each problem is represented through a finite set, S, of logical relations (generalizing the notion of clauses of bounded length). We prove the existence of a dichotomic classification for optimization satisfiability problems Max-Sat(S). We exhibit a particular infinite set of logical relations L, such that the following holds: If every relation in S is O-valid (respectively 1-valid) or if even/relation in S belongs to L, then Max-Sat(S) is solvable in polynomial time, otherwise it is MAX SNP-complete. Therefore, Max-Sat(S) either is in P or has some epsilon-approximation algorithm with epsilon < 1 although not a polynomial-time approximation scheme, unless P = NP: L = {Pos(n), Neg(n), Spider (n,p,q), Complete-Bipartite(n,p):n,p,q epsilon N}, where Pos(n)(X(1), ..., X(n)) = (X(1) Lambda ... Lambda X(n)), Neg(n),p,q(X(1),..., X(n)) = (inverted left perpendicular X(1) Lambda ... Lambda inverted left perpendicular X(n)), Spider n,p,q(X(1), ..., X(n), Y-1, ..., Y-p, Z(1) ..., Z(q)) = Lambda(i=1)(n) (X(1) --> Y-1) Lambda Lambda(i=1)(p) (Y-1=Y(i) Lambda Lambda(i=1)(q) (Y-1 --> Z(i)), and Complete-Bipartite(n,p)(X(1), ..., X(n), Y-1, ..., Y-p) = Lambda(i)=1(n) Lambda(j=1)(p) (X(i) --> Y-j). (C) 1995 Academic Press, Inc.