MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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).

share|cite|improve this question

I found a reference which proves that minimum propositional proof length is NP-hard to linearly approximate for a variety of systems from resolution proofs to Frege proofs. Minimal Propositional Proof Length is NP-hard to Linearly Approximate

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.