Knuth--bendix constraint solving is NP-complete
Konstantin Korovin, Андрей Воронков · ACM Transactions on Computational Logic · 2005
We show the NP-completeness of the existential theory of term algebras with the Knuth--Bendix order by giving a nondeterministic polynomial-time algorithm for solving Knuth--Bendix ordering constraints.