Notes - Logic and Proof MT24, Cutting planes


Flashcards

What is the general idea behind the cutting-plane proof system for CNF formulas?


  • 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$.

@Define the sum rule in the cutting planes proof system.


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}\]

@Define the division rule in the cutting planes proof system, briefly justifying its soundness.


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$.

Can you translate this one-step resolution proof

\[\frac{x_1 \lor x_2 \qquad \lnot x_2 \lor x_3}{x_1 \lor x_3}\]

into a cutting planes proof?


\[\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} }\]

I think that the following is also valid:

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

@Define the triangle trick in the cutting planes proof system and briefly justify its soundness.


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$).

Suppose a CNF formula on $n$ variables has a resolution refutation of length $\ell$.

@Prove that it has a cutting-plane refutation of length $O(\ell n)$.


Consider the following two rules:

  • Weakening: $\frac{C}{C \cup \{L\} }$ (the result is a weaker statement, since either $C$ or $L$ can be true)
  • Restricted resolution: $\frac{C \cup \{L\} \qquad C \cup \{\overline L \} }{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 \{x _ i\}$ is an inequality of the form $f(x _ 1, \ldots, x _ n) + x _ i \ge -c + 1$
    • Then: $C \cup \{\lnot x _ i\}$ 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.

Let $PHP _ n$ be the (unsatisfiable) formula corresponding to the negation of the pigeonhole formula: “there is an injective assignment of $n+1$ pigeons to $n$ holes”. Can you translate this statement into a set of linear inequalities over variables $x _ {i, j}$ where $x _ {i, j}$ stands for “pigeon $i$ is in hole $j$”?


  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).

Let $PHP _ n$ be the (unsatisfiable) formula corresponding to the negation of the pigeonhole formula: “there is an injective assignment of $n+1$ pigeons to $n$ holes”. As a set of linear inequalities over variables $x _ {i, j}$ where $x _ {i, j}$ stands for “pigeon $i$ is in hole $j$”, this reads:

  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$

@Prove that this formula has a cutting-plane refutation of length $O(n^3)$.

(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 \{1, \ldots, n\}$, 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$ 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.



Related posts