Logic and Proof MT24, Cutting planes

• Convert CNF formulas into a series of integer inequalities
• Apply rules about inequalities
• Derive a contradiction of the form $0 \ge c$ where $0 < c$.

Suppose:

• $f(x) = \sum^n _ {i = 1} a _ i x _ i$
• $g(x) = \sum^n _ {i = 1} b _ i x _ i$
• $c, d, \lambda, \mu \in \mathbb Z$ with $\lambda, \mu \ge 0$

Then:

\[\frac{f(x) \ge c \qquad g(x) \ge d}{\lambda f(x) + \mu g(x) \ge \lambda c + \mu d}\]

Suppose:

• $f(x) = \sum^n _ {i = 1} a _ i x _ i$
• $c \in \mathbb Z$
• $\lambda \in \mathbb Z$ such that $\lambda > 0$ divides every $a _ i$

Then:

\[\frac{f(x) \ge c}{\frac 1 \lambda f(x) \ge \lceil \frac c \lambda \rceil}\]

It would obviously be correct without the $\lceil \cdot \rceil$. But since the left hand side is an integer by assumption, and so $\lceil \frac 1 \lambda f(x) \rceil \ge \lceil \frac c \lambda \rceil \implies \frac 1 \lambda f(x) \ge \lceil \frac c \lambda \rceil$.

\[\frac{\frac{x_1 + x_2 \ge 1 \qquad x_3 \ge 0}{x_1 + x_2 + x_3 \ge 1} \qquad \frac{x_1 \ge 0 \qquad -x_2 + x_3 \ge 0}{x_1 - x_2 + x_3 \ge 0} }{\frac{2x_1 + 2x_3 \ge 1}{x_1 + x_3 \ge 1} }\]

Suppose:

• $I _ 1, I _ 2, I _ 3$ are three disjoint sets of indices
• $\sum _ {i \in I _ 1 \cup I _ 2} x _ i \le 1$
• $\sum _ {i \in I _ 1 \cup I _ 3} x _ i \le 1$
• $\sum _ {i \in I _ 2 \cup I _ 3} x _ i \le 1$

We can derive the inequality:

\[\sum_{i \in I_1 \cup I_2 \cup I_3} x_i \le 1\]

in three steps by adding the inequalities, dividing by two (since each is double counted), and rounding down ($3/2 \to 1$).

Consider the following two rules:

• Weakening: $\frac{C}{C \cup \lbrace L\rbrace }$ (the result is a weaker statement, since either $C$ or $L$ can be true)
• Restricted resolution: $\frac{C \cup \lbrace L\rbrace \qquad C \cup \lbrace \overline L \rbrace }{C}$ (different from normal resolution since $C$ is the same on both sides).

One resolution step can be simulated by at most $2n+1$ steps of these two rules above, by first weakening the clauses being resolved around and then performing one step of restricted resolution.

Both of these rules themselves can be performed by cutting-planes:

• Weakening: Since $x _ i \ge 0$ and $1 - x _ i \ge 0$ are axioms, weakening follows by the sum rule (just add the extra variable).
• Restricted resolution:
  • $C$ is a linear inequality of the form $f(x _ 1, \ldots, x _ n) \ge -c$ where $c$ is the number of variables occurring negatively but not positively in $C$.
  • Then: $C \cup \lbrace x _ i\rbrace$ is an inequality of the form $f(x _ 1, \ldots, x _ n) + x _ i \ge -c + 1$
  • Then: $C \cup \lbrace \lnot x _ i\rbrace$ is an inequality of the form $f(x _ 1, \ldots, x _ n) - x _ i \ge -c$
  • Summing these up yields $2f \ge 1-2c$, and then dividing by 2 and rounding up gives $f \ge 1 - c$.

Therefore the cutting planes refutation has at most $O(\ell n)$ steps.

1. Every pigeon is in some hole: $\sum^n _ {k = 1} x _ {i, j} \ge 1$ for all $1 \le i \le n+1$
2. Each hole has at most one pigeon: $x _ {i, j} + x _ {k, j} \le 1$ for $1 \le i < k \le n+1$, $1 \le j \le n$
3. Variables are $0-1$ valued: $x _ {i, j} \ge 0$, $x _ {i, j} \le 1$ for all $1 \le i \le n + 1, 1 \le j \le n$

(note that this is a linear program, not an integer one. But if the linear program is unsatisfiable, then for sure the corresponding integer one is also).

• For each $j$, derive the following: for every $m \in \lbrace 1, \ldots, n+1\rbrace$, we have $x _ {1, j} + \cdots + x _ {m, j} \le 1$. This can be shown by induction on $m$:
  • Base case: $x _ {1, j} \le 1$ is an axiom for every $j$
  • Inductive step: Suppose we have derived $x _ {1, j} + \cdots + x _ {m, j} \le 1$. We can derive $x _ {1, j} + \cdots + x _ {m+1,j} \le 1$ as follows:
  • Using the sum rule, add $x _ {1, j} + \cdots + x _ {m, j} \le 1$ to itself $m-1$ times to obtain $(m-1)x _ {1, j} + \cdots + (m-1)x _ {m, j} \le m - 1$.
  • (this increases proof length by $m-1$)
  • To this, add $x _ {i, j} + x _ {m+1, j} \le 1$ for each $i = 1, \ldots, m$ (this comes from 2). This obtains $m x _ {1, j} + \cdots + mx _ {m+1, j} \le 2m - 1$.
  • (this increases proof length by $m$)
  • Apply the division rule with $m$ to obtain $x _ {1, j} + \cdots + x _ {m+1, j} \le \lfloor (2m-1)/m \rfloor = 1$.
  • (this increases proof length by $1$, note also that $\lfloor \cdot \rfloor$ is being used here rather than $\lceil \cdot \rceil$, this is okay since the inequality is the other way around and so we would obtain the true cutting planes proof by negating everything)
