On the Complexity of Hmelevskii's Theorem and Satisfiability of Three Unknown Equations

Abstract. We analyze Hmelevskii's theorem, which states that the general solutions of constant-free equations on three unknowns are expressible by a finite collection of formulas of word and numerical parameters. We prove that the size of the finite representation is bounded by an exponential function on the size of the equation. We also prove that the shortest nontrivial solution of the equation, if it exists, is exponential, and that its existence can be solved in nondeterministic polynomial time.

• Type: Journal
• Year: 2009
• Where: DLT
• Authors: Aleksi Saarela
• Keywords: DLT 2009, Exponential Function, Nondeterministic Polynomial Time, Shortest Nontrivial Solution, Theoretical Computer Science