A non-linear problem can be first treated as a linear one, that is considering two occurrences of a same variable as two different variables. After this step, one has to solve the equations between the different values that have been obtained for the different occurrences of a same variable. We show that one can restrict the search of the solutions of these latter equations to linear substitutions. This result is based on the analysis of how the minimal solutions of a linear Diophantine equation can be built-up using the solutions of the trivial Diophantine equation associated with the linearized AC-equation.
This provides a new AC-unification algorithm which does not make an explicit use of the solving of linear Diophantine equations.