## Séminaire Algorithmique |

Le séminaire a lieu **le mardi à 11 h 45** (sauf modification exceptionnelle), au campus Côte de Nacre, bâtiment Sciences 3, salle S3 351, 3ème étage.

# Résumé du séminaire du Mardi 1 Février 2011

*Helly Property and Satisfiability of Boolean Formulas
Defined on Set Families*

## par Miki Hermann (LIX, Ecole polytechnique)

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

Joint work with Victor Chepoi, Nadia Creignou, et Gernot Salzer.