When trying to prove that a particular instance of a problem like graph coloring or SAT is unsatisfiable, generally one explores the search tree using an algorithm like DPLL and the proof of unsatisfiability consists of the exhaustive exploration of the search tree - i.e. try an partial assignment of values to variables, do propagation and if the domain of a variable becomes empty, you know the assignment does not satisfy the instance so you backtrack. By propagation I mean, one looks at every constraint and then for every variable in the constraint, one prunes the values in the domain of the variable which are not part of any model satisfying that particular constraint.
My question is that how hard in terms of computational complexity is to find a search tree proving infeasibility of minimal size, i.e. if the size of the search tree is $S$, then how hard is it to find the minimal such search tree given that the size of the input is taken as $S$ (Note - that can be much larger than the size of the original problem, exponential in the worst case).
