Please note that the pigeonhole-style formulas used in the MBound
paper (AAAI-06) encode what's called the "functional" version of the
pigeonhole problem, where a pigeon goes into at most one hole. This
is, in fact, how most people think of the pigeonhole problem, that a
pigeon is "mapped" to a single hole. In this case, with n pigeons and
k holes, the number of solutions is precisely k!/(k-n)!, as stated in
the paper. In the non-functional version, a pigeon can go into
multiple holes; this is a weaker constraint with many more solutions
and of interest mostly to proof complexity researchers.

The benchmarks file AAAI06-Suite.tgz available for download till Nov
16, 2008 incorrectly included the non-functional version of the two
PHP formulas, php-010-020 and php-015-020. This has been corrected and
the included formulas fphp-010-020 and fphp-015-020 now correctly
reflect the CNF files used in the experiments with MBound.

Apologies for any confusion, and thanks to Carmel Domshlak and
colleagues for bringing this up!

Ashish Sabharwal

Nov 16, 2008

(fixed typo on Dec 2, 2008)