We take a look at k-DFAOs, which are Deterministic Finite Automata with Output with a special property: each k-DFAO represents a k-automatic sequence a, an infinite sequence in which the i-th element is the output the automata produces for the k-ary representation of i. Given any k-automatic sequence a, we define their complexity ||a||k as the size of the smallest possible k-DFAO representing our sequence and similarly the reverse complexity ||a||Rk for the right to left representation of k-ary numbers.
To be more specific, we look at local changes f to our sequences, that only change a finite amount of elements, and find an upper bound for the complexities ||f(a)||k and ||f(a)||Rk, when applied to an arbitrary sequence a.
We then use SAT/SMT solvers to prove that these upper bounds can not be further improved, thus establishing a lower bound as well.
We also create an algorithm for minimizing any k-DFAO, which will give us a more efficient way of getting ||a||k than using a SAT/SMT solver.