On the complexity of computing minimal unsatisfiable LTL formulas