Sufficient conditions for tractability Some complexity results prove that some restrictions are polynomial without proving that all other possible restrictions of the same kind are NP-hard. Datalog A sufficient condition for tractability is related to expressibility in Datalog. A Boolean Datalog query gives a truth value to a set of literals over a given alphabet, each literal being an expression of the form ; as a result, a Boolean Datalog query expresses a set of sets of literals, as it can be considered semantically equivalent to the set of all sets of literals that it evaluates to true. On the other hand, a non-uniform problem can be seen as a way for expressing a similar set. For a given non-uniform problem, the set of relations that can be used in constraints is fixed; as a result, one can give unique names to them. An instance of this non-uniform problem can be then written as a set of literals of the form . Among these instances/sets of literals, some are satisfiable and some are not; whether a set of literals is satisfiable depends on the relations, which are specified by the non-uniform problem. In the other way around, a non-uniform problem tells which sets of literals represent satisfiable instances and which ones represent unsatisfiable instances. Once relations are named, a non-uniform problem expresses a set of sets of literals: those associated to satisfiable (or unsatisfiable) instances. A sufficient condition of tractability is that a non-uniform problem is tractable if the set of its unsatisfiable instances can be expressed by a Boolean Datalog query. In other words, if the set of sets of literals that represent unsatisfiable instances of the non-uniform problem is also the set of sets of literals that satisfy a Boolean Datalog query, then the non-uniform problem is tractable. Local consistency Satisfiability can sometimes be established by enforcing a form of local consistency and then checking the existence of an empty domain or constraint relation. This is in general a correct but incomplete unsatisfiability algorithm: a problem may be unsatisfiable even if no empty domain or constraint relation is produced. For some forms of local consistency, this algorithm may also require exponential time. However, for some problems and for some kinds of local consistency, it is correct and polynomial-time. The following conditions exploit the primal graph of the problem, which has a vertex for each variable and an edge