We present a minimization algorithm for finite state automata that finds and merges bisimulation-equivalent states, identified through partition aggregation. We show the algorithm to be correct and run in time O(n(2)d(2) vertical bar Sigma vertical bar), where n is the number of states of the input automaton M, d is the maximal outdegree in the transition graph for any combination of state and input symbol, and vertical bar Sigma vertical bar is the size of the input alphabet. The algorithm is slower than those based on partition refinement, but has the advantage that intermediate solutions are also language equivalent to M. As a result, the algorithm can be interrupted or put on hold as needed, and the derived automaton is still useful. Furthermore, the algorithm essentially searches for the maximal model of a characteristic formula for M, so many of the optimisation techniques used to gain efficiency in SAT solvers are likely to apply.