Tractable constraints in finite semilattices

We introduce the notion of definite inequality constraints involving monoto ne functions in a finite meet-semilattice, generalizing the logical notion of Horn-clauses, and we give a linear time algorithm for deciding satisfiab ility. We characterize the expressiveness of the framework of definite cons traints 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 problem. We give an alternative technique f or reducing inequalities to satisfiability of Hem-clauses (HORNSAT) and stu dy its efficiency. Finally, we show that the algorithm is complete for a ma ximal class of tractable constraints, by proving that any strict extension will lead to NP-hard problems in any meet-semilattice. (C) 1999 Elsevier Sc ience B.V. All rights reserved.