Knuth-Bendix constraint solving is NP-complete

2002/07/17 by Konstantin Korovin, Korovin, Konstantin, Андрей Воронков +2 · 2 citations
Computer Science · #Constraint Satisfaction and Optimization #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO

paper · pdf · doi:10.48550/arxiv.cs/0207068

27 pages

arxiv created 2002/07/17 · openalex publication_date 2002/07/17 · arxiv updated 2009/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Cited by

• Term Ordering Diagrams
• Partial Redundancy in Saturation

Related

• Satisfying KBO Constraints
• On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories
• Undecidability in First-Order Theories of Term Algebras Extended with a\n Substitution Operator
• A syntactic tool for proving hardness in the Second Level of the Polynomial-Time Hierarchy
• Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations