In this paper, we show various hardness results for the satisfiability of ground sets of literals in the theory of equality and uninterpreted functions (EUF) with finite cardinality constraints. It is known that this problem is NP-complete in the general case, when a domain has a finite cardinality constraint || ≤ , for any ≥ 3. We notice that this problem stays NP-complete in the case of a single domain of cardinality 2, indicating that even the Boolean sort can be hard to handle when functions are present. It is trivial that the function-free case with Boolean sorts has good complexity, but allowing a single binary function, or (an arbitrary number of) unary functions only, makes the problem NP-complete.
Satisfying a set of ground literals in the theory of equality and uninterpreted functions boils down to extending to a complete set of equalities and disequalities over the terms in (i.e., for each pair of terms , ′in , we have either ≈ ′ ∈ , or ̸≈ ′ ∈ ), such that satisfies the EUF axioms: This is the goal of congruence closure. In extending it for finite cardinality constraints, we must make sure not to break those constraints.
Reflexivity is implicitly assumed and, therefore, automatically satisfied. Symmetry and transitivity are enforced by the use of the union-find data structure, i.e., by working with congruence classes rather than with the equalities directly. Two terms are supposed to be equal if and only if they are in the same congruence class. The equalities in are satisfied by merging the necessary classes: if ≈ ′ ∈ , the classes of and ′ are merged. Finally, the congruence axioms are satisfied by merging the classes of functional terms (1, . . . ) and (′1, . . . ′) whenever their top symbols and arguments match. The result is the minimal set of equalities that satisfies both the EUF axioms and the equalities in . Every possible disequality holds, and therefore is satisfied if and only if none of the disequalities in is violated in the resulting set of congruence classes.
Since this is the minimal set of equalities, congruence classes cannot be split to satisfy cardinality constraints. The only possible move is merging congruence classes until there are no more classes than the requested number of elements in the domain. The dificulty lies in doing this without violating the disequalities in (or showing that this task is impossible).
In the absence of functions, the satisfiability problem for a set of ground equalities and disequalities
is equivalent to graph coloring, as suggested in [
First, notice that it is not important whether we are considering the many-sorted case or the onesorted case, the many-sorted case being simply the juxtaposition of independent one-sorted problems. Indeed, since there are no functions, each literal is of the form ≈ , or ̸≈ , where and are constants. There is no way for elements of diferent sorts to interact, so each sort can be treated independently.
Given a set of equalities and disequalities in a sort with some cardinality constraint stating that the sort is of cardinality at most , a congruence closure-like procedure can be applied to obtain an equivalence relation ≡ over the terms in . In absence of functions, the congruence rule plays no role, but a congruence closure algorithm can still be used to compute this equivalence relation.
Once this equivalence relation is known, it remains to assign one of at most elements to each equivalence class, while making sure not to assign the same element to two classes that have a disequality between them. The classes that are assigned the same element can subsequently be merged. This is exactly the problem of graph -coloring: the vertices are the equivalence classes, the edges are the disequalities between those classes, and the colors are the elements of the domain. Therefore, determining the satisfiability of a set of ground equalities and disequalities in presence of cardinality constraints reduces to graph coloring. Conversely, any graph coloring problem can be trivially encoded as a satisfiability problem in the theory of finite cardinality constraints. Graph coloring is NP-complete for any ≥ 3, and thus, the same applies to the satisfiability of a set of ground equalities and disequalities with finite cardinality constraints. For ≤ 2, however, graph coloring can be solved in linear time, yielding a linear-time procedure for the satisfiability of a set of (dis-)equalities with cardinality constraints only imposing domains of at most two elements.
Incidentally, note that graph coloring can be instrumental to prove the NP-hardness of many
firstorder theories [
We now consider the complexity when the theory of uninterpreted functions is combined with finite cardinality constraints. For cardinality constraints requiring domains to contain at most elements with ≥ 3, the problem is NP-complete, since the hardness is directly inherited from the case without functions above. In the degenerate case = 1, the problem is no harder than standalone EUF. Within the sorts which have a cardinality 1 constraint, all elements must be equal. The problem can thus be solved by applying regular congruence closure, and merging all congruence classes within the cardinalityrestricted sorts. The polynomial complexity of congruence closure is preserved. For ≤ 2, one could hope to still have polynomial-time algorithms, as in the function-free case. The case = 2 would be particularly helpful in integrating Boolean cardinality constraints with EUF reasoning. Unfortunately, we show that functions do actually make the problem significantly harder.
With = 2, the problem is NP-hard: there is a simple polynomial reduction of 3-SAT to the satisfiability of a set of literals in the (quantifier-free) theory of equality with uninterpreted functions, where at least one sort is constrained to a domain with at most two elements.
First, introduce two constants for the sort constrained to at most two elements, and impose that they are diferent, by asserting a disequality between those constants. This results in the sort having at least two congruence classes. Those two congruence classes will represent elements which are true and false respectively, so the constants are named accordingly.
true ̸≈ false The cardinality constraint on the sort imposes that any element in the sort is either equal to true or false. Next, for each proposition in the 3-SAT instance, introduce two constants representing the proposition and its negation. The two constants must be diferent, since they have diferent truth values. For example, with propositions , , , introduce constants , , , ¯, ¯, ¯, and add the constraints: ̸≈ ¯ ̸≈ ¯ ̸≈ ¯
Finally, introduce a function : Bool3 → , where Bool is the sort of cardinality two, and is an arbitrary sort (with cardinality 2, finite cardinality larger than 2, or arbitrary cardinality). For each clause in the 3-SAT instance, e.g. ∨ ∨ ¬, introduce a corresponding constraint of the form: (, , )¯ ̸≈ (false, false, false) Since the top symbol is the same, this constraint imposes that one of the arguments of difers, i.e., that ̸≈ false, ̸≈ false, or ¯ ̸≈ false, which is equivalent to the constraint imposed by the clause.
If a model is found that satisfies all these constraints, it can trivially be translated to a model of the original 3-SAT formula. The converse is also true, meaning that this set of disequalities is satisfiable if and only if the original 3-SAT problem is.
Note that can be the same sort as Bool. An example of a satisfying would be a function that maps a clause to its truth value. This means that the proof holds even if the Boolean sort is the only sort in the problem. Furthermore, if returns Boolean values, a single binary function is enough; clauses can be encoded in the following way:
( (, ), )¯ ̸≈ ( (false, false), false)
The problem is also in NP: it can be solved in polynomial time by non-deterministically partitioning the set of terms of each cardinality-restricted sort into (at most) two classes, then running the usual congruence closure algorithm. This can be done by first selecting two terms to be the representatives of the two classes (or a single representative term for the case where one class is empty), then adding an equality with one of the representatives for each term. This operation takes linear time, and linearly increases the size of the set of literals. Since congruence closure takes polynomial time, the complete runtime is also polynomial.
Even in the case where all functions are unary, the satisfiability problem for a set of EUF literals where at least one sort must be interpreted as a domain of cardinality two remains NP-complete. This is due to the interaction between transitivity and congruence. Disequalities stemming from transitivity alone are easy to find by reasoning about equivalence classes rather than individual (dis-)equalities. For congruence, in the unary case, the rule manifests as a set of binary clauses, each with one positive and one negative literal (e.g., ̸≈ ∨ () ≈ ()). Thus, exhaustively propagating all consequences of the congruence rule is easy. Taken together, however, transitivity and congruence can interact in complex ways and allow encoding arbitrary clauses. Consider the literals: Adding equalities 1 ≈ 2 and 3 ≈ 4 leads to a conflict, but neither equality leads to a conflict on its own. In other words, the disjunction 1 ̸≈ 2 ∨ 3 ̸≈ 4 is a logical consequence of these literals, and neither of its disjuncts is. A ternary disjunction can be built by applying this encoding twice: 1 ̸≈ 2 ∨ 3 ̸≈ 4 ∨ 5 ̸≈ 6 becomes: then, This can be used to encode 3-SAT. Using a similar encoding as in Section 4.1, a clause ∨ ∨ ¬ can be translated into EUF literals using two unary functions: (1) ̸≈ (3) (2) ≈ (4) (1) ̸≈ (3) ∨ 5 ̸≈ 6
(2) ≈ (4) ( (1)) ̸≈ (5) ((3)) ≈ (6) (2) ≈ (4) ( ()) ̸≈ ()¯ (()) ≈ (false) (false) ≈ (false) One can easily verify by case analysis on the truth values of , , and ¯, that this is satisfiable (i.e., there exist appropriate functions and over the 2-element domain) if and only if , , and ¯ are not all equal to false. Additional clauses can be encoded in a similar way, introducing two fresh functions instead of and for each clause. This SAT encoding is polynomial, therefore the satisfiability of sets of EUF literals with unary functions only is NP-hard, if the domain is constrained to two elements.
In general, EUF problems in SMT are expressed in many-sorted logic, and have to be solved for multiple domains at once. Some domains might have cardinality constraints, and some others might not. When there exists a function that takes arguments of multiple diferent sorts, or that returns values of a sort diferent from the argument sort(s), the corresponding domains have to be treated together.
Sections 4.1 and 4.2 suggest that functions are hard to handle in the case of a 2-element domain, but this does not mean that all functions need to be avoided in order to maintain a polynomial complexity. If none of the functions take arguments of a cardinality-restricted sort, the reduction of Section 3 can still be applied. This time, the congruence rule needs to be used, since functions are present, so the first step of the reduction corresponds to regular congruence closure.
After applying congruence closure, notice that merging congruence classes of a cardinality-restricted sort does not require merging any other classes; since no functions take arguments of this sort, the congruence rule cannot apply. This means that merging two congruence classes of this sort will lead to a conflict if and only if there is an explicit disequality in between elements of those classes. Thus, the problem once again reduces to graph 2-coloring: two classes can have the same color (i.e., correspond to the same element) if and only if there is no explicit disequality between them.
The above theoretical bounds have a practical consequence: any procedure for congruence closure with ifnite cardinality constraints, except in very degenerate cases, will require some kind of SAT solver-like reasoning capacity, since the problem is NP-complete. Given a partition of terms in congruence classes, taking into account the cardinality constraints essentially boils down to iteratively merging classes, until the target cardinality upper bounds are met for the sorts with cardinality restrictions. It would therefore be highly valuable to know beforehand, at each point, which pairs of classes not to merge, i.e., ifnding out which disequalities are consequences of the current set of literals. This is not totally trivial: if two congruence classes do not have an explicit disequality between them, merging them can lead to other class merges, leading to a “hidden” conflict. For example, with three Boolean constants , , , and given the disequality () ̸≈ (), where returns values of an arbitrary unconstrained sort, merging the classes of and is not possible. There is no explicit disequality between their classes, but merging them leads to merging the classes of () and (), triggering a conflict.
To avoid this, one solution is to propagate disequalities “backwards” through the congruence rule. Taking the contrapositive of the congruence rule gives () ̸≈ () ⇒ ̸≈ . This allows propagating ̸≈ , this explicit disequality preventing the merge of the classes of and . With binary functions and above, this becomes more complicated since the propagation yields a disjunction of disequalities. For example, we have (1, 2) ̸≈ (1, 2) ⇒ (1 ̸≈ 1 ∨ 2 ̸≈ 2).
Exhaustive disequality propagation is obviously polynomial. Indeed, if there are terms, it sufices to run × ( − 1)/2 times the quasi-linear satisfiability checking procedure on ∪ ( ≈ ′) for any pair , ′ of terms to check whether ̸≈ ′ is a logical consequence of . Exhaustive disequality propagation is therefore upper bounded by 3 log . In practice, however, deducing all implied equalities might be subtle. Considering the literal
(1, . . . ) ̸≈ (1, . . . ), it is clear that the disjunction 1 ̸≈ 1 ∨ . . . ̸≈ holds. The set of constraints might contain equalities ≈ () and ≈ () for each , and therefore ̸≈ would in turn be a consequence of each disjunct. This however requires to consider each ̸≈ successively, before concluding that ̸≈ holds.
For future work, it would be interesting to either prove that the time complexity of disequality propagation has an impractical lower bound, e.g., 2, or to design an eficient algorithm (i.e., with quasi-linear time complexity).
Our objective is to understand how to best tune a practical congruence closure algorithm to accommodate cardinality constraints. It appears that checking the satisfiability of sets of EUF literals with cardinality constraints is NP-hard, even with strong restrictions on the use of functions. A bit surprisingly (the graph 2-coloring problem is linear) this high complexity even occurs for cardinality constraints with two elements. This tells us that a complete algorithm will necessarily embed reasoning capabilities similar to those of a SAT solver. Future work will need to determine whether eficient algorithms can simply embed of-the-shelf SAT solvers, or if they need to be tailored while getting inspiration from state-of-the-art SAT solving techniques.
Heuristics are often crucial for practically solving NP-complete problems. Here, we believe that disequality propagation is worth further investigation.
Acknowledgments The authors are grateful to the anonymous reviewers for their comments. Ellen Dasnois gratefully acknowledges the financial support of the Wallonia-Brussels Federation for her FRIA grant. Research reported in this paper was supported in part by an Amazon Research Award, Fall 2022 CFP. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not reflect the views of Amazon. This work was also partially supported by the Fonds de la Recherche Scientifique - FNRS WEAVE under Grant number T.W028.23. Declaration on Generative AI The authors have not employed any Generative AI tools.