The Helly property and satisfiability of Boolean formulas defined on set families

In this paper, we study the problem of satisfiability of Boolean formulas φφ in conjunctive normal form (CNF) whose literals have the form v∈Sv∈S and express the membership of values to sets SS of a given set family SS defined on a finite domain DD. We establish the following dichotomy result. We show that checking the satisfiability of such formulas (called SS-formulas  ) with three or more literals per clause is NP-complete except the trivial case when the intersection of all sets in SS is nonempty. On the other hand, the satisfiability of SS-formulas φφ containing at most two literals per clause is decidable in polynomial time if SS satisfies the Helly property, and is NP-complete otherwise (in the first case, we present an O(|φ|⋅|S|⋅|D|)O(|φ|⋅|S|⋅|D|)-time algorithm for deciding if φφ is satisfiable). Deciding whether a given set family SS 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.