Satisfiability for quadratic word equations with linear side proven NP-complete
Quadratic Word Equations with a Linear Side: Polynomial Nielsen Graph Diameter and NP-Completeness
Formal Languages and Automata TheoryComputational Complexity
Summary
The problem studied is whether a word equation can be solved by replacing variables with words to make both sides equal. The authors focused on a special type called quadratic word equations with a linear side, where variables appear only once on one side of the equation. They proved that checking if such equations can be satisfied is a problem that is both hard and belongs to a known complexity class called NP-complete. This settles a question that was previously open for this class of equations.
What this means in practice
- •For automated theorem provers: Determine the computational difficulty of solving word equations with specific variable constraints to better optimize solver design and heuristics.
- •For formal verification engineers: Use the NP-completeness result for these word equations to guide expectations about complexity when verifying string constraints in software correctness.
A theory result. No direct application yet.
Authors
Yuki Yonemoto
Abstract
The satisfiability problem for word equations asks whether variables can be replaced by words so that the two sides become equal. For regular word equations, in which each variable occurs at most once on each side, satisfiability is NP-complete. For general quadratic word equations, in which each variable occurs at most twice in total, satisfiability is NP-hard, but its membership in NP remains open. We consider an intermediate class: quadratic word equations with a linear side, where each variable occurs at most once on one designated side. We show that the Nielsen graph of an equation $U=V$ in this class, with total length $N=|U|+|V|$, has diameter $O(N^{12})$, measured over reachable pairs of vertices. Together with the known NP-hardness for regular word equations, this result establishes NP-completeness of satisfiability for this class.