On the Complexity of Computing Minimal Unsatisfiable LTL formulas