[Back]

V. Chepoi, N. Creignou, M. Hermann, G. Salzer:
"The Helly Property and Satisfiability of Boolean Formulas Defined on Set Families";
European Journal of Combinatorics, 31 (2010), 2; 502 - 516.

In this paper, we study the problem of satisfiability of Boolean formulas phi in conjunctive normal form (CNF) whose literals have the form "v is element of S" and express the membership of values to sets S of a given set family F defined on a finite domain D. We establish the following dichotomy result. We show that checking the satisfiability of such formulas (called F-formulas) with three or more literals per clause is NP-complete except the trivial case when the intersection of all sets in F is nonempty. On the other hand, the satisfiability of F-formulas phi containing at most two literals per clause is decidable in polynomial time if F satisfies the Helly property, and is NP-complete otherwise (in the first case, we present an O(|phi| F |D|)-time algorithm for deciding if phi is satisfiable). Deciding whether a given set family F satisfies the Helly property can be done in polynomial time. We also overview several well-known examples of Helly families and discuss the consequences of our result to such set families and its relationship with the previous work on the satisfiability of signed formulas in multiple-valued logic.

satisfiability, conjunctive normal form, membership, finite domain, dichotomy theorem, Helly property, Helly family, many-valued logics

http://dx.doi.org/10.1016/j.ejc.2009.03.022