Knuth-Bendix constraint solving is NP-complete
<|reference_start|>Knuth-Bendix constraint solving is NP-complete: 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.<|reference_end|>
@article{korovin2002knuth-bendix,
    title={Knuth-Bendix constraint solving is NP-complete},
    author={Konstantin Korovin and Andrei Voronkov},
    journal={arXiv preprint arXiv:cs/0207068},
    year={2002},
    archivePrefix={arXiv},
    eprint={cs/0207068},
    primaryClass={cs.LO}
}