and N .Creignou M .More

Dept. de Maths, Universite de Caen, 14032 Caen ,France . E-mail: {Malika.More/Nadia.Creignou}@math.unicaen.fr

ABSTRACT The problem SAT of CNF-Satisfiability is the prototype of NP-complete problems. In this problem the question is whether there exists a truth assignment such that each clause contains at least one true literal. Conversely, the problem 1-At-Most-SAT, in which the question is whether there exists a truth assignment so that each clause contains at most one true literal, is polynomial-time decidable. We define an infinite class of problems SAT([Sigma]

1 ,...,[Sigma]p ), parameterized by symmetric polynomial-time decidable languages and generalizing usual satisfiability problems. For instance, the two problems previously considered are, respectively, parameterized by the languages corresponding to the regular expressions 0^{*}1(0+1)^{*}and 0^{*}+0^{*}10^{*}. We prove a dichotomy theorem for these satisfiability problems with symmetric polynomial clauses: SAT([Sigma]1 ,...,[Sigma])is either polynomial or NP complete. We also show a dichotomy result for the corresponding counting problems: #SAT([Sigma]1 ,...,[Sigma]p is either in FP or #P-complete. Besides, we provide a normal form characterization of the symmetric regular languages [Sigma] leading to a polynomial-time decidable problem SAT([Sigma]). This characterization induces an algorithm to decide whether a given problem SAT([Sigma]1 ,...,[Sigma]p ) is polynomial-time decidable, provided that the languages [Sigma]1 ,...,[Sigma]p are symmetric and regular.

Keywords:Computational complexity, , NP-completeness, satisfiability, counting problems, #P-completeness, polynomial time, symmetric languages, regular languages

Pages:

353 -365

Part of the OUP Journal of Logic and Computation WWW service

Click here to register with OUP.

This page is maintained by OUP admin

Part of the OUP Journals World Wide Web service.

Last modification: 22 Jul 1997

Copyright© Oxford University Press, 1997.