Are there algorithms to exactly minimize NFAs which are sometimes efficient?

I'm doing some research with NFAs, and I'm wondering there are algorithms which quasi-efficiently minimize them. I realize that this problem is $PSPACE$ hard, so I'm not looking for a polynomial time algorithm.

What I mean by this is an algorithm which may run in exponential time in the worst cases, but which uses some sort of heuristic to speed up the process, albiet not enough to make it exponential.

I'm only using this to try to get a better idea of what the minimal NFAs of certain languages look like. I'm not using it in any production code, so it doesn't need to be blazingly fast.

For example, the Antichains algorithm for NFAs does equivalence testing which is usually fast but sometimes has exponential explosion. I'm looking for something similar, but for minimization.

Note that I'm NOT looking for things like equivalences, etc. which run efficiently but don't produce a minimal NFA.

Bonus points to anyone who find one with an implementation, and quadruple bonus points if it's in Prolog or Python.
If the tool I'm looking for doesn't exist, I'd be happy if anyone gave any old implementation of NFA minimization.

SAT solvers have been pretty good at this. See [1] for more; the method produces a minimal automaton in almost all cases. Following some references, Tsyganov [2] combined the Kameda-Weiner with local search methods.

I don't know if there are readily available implementations out there, but at least [1] describes the reduction to SAT. One can then use any available SAT solver.

[1] Geldenhuys, Jaco, Brink Van Der Merwe, and Lynette Van Zijl. "Reducing nondeterministic finite automata with SAT solvers." Finite-State Methods and Natural Language Processing. Springer Berlin Heidelberg, 2010. 81-92.

[2] Tsyganov, Andrey V. "Local Search Heuristics for NFA State Minimization Problem." International Journal of Communications, Network and System Sciences 5 (2012).

StackExchange Computer Science Q#13206, answer score: 3