Satisfiability is the prototypic NP-complete problem. This paper considers the satisfiability problem for term algebras and shows that this problem is NP-complete. At first glance this result is not surprising, but whereas variables in the usual satisfiability problem have only two possible values, in the term algebra problem, variables have a potential infinity of values. The clever work in this paper shows that there are blocking structures such that any large enough value must include one of these structures. This leads to a representation of the formula as a directed acyclic graph (DAG) and an argument that blocking structures have sizes bounded by a polynomial in the size of this DAG. From this argument a nondeterministic polynomial time algorithm is constructed; hence, the satisfiability problem for term algebras is shown to be in NP. The problem is shown to be NP-complete by showing that the usual three-satisfiability problem is a special case.

This paper also shows that more general problems about term algebras are undecidable. These undecidable problems allow the use of existential quantifiers followed by bounded universal quantifiers. Undecidability is shown by reduction from Post’s correspondence problem.