The max-atom problem and its relevance

Abstract.Let F be a conjunction of atoms of the form max(x; y)+k z, where x; y; z are variables and k is a constant value. Here we consider the satisability problem of such formulas (e.g., over the integers or ra-tionals). This problem, which appears in unexpected forms in many ap-plications, is easily shown to be in NP. However, decades of eorts (in several research communities, see below) have not produced any polyno-mial decision procedure nor an NP-hardness result for this-apparently so simple- problem. Here we develop several ingredients (small-model property and lattice structure of the model class, a polynomially tractable subclass and an inference system) which altogether allow us to prove the existence of small unsatisability certicates, and hence membership in NP intersec-tion co-NP. As a by-product, we also obtain a weakly polynomial decision procedure. We show that the Max-atom problem is PTIME-equivalent to several other well-known-and at rst sight unrelated- problems on hypergraphs and on Discrete Event Systems, problems for which the existence of PTIME algorithms is also open. Since there are few interesting problems in NP intersection co-NP that are not known to be polynomial, the Max-atom problem appears to be relevant