EDIT: ad hoc speed-ups are excluded.
We have the result that propositional resolution requires exponential time. The resolution result uses the proof of the pigeonhole principle as an example of a proof that takes exponential time.
Let's also say we have a hypothetical algorithm M for SAT that runs in polynomial time. EDIT : M is correct, complete, sound, and general-purpose; it contains no ad hoc speed-up rules for the pigeonhole principle or any other theorem that requires exponential length in resolution. M takes its input in clausal form; we'll set up the input like a resolution proof where the consequent is negated to lead to unsatisfiability if the theorem is true. Now let's consider how the proof of the pigeonhole principle works in algorithm M with a strong condition C added:
C. We are given that M simply transforms one clause (or set of clauses) to another clause (or set of clauses). Every such transformation is logically sound.
Some questions; please point out the most fatal flaws:
- Given condition C above, and since M's rule system must be finite, correct, and complete, can we conclude that there is a translation from M's rule system to an equivalent set of expansions based on resolution?
- Are we now in a place where we can conclude that M would produce a computation that could be mapped by the translation in point 1 above into an impossible polynomial-time resolution proof of the pigeonhole principle?