Thanks, I'll have to take your word that this TDD minimization is useful in practice, the way SAT solvers are useful despite SAT being NP-hard. The general problem of Boolean function minimization is of course horrendously intractable; as you say, way harder than SAT.