9
$\begingroup$

It is well known that the pigeonhole principle $PHP_n^{n+1}$ is hard for general resolution. The original proof due to Haken is elegant. One first defines a complexity measure for derived clauses, in which axioms have low complexity, and the final empty clause has high complexity. Then one shows that clauses of medium complexity must have many literals. Finally, one shows that if $\Pi$ is a refutation of small size, then one can restrict the values of some variables in such a way that the resulting formula $PHP_{n-k}^{n-k+1}$ has a corresponding refutation $\Pi'$ of width smaller than what it should be. Contradiction.

Regular resolution is the special case of resolution where variables are not allowed to be resolved more than once in any path from an axiom to the final empty clause. It is well known that regular resolution refutations are essentially read-once branching programs.

Is there a well known way of proving that $PHP_n^{n+1}$ is hard for regular resolution directly, without using Haken's arguments? I would imagine that since regular resolution proofs correspond to read-once branching programs, one could actually use a more direct approach based on rectangle covers and so on. Is this intuition right? Are there any discussions of this technique in the literature?

Ps: I'm aware of a paper due to Pitassi and Raz, which shows that the weak pigeonhole principle is hard for regular resolution. But now this proof is probably much more complicated than a proof for the original $PHP_n^{n+1}$ tautologies due to the weak modification.

$\endgroup$
  • $\begingroup$ I haven't read such a paper, but I think that such a proof outline can likely work out. I wrote a paper with Paul Beame and Russell Impagliazzo in 2012 about Time Space tradeoffs in Tseitin tautologies. Your question isn't about tradeoffs, but one technique we gave does give a sharp lower bound (for regular resolution) for Tseitin taulogies, showing that at least $2^{(w-1)}$ medium complexity clauses are required for Tseitin tautologies on a grid of width w, matching the ~ $2^w$ upper bound pretty closely. For your question I would consider adapting the "probabilistic adversary" approach $\endgroup$ – Chris Beck Oct 21 '18 at 17:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.