Tractable constraints in finite semilattices

摘要

We introduce the notion of definite inequality constraints involving monotone functions in a finite meet-semilattice, generalizing the logical notion of Horn-clauses, and we give a linear time algorithm for deciding satisfiability. We characterize the expressiveness of the framework of def- inite constraints and show that the algorithm uniformly solves exactly the set of all meet-closed relational constraint problems, running with small linear time constant factors for any fixed prob- lem. We give an alternative technique for reducing inequalities to satisfiability of Horn-clauses (HORNSAT) and study its efficiency. Finally, we show that the algorithm is complete for a max- imal class of tractable constraints, by proving that any strict extension will lead to NP-hard problems in any meet-semilattice.