• (Each proof for each $j$ adds $O(n^2)$ to the length, and this is done $n$ times, so overall increasing the length by $O(n^3)$)
• Taking $m = n+1$ and then summing over every $j$ gives $\sum^{n+1} _ {i=1} \sum^n _ {j = 1}x _ {i, j} \le n$. (increases the length by $n+1$, and if done by divide and conquer, increases the rank by $O(\log n)$)
• On the other hand, summing the inequalities in (1) given $\sum^{n+1} _ {i = 1} \sum^{n} _ {j = 1} x _ {i, j} \ge n + 1$. (increases the length by $n+1$, and if done by divide and conquer, increases the rank by $O(\log n)$)
• A final sum gives $-1 \ge 0$, a contradiction.

Suppose that as input we have a CNF formula $F(x, z) \land G(y, z)$ over common variables $z$ with a corresponding refutation $\lbrace f _ i(x) + g _ i(y) + h _ i(z) \ge c _ i\rbrace _ {i=1}^\ell$. We aim to output a proof $\lbrace f _ i(x) \ge d _ i \rbrace^\ell _ {i=1}$ from $F(x, \alpha)$ and a proof $\lbrace g _ i(y) \ge e _ i \rbrace^\ell _ {i=1}$ from $G(y, \alpha)$ such that at least one of the two proofs ends in a contradiction. If the first proof ends in a contradiction, we output $I(\alpha)$ equals $0$, and otherwise we output that $I(\alpha)$ equals $1$.

Split each inequality $f _ i(x) + g _ i(y) + h _ i(z) \ge c _ i$ into an “$x$-part” $f _ i(x) \ge d _ i$ and a “$y$-part” $g _ i(y) \ge e _ i$ while maintaining the invariant

\[d_i + e_i \ge c_i - h_i(\alpha)\]

which ensures that

\[\lbrace f_i(x) \ge d_i, g_y(y) \ge e_i \rbrace \models f_i(x) + g_i(y) + h_i(\alpha) \ge c_i\]

The construction, which is solely determined by the choice of constants $d _ i$ and $e _ i$, is by induction on $i$:

Case $f _ i(x) + h _ i(z) \ge c _ i$ hypothesis of $F$: Then the $x$-part is $f _ i(x) \le c _ i - h _ i(\alpha)$ and the $y$-part is $0 \ge 0$, i.e. $d _ i := c _ i - h _ i(\alpha)$ and $e _ i = 0$, so the invariant is maintained.

Case $g _ i(y) + h _ i(z) \ge d _ i$ hypothesis of $G$: Then the $x$-part is $0 \ge 0$, and the $y$-part is $g _ i(y) \ge d _ i - h _ i(\alpha)$, i.e. $d _ i := 0$ and $e _ i = c _ i - h _ i(\alpha)$, so the invariant is maintained.

Case $f _ i(x) + g _ i(y) + h _ i(z) \ge c _ i$ obtained from sum rule of $f _ j(x) + g _ j(y) + h _ j(z) \ge c _ j$ and $f _ k(x) + g _ k(y) + h _ z(z) \ge c _ k$ for some $j, k < i$ by an application of the sum rule with coefficients $\lambda, \mu \ge 0$: Then take the $x$-part to be what is obtained by applying the sum rule to the respective $x$-parts of the two summands, and take the $y$-parts similarly. Then $d _ i := \lambda d _ j + \mu d _ k$ and $e _ i = \lambda d _ j + \mu d _ k$. The invariant is maintained.

Case $f _ i(x) + g _ i(y) + h _ i(z) \ge c _ i$ follows from $f _ j(x) + g _ j(y) + h _ j(z) \ge c _ j$ by dividing by $\lambda > 0$ and rounding up. Take the $x$-part and $y$-part to be the result of applying the same division rule to the $x$-part $f _ j(x) \ge d _ j$ and $y$-part $g _ j(y) \ge d _ j$. Thus

\[\begin{aligned} d_i + e_i &= \lceil d_j / \lambda \rceil + \lceil e_j / \lambda \rceil &&(\text{def. of } d_i \text{ and } e_i) \\\\ &\ge \lceil (d_j + e_j) / \lambda \rceil &&(\text{since }\lceil x \rceil + \lceil y \rceil \ge \lceil x + y\rceil \text{ for all }x, y) \\\\ &\ge \lceil (c_j - h_j(\alpha))/\lambda \rceil &&(\text{inductive hypothesis}) \\\\ &= \lceil c_j / \lambda \rceil - h_i(\alpha) &&(\text{since }\lambda h_i(\alpha) = h_j(\alpha)) \\\\ &= c_i - h_i(\lambda) &&(\text{definition of }c_i) \end{aligned}\]

Since the input proof ends in a contradiction, this implies that at least one of the $x$-part or the $y$-part ends in a contradiction, as required.