# Complexity class of conditional dependency resolution

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.

This seems to be solvable in quadratic time using the following algorithm (denote the number of theorems by $$n$$):

Let $$L$$ be an empty list.

While ( size of $$L$$ $$<$$ $$n$$):

• If there's a theorem provable by the theorems in $$L$$ (arbitrarily chose one if there are multiple such theorems), append the theorem to $$L$$.
• Else: return that no such ordering exist.

It's easy to see that if there exists some legal list of proving order, the algorithm will find such list.

Overall, we might need to go over all (remaining) theorems in each iteration, so the runtime is quadratic in the input size.

• The problem is that there is not a single proof for each theorem. This method will work given a specific proof for each theorem, but it must be done for each choice function of proofs over theorems, which will not scale well when each theorem has many proofs with different dependencies. Feb 18 '15 at 9:15
• @HevyLight - Then it should be better worded in the question, please see my edit.
– R B
Feb 18 '15 at 9:24