Complexity of Clausal Constraints Over Chains

We investigate the complexity of the satisfiability problem of constraints over finite totally ordered domains. In our context, a clausal constraint is a disjunction of inequalities of the form x d and x d. We classify the complexity of constraints based on clausal patterns. A abstracts away from variables and contains only information about the domain elements and the type of inequalities occurring in a constraint. Every finite set of patterns gives rise to a (clausal) constraint satisfaction problem in which all constraints in instances must have an allowed pattern. We prove that every such problem is either polynomially decidable or NPcomplete, and give a polynomial-time algorithm for recognizing the tractable cases. Some of these tractable cases are new and have not been previously identified in the literature.

• Type: Journal
• Year: 2008
• Where: MST
• Authors: Nadia Creignou, Miki Hermann, Andrei A. Krokhin, Gernot Salzer
• Keywords: Clausal Constraint, MST 2008, Satisfiability Problem, Totally Ordered