I have a problem I am (considering) writing an algorithm for, but which I suspect to be NP-hard. However, I have not been able to prove that it is in fact NP-hard. The problem is stated as so:
Given a set of theorems, and a set of proofs for each of these theorems which may themselves depend on other theorems, find a list of proofs such that each proof only uses theorems which have proofs that precede it in the list.
The fact that these are theorems and proofs is immaterial as far as this problem is concerned; proofs can be considered to be mere sets of required theorems.