Abstract :
[en] 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 D has a finite cardinality constraint |D| ≤ n, for any n ≥ 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.
Funding text :
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.
Scopus citations®
without self-citations
0
