Knuth-Bendix constraint solving is NP-complete
Konstantin Korovin, Andrei Voronkov
TL;DR
This paper proves that solving constraints based on the Knuth-Bendix order in term algebras is NP-complete, highlighting computational complexity challenges in automated reasoning.
Contribution
It establishes the NP-completeness of the existential theory of term algebras with Knuth-Bendix order, providing a polynomial-time algorithm for constraint solving.
Findings
NP-completeness of the existential theory of term algebras with Knuth-Bendix order
Polynomial-time nondeterministic algorithm for solving constraints
Implications for automated reasoning and term rewriting systems
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Constraint Satisfaction and Optimization · Logic, Reasoning, and Knowledge