Lesson 7

The unsatisfiability of the pigeonhole formula can be easily proved in stronger proof systems. For example, the cutting planes (CP) proof system operates with linear inequalities where variables take values from \(\{0,1\}\) and coefficients are integers. There are two inference rules: one can add two inequalities after multiplying them by positive numbers, and one can divide the coefficients of an inequality by their greatest common divisor and round up the free term (if \(2x+2y \ge 3\), then \(x+y \ge \lceil \frac{3}{2} \rceil\)).

A CNF formula can be easily transformed into a system of inequalities. For example, the clause \((\overline{x}\lor y \lor \overline{z})\) can be rewritten as the inequality \((1-x)+y+(1-z) \ge 1\). Then the goal is to derive the inequality \(1 \le 0\).

In the CP proof system the pigeonhole principle is proved easily, but there are other formulas that have no short proofs of unsatisfiability even in the CP system.