# Sub-Exponential Lower Bounds for Branch-and-Bound with General Disjunctions
via Interpolation

Max Gläser  Marc E. Pfetsch

###### Abstract

This paper investigates linear programming based branch-and-bound using
general disjunctions, also known as stabbing planes, for solving integer
programs. We derive the first sub-exponential lower bound (in the encoding
length $L$ of the integer program) for the size of a general branch-and-bound
tree for a particular class of (compact) integer programs, namely
$\smash{2^{\Omega(L^{1/12-\epsilon})}}$ for every $\epsilon>0$. This is
achieved by showing that general branch-and-bound admits quasi-feasible
monotone real interpolation, which allows us to utilize sub-exponential lower-
bounds for monotone real circuits separating the so-called clique-coloring
pair. One important ingredient of the proof is that for every general branch-
and-bound tree proving integer-freeness of a product $P\times Q$ of two
polytopes $P$ and $Q$, there exists a closely related branch-and-bound tree
for showing integer-freeness of $P$ or one showing integer-freeness of $Q$.
Moreover, we prove that monotone real circuits can perform binary search
efficiently.

##  1 Introduction

In recent years, there has been renewed interest in the proof system
associated to branch-and-bound using general disjunctions for solving integer
linear programs (ILPs) [4, 11, 2, 8, 10, 13]; the literature sometimes also
uses the name “Stabbing Planes” (SP), see [4]. In each node, a general
disjunction of the form
$\alpha^{\top}x\leq\delta\lor\alpha^{\top}x\geq\delta+1$ for
$\alpha\in\mathds{Z}^{n}$, $\delta\in\mathds{Z}$ is used to create two child
nodes.

Branching on general disjunctions lies at the core of Lenstra’s algorithm for
integer programming in fixed dimension [20]. It has also been used, for
example, for special ordered sets [3], exploiting flatness [9], achieving
feasibility [21], and symmetry handling [22].

Nevertheless, the dominant strategy in practice is to employ variable
branching of the form $x_{i}\leq\delta\lor x_{i}\geq\delta+1$ for some
variable $x_{i}$, which is the special case where $\alpha$ is the $i$th unit
vector. Some reasons for this choice are that the selection of a branching
disjunction is easier, the sparsity of the constraint matrix is not increased,
and it often allows to fix variables, e.g., if the variables are binary. This
variable branching strategy is then usually enhanced by the application of
cutting planes like Chvátal-Gomory cuts in a branch-and-cut framework, which
has seen a tremendous improvement over the last decades.

As a proof system, branch-and-bound with general disjunctions is not only a
generalization of branch-and-bound using variable disjunctions, but also
branch-and-cut with variable disjunctions and Chvátal-Gomory cuts, see Beame
et al. [4]. Hence, lower bounds on the size of a branch-and-bound tree using
general disjunctions are also lower bounds on the size of a branch-and-cut
tree using Chvátal-Gomory cuts. This fact shows that branch-and-bound using
general disjunctions form a quite general and important algorithm class.

It is thus surprising that so far no family of integer linear programs
provably requiring branch-and-bound trees using general disjunctions of super-
polynomial size (in the encoding length of the program) without some kind of
caveat is known. In fact, no super-linear bounds are known. In this paper we
close this gap by providing a class of compact integer programs requiring
branch-and-bound trees using general disjunctions of size
$2^{\Omega(L^{1/12-\epsilon})}$ for every $\epsilon>0$, where $L$ denotes the
encoding length of the ILP. This has been posed as an open problem by Dadush
and Tiwari [7].

We briefly survey previous contributions: It is actually relatively easy to
give families of ILPs which require branch-and-bound trees of exponential size
_in the number of variables of the ILP_ (but not the encoding size of the
ILP). Here the two main strategies are the following: Dadush and Tiwari [7]
argued that an ILP which is barely infeasible (i.e., removal of any constraint
makes the ILP feasible) must require large branch-and-bound trees, since it is
impossible to construct a certified branch-and-bound tree which does not use
every constraint in at least one Farkas-certificate at its leaves. More
accurately, the obtained bound is the number of constraints divided by the
number of variables, which is only strong for a large number of constraints.
This weakness is mitigated by an extended formulation of the ILP they use
(with polynomial encoding size in the number of variables). However, this
formulation also uses continuous variables. Their strategy was later
generalized by Dey et al. [10]. The other strategy, as investigated by Gläser
and Pfetsch [13], is based on finding a large set of points which have to be
associated to different leaves of some given branch-and-bound trees. Formally,
it considers hiding sets, which have been introduced by Kaibel and Weltge
[17]. However, it seems impossible to derive bounds on the size of a branch-
and-bound tree which exceed the number of the constraints of the ILP via
either of these two strategies.

Despite the fact that no strong lower bounds on the size of a branch-and-bound
tree have been available prior to this paper, Beame et al. [4] gave a family
of unsatisfiable CNF formulas, such that refuting the corresponding ILP
requires a branch-and-bound tree of _depth_ $\Omega(n/\log^{2}n)$. Note that
since trees are not necessarily balanced, this does not yield a good lower
bound on the size of a tree.

Besides lower bounds, there are some structural insights into branch-and-bound
using general disjunctions: Dadush and Tiwari [7] have shown that branch-and-
bound using general disjunctions does not become weaker (with respect to
polynomial simulation) when restricting the coefficients of the disjunctions
to have polynomial _encoding length_ (cf. Theorem 1 below), which is crucial
for our argument. If we restrict the coefficients of branch-and-bound using
general disjunctions to polynomial _size_ then branch-and-bound can be quasi-
polynomially simulated by the cutting planes (CP) proof system (using Chvátal-
Gomory cuts), see Fleming et al. [11]. Thus, known lower bounds for CP [23,
16, 12] can be lifted to branch-and-bound using general disjunctions with
polynomially bounded coefficients.

The strategy we employ in this paper is to show that branch-and-bound using
general disjunction admits _quasi-feasible real monotone interpolation_ and
then lift lower bounds for monotone real circuits separating the so-called
clique-coloring pair given by Pudlák [23] (cf. Theorem 2) to lower bounds for
branch-and-bound trees. This idea is explained in Section 2 and has already
been successfully used for other proof systems. Most prominently, [23] derived
sub-exponential lower bounds for CP for the same ILP used below by showing
that CP admits real feasible monotone interpolation and a similar result for
the resolution proof system. The concept of feasible interpolation and the
method in which it is used to derive lower bounds has been developed in the
sequence of papers [18, 25, 19, 6, 23].

The rest of this paper is structured as follows: We first survey some
necessary preliminaries in Section 2. Then we explicitly state our results in
Section 3 and describe in which way they are related. The proofs are then
given in Section 4.

##  2 Preliminaries

For polyhedra $P\subseteq\mathds{R}^{n_{1}}$ and
$Q\subseteq\mathds{R}^{n_{2}}$, let $P\times
Q=\\{\binom{x}{y}\in\mathds{R}^{n_{1}+n_{2}}\,|\,x\in P,\;y\in Q\\}$ denote
their Cartesian product. For $n\in\mathds{N}$, we use
$[n]\coloneqq\\{1,\dots,n\\}$.

#### Systems of Linear Inequalities

Let $Ax\leq b$ with $A\in\mathds{Q}^{m\times n}$ and $b\in\mathds{Q}^{m}$ be a
system of linear inequalities. By scaling, we can assume that $A$ and $b$ have
integral entries. If a polyhedron $P$ is described by $Ax\leq b$ we write
$\\{Ax\leq b\\}\coloneqq\\{x~{}|~{}Ax\leq b\\}=P$ for brevity.

We say $Ax\leq b$ is _integer-feasible_ , if there is a point
$\hat{x}\in\mathds{Z}^{n}$ with $A\hat{x}\leq b$ and _integer-infeasible_
otherwise. The polyhedron $\\{Ax\leq b\\}$ is _integer-free_ if $Ax\leq b$ is
integer-infeasible. Similarly, $Ax\leq b$ is _LP-feasible_ , if there is a
point $\hat{x}\in\mathds{Q}^{n}$ with $A\hat{x}\leq b$ and _LP-infeasible_
otherwise.

A _Farkas-certificate (of infeasibility)_ for the system $Ax\leq b$ is a
vector $f\in\mathds{Z}^{m}_{+}$, such that $f^{\top}A=0$ and $f^{\top}b<0$. It
is well known that a linear system $Ax\leq b$ is LP-infeasible if and only if
it admits a Farkas-certificate of infeasibility. Note that the restriction to
integral $f$ is without loss of generality.

#### Branch-and-Bound Trees

To fix notation, we formalize branch-and-bound trees. A _disjunction_ is a
pair of linear inequalities of the form
$(\alpha^{\top}x\leq\delta,\;\alpha^{\top}x\geq\delta+1)$, where
$\alpha\in\mathds{Z}^{n}$ and $\delta\in\mathds{Z}$, which we denote
$\alpha^{\top}x\leq\delta\lor\alpha^{\top}x\geq\delta+1$. Note that every
integer point satisfies exactly one of them. A _branch-and-bound proof (of
integer-infeasibility)_ or _branch-and-bound tree_ for an system of linear
inequalities $(P)$ is a rooted binary directed tree $T$ with the following
properties:

  1. 1.

For every non-leaf node $N$ there is a disjunction
$\alpha^{\top}x\leq\delta\lor\alpha^{\top}x\geq\delta+1$, such that the _left_
outgoing edge of $N$ is labeled with the inequality $\alpha^{\top}x\leq\delta$
and the _right_ edge is labeled with $\alpha^{\top}x\geq\beta+1$. The neighbor
$N_{\leq}$ of $N$ incident to the left edge is called the
_$(\alpha^{\top}x\leq\delta)$ -child_ of $N$, whereas the neighbor $N_{\geq}$
incident to the right edge is the _$(\alpha^{\top}x\geq\delta+1)$ -child_. The
_$(\alpha^{\top}x\leq\delta)$ -branch_ at a node $N$ is the directed subtree
$T(N_{\leq})$ rooted at $N_{\leq}$ and the _$(\alpha^{\top}x\geq\delta+1)$
-branch_ is the subtree $T(N_{\geq})$ rooted at $N_{\geq}$.

  2. 2.

For a node $N$ in $T$, the problem $T_{N}(P)$ _associated to $N$ in a branch-
and-bound tree $T$ for $(P)$_ is (the LP-relaxation) of $(P)$ and all
constraints occurring as edge labels on the unique path from the root to $N$
in $T$. We say $N$ is _feasible_ if $T_{N}(P)$ is LP-feasible and _infeasible_
otherwise. We require $N$ to be infeasible for every leaf $N$ of $T$.

A _branch-and-bound tree for an integer-free polyhedron $P$_ is a branch-and-
bound tree for a system $Ax\leq b$ with $P=\\{Ax\leq b\\}$.

We emphasize that we do not require non-leaf nodes of $T$ to be feasible. This
is convenient, since then a branch-and-bound tree $T$ for a polyhedron $P$ is
also a branch-and-bound tree for every polyhedron $Q\subseteq P$, see, e.g.,
Dey et al. [10]. Moreover, this does not alter the minimal size of a branch-
and-bound tree for any infeasible integer problem.

A tree labeled as described in Property 1 which does not necessarily satisfy
Property 2 will be called _not necessarily valid branch-and-bound tree_. For
emphasis, we sometimes call trees that satisfy both properties _valid_.

Since we consider only binary trees, the number of nodes of a tree will be
asymptotically twice the number of its leaves. Hence, we may define the _size
$\lvert T\rvert$ of $T$_ to denote the number of leaves of $T$, which turns
out to be slightly more convenient. We let $\mathcal{T}(P)$ be the smallest
size of a branch-and-bound tree using general disjunctions proving integer-
freeness of $P$. For $P$ containing integral points, we define
$\mathcal{T}(P)\coloneqq+\infty$.

An important result about branch-and-bound trees is that they can be
recompiled to reduce the encoding length of the coefficients used in the
disjunctions at the nodes. This is stated in the following Theorem by Dadush
and Tiwari [7]:

######  Theorem 1.

(Theorem 1 in [7] and its proof) Let $P\subseteq\mathds{R}^{n}$ be an integer-
free polytope contained in the ball
$B^{n}_{1}(R)\coloneqq\\{x\in\mathds{R}^{n}~{}|~{}\lVert x\rVert_{1}\leq R\\}$
with radius $R\in\mathds{N}$ with respect to the $\ell_{1}$-norm. Let $T$ be a
branch-and-bound tree showing the integer-freeness of $P$. Then, there exists
a branch-and-bound tree $T^{\prime}$ for $P$, such that $\lvert
T^{\prime}\rvert\leq(4n+5)\lvert T\rvert$, and for every disjunction
$\alpha^{\top}x\leq\delta\lor\alpha^{\top}x\geq\delta+1$ which $T^{\prime}$
branches on we have
$\max\\{\lVert\alpha\rVert_{\infty},\lvert\delta\rvert\\}\leq(10nR)^{(n+2)^{2}}$.

A _certified branch-and-bound tree (for a system of inequalities/polyhedron)_
$T$ is a branch-and-bound tree (for a system of inequalities/polyhedron),
where attached to every leaf $L$ is a Farkas-certificate $f^{L}$ of
infeasibility for the problem associated to $L$.

#### Monotone Real Circuits

A _monotone real circuit_ $C$ is an acyclic directed graph whose vertices are
called _gates_ , such that every gate has either zero or two incoming edges
and the incoming edges at every gate are ordered. The number of incoming edges
of a gate is called its _fan-in_. If gate $g$ has fan-in zero, it is called an
_input gate_ and is labeled with a variable $x_{i}$ and if $g$ has fan-in two,
then $g$ is labeled by a non-decreasing function
$f_{g}\colon\mathds{R}^{2}\rightarrow\mathds{R}$, which is the _function
applied at $g$_. If $x=(x_{1},\dots,x_{k})$ are the variables occurring as
labels of input gates, we define (slightly abusing notation) the function
$g\colon\mathds{R}^{k}\rightarrow\mathds{R}$ _computed by $g$_ inductively
(along a topological order of the underlying graph) to be $g(x)=x_{j}$, if $g$
is an input gate labeled by $x_{j}$ and by $f_{g}(g_{1}(x),g_{2}(x))$, if $g$
is a non-input gate and $g_{1}$ and $g_{2}$ are the first and second
predecessors of $g$. Finally, there is a designated output gate $h$, and the
value $C(x)$ computed by $C$ on input $x$ is $h(x)$. The _size_ $\lvert
C\rvert$ of a circuit $C$ is the number of its gates.

Note that bounded fan-in is essential, since monotone real circuits with
unbounded fan-in of linear size can compute arbitrary monotone functions
(consider the circuit with a unique non-input gate connected to all inputs).
Moreover, the term ‘real monotone’ circuit is slightly misleading: the
arithmetical structure of the real numbers $\mathds{R}$ does not play a role
in above definition – instead $\mathds{R}$ merely plays the role of a
sufficiently large linearly ordered domain (this has already been mentioned in
[23]).

A circuit $C$ _decides_ (the membership problem for) a set
$X\subseteq\mathds{R}^{k}$, if $C(x)=1$ for $x\in X$ and $C(x)=0$ otherwise.
Similarly, $C$ separates two sets $Z_{1}\subseteq\mathds{R}^{k}$ and
$Z_{2}\subseteq\mathds{R}^{k}$, if $C(z)=1$ for all $z\in Z_{1}$ and $C(z)=0$
for all $z\in Z_{2}$ or vice versa. While modifying a given circuit, _post-
composing_ the function $f_{g}$ applied at a gate $g$ with a function
$\varphi\colon\mathds{R}\rightarrow\mathds{R}$ means replacing $f_{g}$ by
$\varphi\circ f_{g}$ , where $\circ$ denotes the composition of functions.
Similarly, _pre-composing the first [second] input_ means replacing the
function $f_{g}\colon x,y\mapsto f_{g}(x,y)$ by $x,y\mapsto
f_{g}(\varphi(x),y)$ [${x,y\mapsto f_{g}(x,\varphi(y))}$]. The notion of
monotone real circuits was introduced in [23].

#### Interpolation

We briefly translate the notion of interpolation into the language of linear
integer programs. For this, we consider integer-infeasible linear inequality
systems of the following form:

$\begin{pmatrix}A\\\ 0\end{pmatrix}x+\begin{pmatrix}0\\\
B\end{pmatrix}y+\begin{pmatrix}C\\\ D\end{pmatrix}z\leq\begin{pmatrix}a\\\
b\end{pmatrix},\qquad x,\,y,\,z\in\\{0,1\\}^{n_{1}+n_{2}+n_{3}},$ (1)

where $C\geq 0$ and $D\leq 0$ (entry-wise). Moreover, we let
$A\in\mathds{Z}^{m_{1}\times n_{1}}$, $B\in\mathds{Z}^{m_{2}\times n_{2}}$,
$C\in\mathds{Z}^{m_{1}\times n_{3}}$, $D\in\mathds{Z}^{m_{2}\times n_{3}}$,
$a\in\mathds{Z}^{m_{1}}$, $b\in\mathds{Z}^{m_{2}}$ and $n\coloneqq
n_{1}+n_{2}+n_{3}$.

Since (1) is integer-infeasible, at least one of the systems $Ax\leq
a-Cz,\;x\in\\{0,1\\}^{n_{1}}$ or $By\leq b-Dz,\;y\in\\{0,1\\}^{n_{2}}$ is
infeasible for every fixed $z\in\\{0,1\\}^{n_{3}}$. An _interpolant_ for (1)
is a binary function $I\colon\\{0,1\\}^{n_{3}}\rightarrow\\{0,1\\}$, such that
$I(z)=1$ implies that the first system is infeasible and $I(z)=0$ implies that
the second is infeasible. Note that there is a interpolant for every integer-
infeasible system of the form (1). We say a proof system $\mathcal{S}$ _admits
(monotone/real monotone) [quasi-]feasible interpolation_ , if for any proof of
infeasibility of (1) in $\mathcal{S}$ of size $S$ there exists a
(monotone/real monotone) circuit of size [quasi-]polynomial in $S$ and the
encoding size of (1) computing such an interpolant. Then, if every such
monotone circuit must be large, also any proof for (1) in $\mathcal{S}$ must
be large. This is the case for the examples described in the next paragraph.

#### The Clique-Coloring Pair and the Broken-Mosquito-Screen Pair

The following construction is based on the observation that no $r$-vertex
graph $G$ simultaneously admits both a $(k-1)$-coloring and a $k$-clique. This
is expressed by the integer-infeasibility of:

$\displaystyle x_{i\ell}+x_{j\ell}$ $\displaystyle\leq 2-z_{ij}$
$\displaystyle\forall\,\\{i,j\\}\in\binom{[r]}{2},\;\forall\,\ell\in[k-1],$
(2a) $\displaystyle\sum_{\ell\in[k-1]}x_{i\ell}$ $\displaystyle\geq 1$
$\displaystyle\forall\,i\in[r],$ (2b) $\displaystyle y_{i}+y_{j}$
$\displaystyle\leq 1+z_{ij}$
$\displaystyle\forall\,\\{i,j\\}\in\binom{[r]}{2},$ (2c)
$\displaystyle\sum_{i\in[r]}y_{i}$ $\displaystyle\geq k,$ (2d) $\displaystyle
x\in[0,1]^{r\times(k-1)},\;$ $\displaystyle
y\in[0,1]^{r},\;z\in[0,1]^{{[r]\choose 2}},$ (2e)

where we interpret $z\in\\{0,1\\}^{[r]\choose 2}$ as an encoding of the graph
$G=([r],E)$, with $z_{ij}=1$ if and only if $\\{i,j\\}\in E$,
$x\in\\{0,1\\}^{r\times(k-1)}$ as a $(k-1)$-coloring of $G$, with
$x_{i\ell}=1$ if and only if vertex $i$ gets assigned color $\ell$, and
$y\in\\{0,1\\}^{r}$ as an $k$-clique of $G$, with $y_{i}=1$ if and only the
clique contains vertex $i$.

If we write (2) in the form of (1), the pair of sets

$\displaystyle Z_{1}\coloneqq\\{z\in\\{0,1\\}^{[r]\choose 2}~{}|~{}\exists
x\in\\{0,1\\}^{r\times(k-1)}\colon Ax\leq a-Cz\\}\text{ and }$ $\displaystyle
Z_{2}\coloneqq\\{z\in\\{0,1\\}^{[r]\choose 2}~{}|~{}\exists
y\in\\{0,1\\}^{r}\colon By\leq b-Dz\\}$

is known as the _clique-coloring pair_ or _CC-pair_. Note that $n_{1}=r(k-1)$,
$n_{2}=r$, and $n_{3}={r\choose 2}=(r^{2}-r)/2$ for later calculations. As
already remarked, we have $Z_{1}\cap Z_{2}=\emptyset$.

Pudlák [23] gave the following lower-bound for any monotone real circuit
separating the CC-pair:

######  Theorem 2.

Every family of monotone real circuits separating the CC-pair with $r$
vertices and $k\coloneqq\lfloor\frac{1}{8}(r/\log r)^{2/3}\rfloor$ has size
$2^{\Omega((r/\log r)^{1/3})}$.

Note that all logarithms in this paper are with respect to base $2$.

Since $n_{3}=(r^{2}-r)/2$ is the number of inputs to a circuit separating the
CC-pair, we note

$2^{\Omega((r/\log r)^{1/3})}=2^{\Omega((n_{3}/\log n_{3})^{1/6})}\in
2^{\Omega(n_{3}^{1/6-\epsilon})}\text{ for every }\epsilon>0.$

Theorem 2 is in contrast to the fact that the CC-Pair can be separated in
polynomial time by semi-definite programming using Lovász’ Theta body (cf.,
e.g., Remark 9.3.20(b) in [14]).

Another example of a disjoint pair of languages which requires a large
monotone real circuit to be separated is the _broken-mosquito-screen pair_ or
_BMS-pair_. The BMS-pair is equivalent to the CC-pair [24] and is therefore
also polynomial time separable. For the BMS-pair, a slightly more explicit
bound is available in the literature: Cook and Haken [15] show that any
circuit separating the BMS-pair has at least $2^{Kn_{3}^{1/8}}$ gates for some
$K>0.32$.

##  3 Results

The central result of this work is that branch-and-bound using general
disjunctions admits quasi-feasible monotone real interpolation, that is:

######  Theorem 3.

Given a branch-and-bound tree $T$ for (1), there exists a monotone real
circuit of size $50(n+1)^{2}\lvert
T\rvert^{2}\cdot[(n+2)^{2}\log(10n^{3}+3)]^{\log((4n+5)\lvert T\rvert)}$ with
input $z$, which separates the sets
$Z_{1}\coloneqq\\{z\in\\{0,1\\}^{n_{3}}~{}|~{}\exists
x\in\\{0,1\\}^{n_{1}}\colon Ax\leq a-Cz\\}$ and
$Z_{2}\coloneqq\\{z\in\\{0,1\\}^{n_{3}}~{}|~{}\exists
y\in\\{0,1\\}^{n_{2}}\colon By\leq b-Dz\\}$.

Choosing (1) to be integer linear programs expressing a separation problem for
which we have lower bounds for separating monotone real circuits, we obtain
lower bounds for branch-and-bound trees for (1). For example, combining
Theorems 3 and 2, we immediately obtain the following sub-exponential bound:

######  Theorem 4.

Every family of branch-and-bound trees for (2), where
$k\coloneqq\lfloor\frac{1}{8}(r/\log r)^{2/3}\rfloor$, has size at least
$2^{\Omega(n^{1/6-\epsilon})}$, for every $\epsilon>0$, where $n$ is the
number of variables.

We note that one could make this bound completely explicit, i.e., for fixed
$\epsilon>0$, we can give $N\in\mathds{N}$ and $\delta>0$, such that any
branch-and-bound tree for (2) has size at least $2^{\delta n^{1/6-\epsilon}}$
for every $n\geq N$, by tracking the factor hidden in the $\Omega$-notation in
Theorem 2 through its proof (see [23] building on [1] as presented in [26]).
Alternatively, we can give a similar bound for the BMS-pair, which can then be
made explicit by some elementary calculations.

Since the encoding length $L$ of (2) satisfies $L\in\Theta(n^{2})$, we
immediately obtain:

######  Corollary 5.

Every family of branch-and-bound trees for (2), where
$k\coloneqq\lfloor\frac{1}{8}(r/\log r)^{2/3}\rfloor$, has size at least
$2^{\Omega(L^{1/12-\epsilon})}$, for every $\epsilon>0$, where $L$ is the
encoding length (2).

The remainder of this section outlines how we prove Theorem 3. For this we
will require three ingredients.

Let $P\in\mathds{R}^{n_{1}}$ and $Q\in\mathds{R}^{n_{2}}$ be two polytopes.
Our first ingredient is the fact that given a certified branch-and-bound tree
$T$ showing the integer-freeness of $P\times Q$, there is a branch-and-bound
tree for the integer-freeness of $P$, which is structurally very close to $T$,
or there is such a tree showing the integer-freeness of $Q$. This is helpful
for showing Theorem 3, since after fixing the variables $z$, the feasible
region of the LP-relaxation of (1) is a product of two lower-dimensional
polytopes:

$\\{x\in[0,1]^{n_{1}}~{}|~{}Ax\leq
a-Cz\\}\times\\{y\in[0,1]^{n_{2}}~{}|~{}By\leq b-Dz\\}.$

Given a branch-and-bound tree $T$ for showing integer-freeness of $P\times
Q\subseteq\mathds{R}^{n_{1}\times n_{2}}$, a branch-and-bound tree
$T^{\prime}$ for $P$ _conforms to $T$_, if their underlying directed graphs
(including the ordering of the children as $\leq$\- and $\geq$-children) are
identical and, if the disjunction used by $T$ at a node $N$ is
$\alpha^{\top}x+\beta^{\top}y\leq\delta\lor\alpha^{\top}x+\beta^{\top}y\geq\delta+1$,
then the disjunction used by $T^{\prime}$ at $N$ is
$\alpha^{\top}x\leq\delta^{\prime}\lor\alpha^{\top}x\geq\delta^{\prime}+1$ for
some $\delta^{\prime}\in\mathds{Z}$.

A precursor to our first ingredient will be the following Lemma.

######  Lemma 6.

(Structural Interpolation Lemma) For every branch-and-bound tree $T$ for an
integer-free product of polytopes $P\times Q$ there exits

  1. (a)

a branch-and-bound tree $T^{P}$ for $P$ conforming to $T$ or

  2. (b)

a branch-and-bound tree $T^{Q}$ for $Q$ conforming to $T$.

By applying Lemma 6 to a smallest branch-and-bound tree for $P\times Q$, we
immediately obtain the following result, which is of independent interest.

######  Corollary 7.

$\mathcal{T}(P\times Q)=\min(\mathcal{T}(P),\mathcal{T}(Q))$

Note that Lemma 6 does not give any information of what the right hand side of
the disjunctions used at the nodes of $T^{P}$ or $T^{Q}$ should be, while
almost every other property of the tree is preserved. The remaining two
ingredients for the proof of Theorem 3 are intended to supply this
information. To this end, it would be helpful, if Farkas-certificates maintain
their validity when passing from $T$ to $T^{P}$ or $T^{Q}$. This is due to the
fact that it is not clear how we can decide the LP-feasibility of a system of
linear inequalities (even without integrality constraints), since we need to
perform computations via monotone real circuits. However, it is easy to check
whether a given Farkas-certificate is valid.

Unfortunately, Lemma 6 does not seem to hold for _certified_ branch-and-bound
trees. Indeed, the naive way to obtain Farkas-certificates for $T^{P}$ (or
$T^{Q}$) from Farkas-certificates for $T$ does not work, i.e., for a leaf $L$
in $T^{P}$ using the projection of the Farkas-certificate $f^{L}$ attached to
$L$ in $T$ onto constraints of $P$ and branching constraints. As a counter
example, consider the square of the two-dimensional cross-polytope

$\displaystyle C_{x}^{2}\times C_{y}^{2}\coloneqq\quad$
$\displaystyle\\{x_{1},x_{2}\in[0,1]\colon\;\sum_{i\in S}x_{i}+\sum_{i\not\in
S}(1-x_{i})\leq\tfrac{3}{2}\quad\forall S\subseteq\\{1,2\\}\\}$
$\displaystyle\times$ $\displaystyle\\{y_{1},y_{2}\in[0,1]\colon\;\sum_{i\in
S}y_{i}+\sum_{i\not\in S}(1-y_{i})\leq\tfrac{3}{2}\quad\forall
S\subseteq\\{1,2\\}\\}$

and the branch-and-bound tree shown in Figure 1(a) for $C_{x}^{2}\times
C_{y}^{2}$. Here, let all Farkas-certificates at the leaves have the form

$\displaystyle 1\,\cdot$ $\displaystyle\qquad\textstyle(\sum_{i\in
S}x_{i}+\sum_{i\not\in S}(1-x_{i})\leq\tfrac{3}{2})$
$\displaystyle\textstyle+$ $\displaystyle\textstyle\sum_{i\in S}$
$\displaystyle 1\,\cdot$ $\displaystyle\qquad(-x_{i}\leq-1)$
$\displaystyle\textstyle+$ $\displaystyle\textstyle\sum_{i\not\in S}$
$\displaystyle 1\,\cdot$ $\displaystyle\qquad(x_{i}\leq 0)$
$\displaystyle\qquad(0\leq-0.5)$

for some $S\subseteq\\{1,2\\}$ or the analogous form for variables from
$C_{y}^{2}$. For any leaf, there is only one such choice.

It is not hard to see that no choice of new right-hand-sides $\hat{\delta}$
can make every Farkas-certificate $\hat{f}^{L}$ obtained as described above
valid for all leaves simultaneously, when we try to obtain a conforming
branch-and-bound tree for either $C_{x}^{2}$ or $C_{y}^{2}$: For $C_{x}^{2}$,
$\hat{\delta}_{r}\leq-1$ has to hold for the right-hand-side
$\hat{\delta}_{r}$ used in the disjunction at the root $r$, if all Farkas-
certificates in the $\leq$-branch at the root are to be valid. But then it is
impossible for both Farkas-certificates at leaves in the $\geq$-branch to be
valid simultaneously. The situation for $C_{y}^{2}$ is similar.

for tree=circle, fill, inner sep=0pt, minimum size=6pt, l sep=20pt, s sep =
40pt [, [, edge label=node[midway,left,yshift =2pt] $x_{1}\leq 0$ [,edge
label=node[midway,left,yshift =2pt] $y_{1}\leq 0$, [,cross, edge
label=node[midway,left,yshift =2pt] $y_{2}\leq 0$] [,cross, edge
label=node[midway,right,yshift =2pt] $y_{2}\geq 1$] ] [,edge
label=node[midway,right,yshift =2pt] $y_{1}\geq 1$ [,cross, edge
label=node[midway,left,yshift =2pt] $y_{2}\leq 0$] [,cross, edge
label=node[midway,right,yshift =2pt] $y_{2}\geq 1$] ] ] [,edge
label=node[midway,right,yshift =2pt] $x_{1}\geq 1$ [, cross, edge
label=node[midway,left,yshift =2pt] $x_{2}\leq 0$] [, cross, edge
label=node[midway,right,yshift =2pt] $x_{2}\geq 1$] ] ]

(a) A branch-and-bound tree for $C_{x}^{2}\times C_{y}^{2}$.

for tree=circle, fill, inner sep=0pt, minimum size=6pt, l sep=20pt, s sep =
40pt [, [, edge label=node[midway,left,yshift =2pt] $0\leq 5$ [,edge
label=node[midway,left,yshift =2pt] $y_{1}\leq 0$, [,cross, edge
label=node[midway,left,yshift =2pt] $y_{2}\leq 0$] [,cross, edge
label=node[midway,right,yshift =2pt] $y_{2}\geq 1$] ] [,edge
label=node[midway,right,yshift =2pt] $y_{1}\geq 1$ [,cross, edge
label=node[midway,left,yshift =2pt] $y_{2}\leq 0$] [,cross, edge
label=node[midway,right,yshift =2pt] $y_{2}\geq 1$] ] ] [,gray,edge
label=node[midway,right,yshift =2pt] $0\geq 5$, edge =gray [, cross, gray,
edge label=node[midway,left,yshift =2pt] $0\leq 0$, edge =gray] [, cross,
gray, edge label=node[midway,right,yshift =2pt] $0\geq 1$, edge =gray] ] ]

(b) A conforming tree using quasi-Farkas-certificates.

Figure 1: A branch-and-bound tree for $C_{x}^{2}\times C_{y}^{2}$ showing that
Lemma 6 does not hold for certified branch-and-bound trees. (b) shows a tree
for $C_{y}^{2}$ conforming to the one in (a) using quasi-Farkas-certificates.
For the grey part of the tree, the second case from the definition of quasi-
Farkas-certificates holds, i.e., we do not require the validity of Farkas-
certificates there.

However, if we relax the notion of a Farkas-certificate very slightly, then
Lemma 6 holds also for certified trees: Let $P$ be a polytope and $U$ an
arbitrary set with $P\subseteq U$. A _quasi-certified branch-and-bound tree_
$T$ for $P$ relative to $U$ is a branch-and-bound tree for $P$, such that to
every leaf $L$ there is an attached _quasi-Farkas-certificate $f^{L}$ relative
to $U$_, i.e., a vector $f^{L}\in\mathds{Z}^{m_{L}}_{+}$ indexed by the
$m_{L}$ constraints of the problem $T_{L}(P)$ associated to $L$, such that

  1. 1.

$f^{L}$ is a valid Farkas-certificate for $T_{L}(P)$ or

  2. 2.

an edge on the unique root-leaf path in $T$ to $L$ is labeled with a
constraint $\alpha^{\top}x\leq\gamma$ ($\alpha^{\top}x\geq\gamma+1$), such
that $U\cap\\{\alpha^{\top}x\leq\gamma\\}=\emptyset$
($U\cap\\{\alpha^{\top}x\geq\gamma+1\\}=\emptyset$).

Note that $f^{L}$ does not appear in the second condition. A quasi-certified
branch-and-bound tree $T^{\prime}$ for $P$ _conforms_ to a quasi-certified
branch-and-bound tree $T$ for $P\times Q$, if it does so as (uncertified)
branch-and-bound tree and moreover the quasi-Farkas-certificate
$(f^{\prime})^{L}$ attached to a leaf $L$ of $T^{\prime}$ is the projection of
the quasi-Farkas-certificate $f^{L}$ attached to the leaf $L$ in $T$ onto
variables corresponding to constraints of $P$ and branching constraints.

In the above example, there exists a quasi-certified branch-and-bound relative
to $[0,1]^{2}$ conforming to the previously problematic tree, which is shown
in Figure (1(b)). More generally, we have:

######  Lemma 8.

(Certified Structural Interpolation Lemma) For every quasi-certified branch-
and-bound tree $T$ for an integer-free product of polytopes $P\times Q$
relative to $U=U_{P}\times U_{Q}$, where $P\subseteq U_{P}$, $Q\subseteq
U_{Q}$ and $U_{P}$ and $U_{Q}$ are bounded, there exists

  1. (a)

a quasi-certified branch-and-bound tree $T^{P}$ for $P$ relative to $U_{P}$
conforming to $T$ or

  2. (b)

a quasi-certified branch-and-bound tree $T^{Q}$ for $Q$ relative to $U_{Q}$
conforming to $T$.

Passing from certified trees to quasi-certified trees allows us to choose not
to branch at a node $N$ of $T$ during construction of $T^{P}$ or $T^{Q}$ and
instead immediately proceed as in one of the subtrees rooted at the children
of $N$. Conceptually, it might seem cleaner to consider certified branch-and-
bound trees which embed into $T$ for some suitable notion of embedding.
However, this does not appear to work well with certificates. Moreover, we do
not want to be forced to enumerate over all possible embedded trees later.

As previously mentioned, the last two ingredients for the proof of Theorem 3
instruct us how to reconstruct the right-hand-sides of the disjunctions in the
tree $T^{P}$ or $T^{Q}$ given by Lemma 8. The first ingredient is Theorem 1,
which establishes that the set of possible right-hand-sides is not too large
(if we recompile $T$ beforehand).

It then remains to show that if a tree $T^{P}$ as in Lemma 8 exits, we can
search the space of possible right-hand-side – whose size is limited by
Theorem 1 – efficiently via binary search, even in the quite restricted
computational model of monotone real circuits.

More concretely, assume we have chosen values for the right-hand-sides of all
disjunctions used at a descendant of a node $N$ in $T$ and are now choosing a
value $\gamma_{N}$ for the disjunction used at $N$. If we consider (say) the
$(\alpha_{N}^{\top}x\geq\gamma_{N}+1)$-branch at $N$, then we want to choose
$\gamma_{N}$ as small as possible (i.e., we want to choose the inequality
$\alpha_{N}^{\top}x\geq\gamma_{N}+1$ as weak as possible), such that we still
obtain the validity of all quasi-Farkas-certificates in the
$(\alpha_{N}^{\top}x\geq\gamma_{N}+1)$-branch (depending on the choices for
the right-hand-sides for all disjunctions used at ancestors of $N$). Assume
that we have already expressed the simultaneous validity of the quasi-Farkas-
certificates in the $(\alpha_{N}^{\top}x\geq\gamma_{N}+1)$-branch via a
monotone real circuit computing values in $\\{0,1\\}$. The following result
states we can efficiently compute the smallest possible value of $\gamma_{N}$
making these certificates valid via a monotone real circuit:

######  Lemma 9.

(Oblivious Binary Search Lemma) For a monotone real circuit $C$ computing
values in $\\{0,1\\}$ with $k$ inputs, $\Lambda_{\max}\in\mathds{R}$ such that
$C(x_{1},\dots,x_{k-1},\Lambda_{\max})=1$ for all
$x_{1},\dots,x_{k-1}\in\mathds{R}$, and any $q\in\mathds{N}$, there exists a
monotone real circuit $\tilde{C}$ of size $\lvert C\rvert\cdot q$ which
computes

$b\colon(x_{1},\dots,x_{k-1})\mapsto\max\big{\\{}\lambda\in\\{0,\dots,2^{q}-1\\}~{}|~{}\text{$C(x_{1},\dots,x_{k-1},\Lambda_{\max}-\lambda)=1$}\big{\\}}.$

Note that $\tilde{C}$ uses $q$ invocations of $C$ to find the maximal
$\lambda$ among the $2^{q}$ candidates in $\\{0,\dots,2^{q}-1\\}$ causing $C$
to accept on input $(x_{1},\dots,x_{k-1},\Lambda_{\max}-\lambda)$, which is
the best we can reasonably expect while treating $C$ as a black box. In fact,
the concrete form of the set of candidate values is irrelevant – we can search
over any set of this cardinality with a circuit of the same size. This
reflects the fact that the definition of monotone circuits does not make use
of the arithmetical structure of the real numbers. Finally, we note that the
assumption $C(x_{1},\dots,x_{k-1},\Lambda_{\max})=1$ for all
$x_{1},\dots,x_{k-1}\in\mathds{R}$ is purely for convenience and could be
replaced by one more invocation of $C$ and a slightly less elegant definition
of $b$.

A key observation is that we are able to choose the right-hand-side
$\gamma_{N}$ of the disjunction at a node $N$ by querying the circuit
corresponding to the smaller child subtree. We then have to invoke the circuit
corresponding to the larger subtree only once, to ensure that this choice of
$\gamma_{N}$ works for both subtrees. This will ensure the efficiency of our
construction. Formally, we have:

######  Corollary 10.

For $\kappa$, $\Lambda_{\min}$, $\Lambda_{\max}\in\mathds{Z}$ and monotone
real circuit $C_{1}$ and $C_{2}$ computing values in $\\{0,1\\}$ with $k$
inputs each, such that $C_{1}(x_{1},\dots,x_{k-1},\Lambda_{\max})=1$ for all
$x_{1},\dots,x_{k-1}\in\mathds{R}$ and
$C_{2}(x_{1},\dots,x_{k-1},\kappa-\Lambda_{\min})=1$ for all
$x_{1},\dots,x_{k-1}\in\mathds{R}$, there exists a monotone real circuit
$\tilde{C}$ with $k-1$ inputs which decides whether there exist integral
values $x_{k}$, $x^{\prime}_{k}\in\mathds{Z}$ with
$x_{k}+x^{\prime}_{k}=\kappa$, such that
$C_{1}(x_{1},\dots,x_{k})=C_{2}(x_{1},\dots,x_{k-1},x^{\prime}_{k})=1$ of size
$\lvert C_{1}\rvert\cdot\lceil\log(L+1)\rceil+\lvert C_{2}\rvert$, where
$L\coloneqq\Lambda_{\max}-\Lambda_{\min}$.

Note that above lemma and its corollary are the reason we consider monotone
real circuit complexity. We do not see a way in which binary monotone circuits
can achieve a similar result (when the inputs are provided in binary
encoding).

Finally, for the proof of Theorem 3, we will construct a monotone real circuit
which on input $z\in Z_{1}\cup Z_{2}$ decides whether after fixing the
variables $z$ in (1), there exists a branch-and-bound tree $T^{P(z)}$ for
$P(z)={\\{x\in\\{0,1\\}^{n_{1}}~{}|~{}Ax\leq a-Cz\\}}$ as in Lemma 8 by
efficiently searching the space of possible right-hand-sides using Corollary
10. Clearly, if such right-hand-sides exist, we have $z\in Z_{2}$ and $z\in
Z_{1}$ otherwise.

##  4 Proofs

###  4.1 Proof of Lemmas 6 and 8

To showcase our technique, we begin by showing Lemma 6:

###### Proof of Lemma 6.

Let $P\coloneqq\\{x~{}|~{}Ax\leq a\\}$ and $Q\coloneqq\\{y~{}|~{}By\leq b\\}$.
We will proceed by induction on $\lvert T\rvert$. In case $\lvert T\rvert=1$,
we have $P\times Q=\emptyset$, i.e., $P=\emptyset$ or $Q=\emptyset$, say
$P=\emptyset$. Then there exists a branch-and-bound tree $T^{\prime}$ for $P$
with $\lvert T^{\prime}\rvert=1$ which conforms to $T$, since their common
underlying directed graph does not contain any internal nodes.

Assume $\lvert T\rvert>1$ and that
$\alpha^{\top}x+\beta^{\top}y\leq\delta\lor\alpha^{\top}x+\beta^{\top}y\geq\delta+1$
is the topmost disjunction of $T$. Let $N_{\leq}$ denote the $\leq$-child of
the root of $T$ and $T(N_{\leq})$ the subtree of $T$ rooted at $N_{\leq}$. For
any $\gamma\in\mathds{Z}$ the subtree $T(N_{\leq})$ is a valid branch-and-
bound tree for

$(P\times
Q)_{\leq\gamma}\coloneqq(P\cap\\{\alpha^{\top}x\leq\delta+\gamma\\})\times(Q\cap\\{\beta^{\top}y\leq-\gamma\\}),$

since the two added constraints imply
$\alpha^{\top}x+\beta^{\top}y\leq\delta$.

The induction hypothesis then implies that either (a) or (b) holds for
$T(N_{\leq})$ and $(P\times Q)_{\leq\gamma}$. This allows us to define
$(\mu_{\leq}(\gamma))_{\gamma\in\mathds{Z}}$ by

$\displaystyle\mu_{\leq}(\gamma)\coloneqq\begin{cases}-1,&\text{if
case~{}\ref{case:confP} holds for~{}$T(N_{\leq})$ and~{}$(P\times
Q)_{\leq\gamma}$, but case~{}\ref{case:confQ} does not,}\\\ 0,&\text{if
cases~{}\ref{case:confP} and~{}\ref{case:confQ} both hold for~{}$T(N_{\leq})$
and~{}$(P\times Q)_{\leq\gamma}$,}\\\ 1,&\text{if case~{}\ref{case:confQ}
holds for~{}$T(N_{\leq})$ and~{}$(P\times Q)_{\leq\gamma}$, but
case~{}\ref{case:confP} does not.}\\\ \end{cases}$

Indeed, by the induction hypothesis, we have defined $\mu_{\leq}$ for all
possible cases. It is easy to see that $\mu_{\leq}$ is non-decreasing.
Moreover, $\mu_{\leq}$ is neither identically $-1$ nor identically $1$, since
sufficiently extreme values of $\gamma$ can render both
$(P\cap\\{\alpha^{\top}x\leq\delta+\gamma\\})$ and
$(Q\cap\\{\beta^{\top}y\leq-\gamma\\})$ empty (and hence any branch-and-bound
tree is valid for them).

Similarly, we let $N_{\geq}$ denote the $\geq$-child of the root of $T$ and
$T(N_{\geq})$ the subtree of $T$ rooted at $N_{\geq}$. We define $(P\times
Q)_{\geq\gamma}\coloneqq(P\cap\\{\alpha^{\top}x\geq\delta+\gamma+1\\})\times(Q\cap\\{\beta^{\top}y\geq-\gamma\\})$
and then $(\mu_{\geq}(\gamma))_{\gamma\in\mathds{Z}}$ by

$\displaystyle\mu_{\geq}(\gamma)\coloneqq\begin{cases}-1,&\text{if
case~{}\ref{case:confP} holds for~{}$T(N_{\geq})$ and~{}$(P\times
Q)_{\geq\gamma}$, but case~{}\ref{case:confQ} does not,}\\\ 0,&\text{if
cases~{}\ref{case:confP} and~{}\ref{case:confQ} both hold for~{}$T(N_{\geq})$
and~{}$(P\times Q)_{\geq\gamma}$,}\\\ 1,&\text{if case~{}\ref{case:confQ}
holds for~{}$T(N_{\geq})$ and~{}$(P\times Q)_{\geq\gamma}$, but
case~{}\ref{case:confP} does not.}\\\ \end{cases}$

Note that $\mu_{\geq}(\gamma)$ is non-increasing and neither identically $-1$
nor identically $1$. We remark that this definition is not symmetric in $P$
and $Q$ (the ‘$+1$’ goes with $P$).

The noted properties of $\mu_{\leq}$ and $\mu_{\geq}$ imply that at least one
of the following cases hold: Either (i) there is $\gamma\in\mathds{Z}$, such
that $\mu_{\leq}(\gamma)\leq 0$ and $\mu_{\geq}(\gamma)\leq 0$, or (ii) there
is $\gamma\in\mathds{Z}$, such that
$\mu_{\leq}(\gamma)=\mu_{\geq}(\gamma-1)=1$.

If there exists $\gamma$ as in (i), we construct $T^{P}$ as desired by
branching on
$\alpha^{\top}x\leq\delta+\gamma\lor\alpha^{\top}x\geq\delta+\gamma+1$ and
attaching to the resulting children the trees for
$(P\cap\\{\alpha^{\top}x\leq\delta+\gamma\\})$ and
$(P\cap\\{\alpha^{\top}x\geq\delta+\gamma+1\\})$ conforming to $T(N_{\leq})$
and $T(N_{\geq})$ for which existence is guaranteed by $\mu_{\leq}(\gamma)\leq
0$ and $\mu_{\geq}(\gamma)\leq 0$.

Otherwise, there exists $\gamma$ as in (ii) and we construct $T^{Q}$ as
desired by branching on
$\beta^{\top}y\leq-\gamma\lor\beta^{\top}y\geq-\gamma+1$ and attaching to the
resulting children the trees for $(Q\cap\\{\beta^{\top}y\leq-\gamma\\})$ and
$(Q\cap\\{\beta^{\top}y\geq-\gamma+1\\})$ conforming to $T(N_{\leq})$ and
$T(N_{\geq})$ for which existence is guaranteed by
$\mu_{\leq}(\gamma)=\mu_{\geq}(\gamma-1)=1$. ∎

The proof of Lemma 8 follows the same arguments as Lemma 6, but we now need to
track that the condition on the quasi-Farkas certificates holds as well.

###### Proof of Lemma 8.

Let $P\coloneqq\\{x~{}|~{}Ax\leq a\\}$ and $Q\coloneqq\\{y~{}|~{}By\leq b\\}$,
i.e.,

$P\times Q=\left\\{\begin{pmatrix}x\\\
y\end{pmatrix}~{}\Big{|}~{}\begin{pmatrix}A&0\\\
0&B\end{pmatrix}\begin{pmatrix}x\\\ y\end{pmatrix}\leq\begin{pmatrix}a\\\
b\end{pmatrix}\right\\}.$

We will proceed by induction on $\lvert T\rvert$. If we have $\lvert
T\rvert=1$, then the root $r$ of $T$ is the unique node of $T$ and $T$ does
not branch on any disjunctions. Hence, there is a valid Farkas-certificate
$f^{r}$ attached to $r$. Let $f^{r}_{P}$ denote the projection of $f^{r}$ onto
constraints belonging to $P$ and $f^{r}_{Q}$ the projection of $f^{r}$ onto
constraints belonging to $Q$. We then have

$\begin{pmatrix}{f^{r}_{P}}\\\
{f^{r}_{Q}}\end{pmatrix}^{\top}\begin{pmatrix}A&0\\\
0&B\end{pmatrix}=0,\quad\begin{pmatrix}{f^{r}_{P}}\\\
{f^{r}_{Q}}\end{pmatrix}^{\top}\begin{pmatrix}a\\\
b\end{pmatrix}=(f^{r}_{P})^{\top}a+(f^{r}_{Q})^{\top}b<0.$

It follows that $(f^{r}_{P})^{\top}A=0$, $(f^{r}_{Q})^{\top}B=0$, and that
$(f^{r}_{P})^{\top}a<0$ or $(f^{r}_{Q})^{\top}b<0$. Hence, ${f^{r}_{P}}$ is a
Farkas-certificate for the infeasibility of $P$ or $f^{r}_{Q}$ is a Farkas-
certificate for the infeasibility of $Q$. Thus, the branch-and-bound tree with
a single leaf and certificate ${f^{r}_{P}}$ for this leaf is a quasi-certified
branch-and-bound tree for $P$ relative to $U_{P}$ conforming to $T$ or the
branch-and-bound tree with a single leaf and certificate ${f^{r}_{Q}}$ is a
quasi-certified branch-and-bound tree for $Q$ relative for $U_{Q}$ conforming
to $T$.

Assume $\lvert T\rvert>1$ and that
$\alpha^{\top}x+\beta^{\top}y\leq\delta\lor\alpha^{\top}x+\beta^{\top}y\geq\delta+1$
is the topmost disjunction of $T$. Let $N_{\leq}$ denote the $\leq$-child of
the root of $T$ and $T(N_{\leq})$ the subtree of $T$ rooted at $N_{\leq}$. For
any $\gamma\in\mathds{Z}$ the subtree $T(N_{\leq})$ is a valid branch-and-
bound tree for

$(P\times
Q)_{\leq\gamma}\coloneqq(P\cap\\{\alpha^{\top}x\leq\delta+\gamma\\})\times(Q\cap\\{\beta^{\top}y\leq-\gamma\\}),$

since the two added constraints imply
$\alpha^{\top}x+\beta^{\top}y\leq\delta$. In order to use the induction
hypothesis, we must turn $T(N_{\leq})$ into a quasi-certified branch-and-bound
tree for $(P\times Q)_{\leq\gamma}$ relative to $U$. For every leaf $L$ in $T$
which is a descendant of $N_{\leq}$, there is a quasi-Farkas-certificate
$f^{L}$ for the associated subproblem $T_{L}(P\times Q)$. To obtain the
problem $T(N_{\leq})_{L}((P\times Q)_{\leq\gamma})$ associated to $L$ as a
leaf of the branch-and-bound tree $T(N_{\leq})$ for $(P\times
Q)_{\leq\gamma}$, we have to replace the constraint
$\alpha^{\top}x+\beta^{\top}y\leq\delta$, which we denote by $\eta$, by
$\alpha^{\top}x\leq\delta+\gamma$ and $\beta^{\top}y\leq-\gamma$, which we
denote by $\eta_{P}$ and $\eta_{Q}$, respectively. We define $\tilde{f}^{L}$
indexed by the constraints of $T(N_{\leq})_{L}((P\times Q)_{\leq\gamma})$ by

$\tilde{f}^{L}_{\nu}=\begin{cases}f^{L}_{\nu},&\text{if
$\nu\not\in\\{\eta_{P},\eta_{Q}\\}$,}\\\ f^{L}_{\eta},&\text{if
$\nu\in\\{\eta_{P},\eta_{Q}\\}$.}\end{cases}$

We claim that $\tilde{f}^{L}$ is a Farkas-certificate for
$T(N_{\leq})_{L}((P\times Q)_{\leq\gamma})$, if $f^{L}$ is one for
$T_{L}(P\times Q)$. Indeed, let us consider the system $M\binom{x}{y}\leq m$,
with

$M\coloneqq\begin{pmatrix}A&0\\\ 0&B\\\ E_{1}&E_{2}\\\ \end{pmatrix}\text{ and
}m\coloneqq\begin{pmatrix}a\\\ b\\\ e\\\ \end{pmatrix},$

such that with $E\coloneqq[E_{1},E_{2}]$ we have that $E\binom{x}{y}\leq e$
are the constraints of $T_{L}(P\times Q)$ which come from branching decisions
in $T$ and additionally $\eta_{P}$ and $\eta_{Q}$. Moreover, extend $f^{L}$
and $\tilde{f}^{L}$ with zeros, so that the following computations are well-
defined:

$\displaystyle(f^{L}-{\tilde{f}}^{L})^{\top}M$
$\displaystyle=f^{L}_{\eta}M_{\eta}-{\tilde{f}}_{\eta_{P}}^{L}M_{\eta_{P}}-{\tilde{f}}_{\eta_{Q}}^{L}M_{\eta_{Q}}$
$\displaystyle=f^{L}_{\eta}M_{\eta}-f_{\eta}^{L}M_{\eta_{P}}-f_{\eta}^{L}M_{\eta_{Q}}$
$\displaystyle=f^{L}_{\eta}(M_{\eta}-M_{\eta_{P}}-M_{\eta_{Q}})=f^{L}_{\eta}\cdot
0=0$

and

$\displaystyle(f^{L}-{\tilde{f}}^{L})^{\top}m$
$\displaystyle=f^{L}_{\eta}m_{\eta}-{\tilde{f}}_{\eta_{P}}^{L}m_{\eta_{P}}-{\tilde{f}}_{\eta_{Q}}^{L}m_{\eta_{Q}}$
$\displaystyle=f^{L}_{\eta}m_{\eta}-f_{\eta}^{L}m_{\eta_{P}}-f_{\eta}^{L}m_{\eta_{Q}}=0.$

Hence, we have

$\displaystyle({\tilde{f}}^{L})^{\top}M=({f}^{L})^{\top}M=0\text{ and
}({\tilde{f}}^{L})^{\top}m=({f}^{L})^{\top}m<0.$

Thus, $\tilde{f}^{L}$ is a valid Farkas-certificate for the infeasibility of
$T(N_{\leq})_{L}((P\times Q)_{\leq\gamma})$, if $f^{L}$ is one for
$T_{L}(P\times Q)$. Furthermore, note that if there is an edge $e$ in the path
from the root to $L$ in $T$ labeled with an inequality
$\tilde{\alpha}^{\top}x+\tilde{\beta}^{\top}y\leq\tilde{\delta}$, such that
$U\cap\\{\tilde{\alpha}^{\top}x+\tilde{\beta}^{\top}y\leq\tilde{\delta}\\}=\emptyset$
and $e$ is not the edge between the root and $N_{\leq}$, then $e$ is also
contained in the path between the root and $L$ in $T(N_{\leq})$.

Hence, if $U\cap\\{\alpha^{\top}x+\beta^{\top}y\leq\delta\\}\neq\emptyset$,
then $T(N_{\leq})$ with the quasi-Farkas-certificates constructed above is
indeed a valid quasi-certified branch-and-bound tree for $(P\times
Q)_{\leq\gamma}$ relative to $U$ and thus, the induction hypothesis implies
that (a) or (b) holds for $T(N_{\leq})$ as a branch-and-bound tree for
$(P\times Q)_{\leq\gamma}$ relative to $U$. Moreover, if
$U\cap\\{\alpha^{\top}x+\beta^{\top}y\leq\delta\\}=\emptyset$, then we have
$U_{P}\cap\\{\alpha^{\top}x\leq\delta+\gamma\\}=\emptyset$ or
$U_{Q}\cap\\{\beta^{\top}y\leq-\gamma\\}=\emptyset$.

Define the following cases:

  1. (a′)

Case (a) holds for $T(N_{\leq})$ and $(P\times Q)_{\leq\gamma}$ or
$U_{P}\cap\\{\alpha^{\top}x\leq\delta+\gamma\\}=\emptyset$.

  2. (b′)

Case (b) holds for $T(N_{\leq})$ and $(P\times Q)_{\leq\gamma}$ or
$U_{Q}\cap\\{\beta^{\top}y\leq-\gamma\\}=\emptyset$.

This allows us to define $(\mu_{\leq}(\gamma))_{\gamma\in\mathds{Z}}$ by

$\displaystyle\mu_{\leq}(\gamma)\coloneqq\begin{cases}-1,&\text{if
case~{}\ref{case:confP'} holds, but case~{}\ref{case:confQ'} does not,}\\\
0,&\text{if cases~{}\ref{case:confP'} and~{}\ref{case:confQ'} both hold,}\\\
1,&\text{if case~{}\ref{case:confQ'} holds, but case~{}\ref{case:confP'} does
not.}\\\ \end{cases}$

Indeed, by the induction hypothesis and our previous considerations, we have
defined $\mu_{\leq}$ for all possible cases. It is easy to see that
$\mu_{\leq}$ is non-decreasing. Moreover, $\mu_{\leq}$ is neither identically
$-1$ nor identically $1$, since sufficiently extreme values of $\gamma$ can
render both $(U_{P}\cap\\{\alpha^{\top}x\leq\delta+\gamma\\})$ and
$(U_{Q}\cap\\{\beta^{\top}y\leq-\gamma\\})$ empty.

Similarly, one defines $(P\times
Q)_{\geq\gamma}\coloneqq(P\cap\\{\alpha^{\top}x\geq\delta+\gamma+1\\})\times(Q\cap\\{\beta^{\top}y\geq-\gamma\\})$
and then the following cases:

  1. (a′′)

Case (a) holds for $T(N_{\geq})$ and $(P\times Q)_{\geq\gamma}$ or
$U_{P}\cap\\{\alpha^{\top}x\geq\delta+\gamma+1\\}=\emptyset$.

  2. (b′′)

Case (b) holds for $T(N_{\geq})$ and $(P\times Q)_{\geq\gamma}$ or
$U_{Q}\cap\\{\beta^{\top}y\geq-\gamma\\}=\emptyset$,

and finally $(\mu_{\geq}(\gamma))_{\gamma\in\mathds{Z}}$ by

$\displaystyle\mu_{\geq}(\gamma)\coloneqq\begin{cases}-1,&\text{if
case~{}\ref{case:confP''} holds, but case~{}\ref{case:confQ''} does not,}\\\
0,&\text{if cases~{}\ref{case:confP''} and~{}\ref{case:confQ''} both hold,}\\\
1,&\text{if case~{}\ref{case:confQ''} holds, but case~{}\ref{case:confP''}
does not.}\\\ \end{cases}$

One checks easily that $\mu_{\geq}(\gamma)$ is non-increasing and neither
identically $-1$ nor identically $1$.

The noted properties of $\mu_{\leq}$ and $\mu_{\geq}$ imply that at least one
of the following cases hold: (i) There is $\gamma\in\mathds{Z}$, such that
$\mu_{\leq}(\gamma)\leq 0$ and $\mu_{\geq}(\gamma)\leq 0$, or (ii) there is
$\gamma\in\mathds{Z}$, such that $\mu_{\leq}(\gamma)=\mu_{\geq}(\gamma-1)=1$.

If there exists $\gamma$ as in case (i), i.e., cases (a′) and (a′′) hold for
this $\gamma$, we construct $T^{P}$ as desired by branching on
$\alpha^{\top}x\leq\delta+\gamma\lor\alpha^{\top}x\geq\delta+\gamma+1$ and
attaching to the resulting children $N_{\leq}$ and $N_{\geq}$ the following
trees: If (a) holds for $T(N_{\leq})$ and $(P\times Q)_{\leq\gamma}$, we
attach the quasi-certified branch-and-bound tree $T(N_{\leq})^{P}$ for
$P\cap\\{\alpha^{\top}x\leq\delta+\gamma\\}$ relative to $U_{P}$ conforming to
$T(N_{\leq})$ given by (a). While doing so, we can keep the quasi-Farkas-
certificates attached to leaves in $T(N_{\leq})^{P}$. For this, note that the
set of constraints describing the problem
$(T(N_{\leq})^{P})_{L}(P\cap\\{\alpha^{\top}x\leq\gamma+\delta\\})$ associated
to a leaf $L$ in the branch-and-bound tree $T(N_{\leq})^{P}$ for
$P\cap\\{\alpha^{\top}x\leq\gamma+\delta\\}$ is identical to the constraints
describing the problem $(T^{P})_{L}(P)$ associated to $L$ as a leaf of the
branch-and-bound tree $T^{P}$ for $P$. If (a) does not hold for $T(N_{\leq})$
and $(P\times Q)_{\leq\gamma}$, we have
$U_{P}\cap\\{\alpha^{\top}x\leq\delta+\gamma\\}=\emptyset$, and we attach an
arbitrary, not necessarily valid quasi-certified branch-and-bound tree
conforming to $T(N_{\leq})$.

Similarly, if (a) holds for $T(N_{\geq})$ and $(P\times Q)_{\geq\gamma}$, then
we attach to $N_{\geq}$ the quasi-certified branch-and-bound tree
$T(N_{\geq})^{P}$ relative to $U_{P}$ conforming to $T(N_{\geq})$ given by
(a). Otherwise, we have $U_{P}\cap\\{\alpha^{\top}x\geq\delta+\gamma\
+1\\}=\emptyset$, and we attach an arbitrary, not necessarily valid quasi-
certified branch-and-bound tree for $P$ conforming to $T(N_{\geq})$. Choose
quasi-Farkas-certificates as in the previous case.

It is then easy to see that $T^{P}$ is conforming to $T$. It remains to check
that $T^{P}$ is a valid quasi-certified branch-and-bound tree for $P$ relative
to $U_{P}$. For this consider a leaf $L$ of $T^{P}$ in the subtree rooted at
$N_{\leq}$. If we have
$U_{P}\cap\\{\alpha^{\top}x\leq\delta+\gamma\\}=\emptyset$, there is nothing
to check for $f^{L}$. Similarly, if there is an edge in $T(N_{\leq})^{P}$ on
the path from the root to $L$ labeled with an inequality
$\tilde{\alpha}^{\top}x\leq\tilde{\delta}$, such that
$U_{P}\cap\\{\tilde{\alpha}^{\top}x\leq\tilde{\delta}\\}=\emptyset$, then the
same inequality appears on the path from the root to $L$ in $T^{P}$. The only
remaining case is that the quasi-Farkas-certificate $f^{L}$ attached to $L$ in
$T(N_{\leq})^{P}$ is a Farkas-certificate for the associated problem
$(T(N_{\leq})^{P})_{L}(P\cap\\{\alpha^{\top}x\leq\delta+\gamma\\})$. But then
$f^{L}$ is also a Farkas-certificate for the problem $(T^{P})_{L}(P)$
associated to $L$ in $T^{P}$, which is the same problem. For leaves in the
subtree rooted at $N_{\geq}$ we proceed similarly.

In case (ii) we proceed analogously. ∎

###  4.2 Proofs of Lemma 9 and Corollary 10

###### Proof of Lemma 9.

For ease of notation, we write $p\coloneqq q-1$ instead. Thus we have to
compute

$b\colon(x_{1},\dots,x_{k-1})\mapsto\max\big{\\{}\lambda\in\\{0,\dots,2^{p+1}-1\\}~{}|~{}\text{$C(x_{1},\dots,x_{k-1},\Lambda_{\max}-\lambda)=1$}\big{\\}}.$

We will construct a monotone real circuit $\tilde{C}$ of the desired size
which works in $p+1$ phases $0,\dots,p$. For each phase $i$, there will be a
gate $h_{i}$ in $\tilde{C}$ representing the state of computation after phase
$i$. The gate $h_{i}$ will compute the function

$b_{i}(x)\coloneqq\lfloor b(x)\rfloor_{2^{p-i}},$

where $x=(x_{1},\dots,x_{k-1})$ and $\lfloor\cdot\rfloor_{2^{p-i}}$ denotes
rounding down to the nearest integer divisible by $2^{p-i}$. Clearly, this
suffices, since $h_{p}$ then computes the desired function. Moreover, $b_{0}$
can be computed by a copy $C_{0}$ of $C$, which receives
$(x,\Lambda_{\max}-2^{p})$ where the output gate $h_{0}$ is modified to
compute $b_{0}(x)=2^{p}C(x,\Lambda_{\max}-2^{p})$.

To construct the part of $\tilde{C}$ belonging to phase $i>0$, we will rely on
the recurrence

$b_{i}(x)=b_{i-1}(x)+2^{p-i}C(x,\Lambda_{\max}-b_{i-1}(x)-2^{p-i}).$

Unfortunately, this recurrence is not necessarily monotone in $x$ and
$b_{i-1}$ due to the sign on the second occurrence of $b_{i-1}(x)$. However,
since it is immediate from the definition that $b_{i-1}$ is divisible by
$2^{p-(i-1)}$, we might as well consider the recurrence

$b_{i}=\lfloor b_{i-1}\rfloor_{2^{p-(i-1)}}+2^{p-i}C(x,\Lambda_{\max}-\lfloor
b_{i-1}\rfloor_{2^{p-(i-1)}}-2^{p-i}).$ (3)

Note that we drop the dependence of $b_{i}$ and $b_{i-1}$ on $x$ to improve
readability.

Unfortunately for us, the latter recurrence – while clearly monotone in $x$
and $b_{i-1}$ – still does not provide an obvious monotone real circuit, since
the last summand applies a non-monotone function to $b_{i-1}$.

Thus, we have to give a version of $C$, which passes along the old bound
$b_{i-1}$ from the $k$-th input gate to the output gate in the higher order
bits, together with how $C$ behaves on input
$(x,\Lambda_{\max}-b_{i-1}-2^{p-i})$ in the lower order bits, in order to make
our computation monotone.

We begin by assuming that every non-input gate in $C$ applies a function $f$
with $\operatorname{range}f\subseteq(0,\tfrac{1}{2})$. This can be achieved by
post-composing the function applied at every gate with the monotone bijection

$\varphi\colon\mathds{R}\rightarrow(0,\tfrac{1}{2}),\quad
y\mapsto(\arctan(y)+\tfrac{\pi}{2})/2\pi$

and pre-composing every function applied at a gate, which takes as input such
a modified gate, with $\varphi^{-1}$ for the respective input. Let
$C^{\prime}$ be the monotone real circuit obtained from $C$ this way. We then
have $C^{\prime}(x)=\varphi(C(x))$.

Next, we introduce a gate $\tilde{g}_{k}$, which provides both the $k$-th
input (which is supposed to be $b_{i-1}$) and the transformed value of
$\Lambda_{\max}-b_{i-1}-2^{p-i}$, i.e, both inputs to $\tilde{g}_{k}$ are the
$k$-th input gate $g_{k}$ of $C^{\prime}$ and the function applied at
$\tilde{g}_{k}$ is

$f^{i}(g_{k},g_{k})\coloneqq\lfloor
g_{k}\rfloor_{2^{p-(i-1)}}+\varphi\big{(}\Lambda_{\max}-\lfloor
g_{k}\rfloor_{2^{p-(i-1)}}-2^{p-i}\big{)}.$

Then, for every gate $g$ which uses $g_{k}$ as input in $C^{\prime}$, we let
$g$ use $\tilde{g}_{k}$ as input instead. We note $f^{i}$ is non-decreasing:
If an increase of $g_{k}$ would cause the summand involving $\varphi$ to
decrease, then it decreases by at most $\frac{1}{2}$, but the other summand
then increases by at least $1$.

Let $S$ denote the set of gates in $C^{\prime}$ which are a descendant of
$g_{k}$ (hence now of $\tilde{g}_{k}$) and consider a gate $g$ in $S$ with
predecessors $g_{1}$ and $g_{2}$, such that $g_{1}\in S$, but $g_{2}\not\in
S$. We then replace the function $f_{g}(g_{1},g_{2})$ applied at $g$ by the
function

$\displaystyle f^{i}_{g}(g_{1},g_{2})\coloneqq$ $\displaystyle\lfloor
g_{1}\rfloor_{2^{p-(i-1)}}+f_{g}\big{(}\\{g_{1}\\}_{2^{p-(i-1)}},\,g_{2}\big{)},$

where $\\{g_{1}\\}_{2^{p-(i-1)}}\coloneqq g_{1}-\lfloor
g_{1}\rfloor_{2^{p-(i-1)}}$. We check that $f^{i}_{g}$ is non-decreasing: If
an increase of $g_{1}$ would cause $\\{g_{1}\\}$ to decrease, then
$f_{g}(\\{g_{1}\\}_{2^{p-(i-1)}},\,g_{2})$ decreases by at most
$\tfrac{1}{2}$, since $\operatorname{range}f_{g}\subseteq(0,\tfrac{1}{2})$,
while $\lfloor g_{1}\rfloor_{2^{p-(i-1)}}$ increases by at least $1$.

If $g$ is a gate with both predecessor $g_{1}$ and $g_{2}$ in $S$, we replace
the function $f_{g}$ applied at $g$ by

$\displaystyle f^{i}_{g}(g_{1},g_{2})\coloneqq(\lfloor
g_{1}\rfloor_{2^{p-(i-1)}}+\lfloor
g_{2}\rfloor_{2^{p-(i-1)}})/2+f_{g}\big{(}\\{g_{1}\\}_{2^{p-(i-1)}},\,\\{g_{2}\\}_{2^{p-(i-1)}}\big{)},$

Once again, $f_{g}^{i}$ is non-decreasing by an analogous argument.

Let $C_{i}$ denote the monotone real circuit obtained by applying these
modifications to $C^{\prime}$. For a gate $g^{\prime}$ in $C^{\prime}$, let
$g^{i}$ denote the corresponding gate of $C_{i}$. It is then easy to show by
induction along a topological order on the gates of $C^{\prime}$ (or
equivalently $C_{i}$) that

$g^{i}(x,b_{i-1})=\begin{cases}g^{\prime}\big{(}x,\,\Lambda_{\max}-b_{i-1}-2^{p-i}\big{)},&\text{if
$g\not\in S$},\\\
b_{i-1}+g^{\prime}\big{(}x,\,\Lambda_{\max}-b_{i-1}-2^{p-i}\big{)}&\text{if
$g\in S$.}\\\ \end{cases}$

We note that this holds for the input gates $g_{1},\dots g_{k-1}$ and
$\tilde{g}_{k}$. For a non-input gate $g^{\prime}$ in $C^{\prime}$, consider
for example the case where $g$ has predecessors $g^{\prime}_{1}$ and
$g^{\prime}_{2}$, such that $g^{\prime}_{1}\in S$ and $g^{\prime}_{2}\not\in
S$. Then a straight-forward computation yields

$\displaystyle g^{i}(x,b_{i-1})$
$\displaystyle=f^{i}_{g}\big{(}g_{1}^{i}(x,b_{i-1}),g_{2}^{i}(x,b_{i-1})\big{)}$
$\displaystyle=\lfloor
g_{1}^{i}(x,b_{i-1})\rfloor_{2^{p-(1-i)}}+f_{g}\big{(}\\{g_{1}^{i}(x,b_{i-1})\\}_{2^{p-(1-i)}},\,g^{i}_{2}(x,b_{i-1})\big{)}$
$\displaystyle=\lfloor
b_{i-1}+g_{1}^{\prime}\big{(}x,\,\Lambda_{\max}-b_{i-1}-2^{p-i}\big{)}\rfloor_{2^{p-(1-i)}}$
$\displaystyle\quad+f_{g}\big{(}\\{b_{i-1}+g_{1}^{\prime}(x,\,\Lambda_{\max}-b_{i-1}-2^{p-i})\\}_{2^{p-(i-1)}},\,g_{2}^{\prime}(x,\Lambda_{\max}-b_{i-1}-2^{p-i})\big{)}$
$\displaystyle=b_{i-1}+f_{g}\big{(}g_{1}^{\prime}(x,\,\Lambda_{\max}-b_{i-1}-2^{p-i}),\,g_{2}^{\prime}(x,\Lambda_{\max}-b_{i-1}-2^{p-i})\big{)}$
$\displaystyle=b_{i-1}+g^{\prime}\big{(}x,\,\Lambda_{\max}-b_{i-1}-2^{p-i}\big{)}$

as desired, where the first and last identity are due to the definition of the
computed function, the second due to the definition of $f_{g}^{i}$, the third
due to the induction hypothesis and the fourth due to $b_{i-1}=\lfloor
b_{i-1}\rfloor_{2^{p-(i-1)}}$ and $\operatorname{range}g\in(0,\frac{1}{2})$.
The other cases are analogous.

By considering this identity for the output gate $h^{i}$ of $C_{i}$ (note that
we can assume to be in the second case), we obtain

$\displaystyle C_{i}(x,b_{i-1})$
$\displaystyle=b_{i-(i-1)}+C^{\prime}(x,\Lambda_{\max}-b_{i-1}-2^{p-i})$
$\displaystyle=b_{i-(i-1)}+\varphi(C(x,\Lambda_{\max}-b_{i-1}-2^{p-i})).$

Thus, by our recurrence (3), if we post-compose the function applied at
$h_{i}$ with

$y\mapsto\begin{cases}\lfloor y\rfloor_{2^{p-(i-1)}}&\text{if
$\\{y\\}_{2^{p-(i-1)}}<\varphi(1)$},\\\ \lfloor
y\rfloor_{2^{p-(i-1)}}+2^{p-i}&\text{if
$\\{y\\}_{2^{p-(i-1)}}\geq\varphi(1)$},\\\ \end{cases}$

we obtain a monotone real circuit which on input $(x,b_{i-1})$ computes
$b_{i}$. For this, note that
$\\{C_{i}(x,b_{i-1})\\}_{2^{p-(i-1)}}=\varphi(C(x,\Lambda_{\max}-b_{i-1}-2^{p-i}))<\varphi(1)$
is equivalent to $C(x,\Lambda_{\max}-b_{i-1}-2^{p-i})=0$. Then $\tilde{C}$ can
be constructed in the obvious way, i.e., by sequentially using the constructed
circuits $C_{0},\dots,C_{p}$ to compute the values
$b_{0}(x),\dots,b_{p}(x)=b(x)$.

For the size bound, observe that we have used $q=p+1$ copies of $C$ and that
the introduced auxiliary gates $\tilde{g}_{k}$ can be eliminated from the
circuit, since the functions applied at the children of $\tilde{g}_{k}$ can
instead be pre-composed with the function applied at $\tilde{g}_{k}$. ∎

###### Proof of Corollary 10.

Choose $q\coloneqq\lceil\log(L+1)\rceil$ and apply Lemma 9 to $C_{1}$ to
construct $\tilde{C}_{1}$, such that the output gate $h$ of $\tilde{C}_{1}$
computes

$b\colon(x_{1},\dots,x_{k-1})\mapsto\max\big{\\{}\lambda\in\\{0,\dots,2^{q}-1\\}~{}\big{|}~{}\text{$C(x_{1},\dots,\Lambda_{\max}-\lambda)=1$}\big{\\}}.$

and use a copy of $C_{2}$ to compute
$C_{2}(x_{1},\dots,x_{k-1},\kappa-(\Lambda_{\max}-b(x_{1},\dots,x_{k-1})))$.

Clearly, if the output gate of this copy of $C_{2}$ computes $1$, then
$x_{k}=\Lambda_{\max}-b(x_{1},\dots,x_{k-1})$ and $x^{\prime}_{k}=\kappa-
x_{k}$ satisfy
$C_{1}(x_{1},\dots,x_{k-1},x_{k})=C_{2}(x_{1},\dots,x_{k-1},x^{\prime}_{k})=1$
and $x_{k}+x^{\prime}_{k}=\kappa$. Otherwise, there are no possible such
choices for $x_{k}$ and $x_{k}^{\prime}$, since for
$x_{k}<\Lambda_{\max}-b(x_{1},\dots,x_{k-1})$ we have
$C_{1}(x_{1},\dots,x_{k-1},x_{k})=0$ and for
$x_{k}\geq\Lambda_{\max}-b(x_{1},\dots,x_{k-1})$ and $x^{\prime}_{k}=\kappa-
x_{k}$ we have $C_{2}(x_{1},\dots,x_{k-1},x^{\prime}_{k})=0$. Hence, the
constructed circuit decides the question posed in the corollary. ∎

###  4.3 Proof of Theorems 3 and 4

For ease of notation, we assume that the variable bounds in (1) are
incorporated into the constraints. Then the LP-relaxation of (1) is given by:

$\begin{pmatrix}A\\\ 0\end{pmatrix}x+\begin{pmatrix}0\\\
B\end{pmatrix}y+\begin{pmatrix}C\\\ D\end{pmatrix}z\leq\begin{pmatrix}a\\\
b\end{pmatrix},\qquad$

The basic structure of the proof is as follows: Given $z\in Z_{1}\cup Z_{2}$,
where $Z_{1}=\\{z\in\\{0,1\\}^{n_{3}}~{}|~{}\exists
x\in\\{0,1\\}^{n_{1}}\colon Ax\leq a-Cz\\}$ and
$Z_{2}=\\{z\in\\{0,1\\}^{n_{3}}~{}|~{}\exists y\in\\{0,1\\}^{n_{2}}\colon
By\leq b-Dz\\}$, and a branch-and-bound tree $T$ for the infeasibility of (1),
we compute Farkas-certificates for the leaves of $T$ and then obtain a
certified branch-and-bound tree $\tilde{T}$ for $P(z)\times
Q(z)\coloneqq\\{Ax\leq a-Cz\\}\times\\{Bx\leq b-Dz\\}$ by plugging in the
values for $z$ in the disjunctions used in $T$. Then at least one of the
alternatives in Lemma 8 holds. However, since $z\in Z_{1}\cup Z_{2}$, exactly
one of $P(z)$ and $Q(z)$ is integer-feasible, and thus at most one of the
alternatives in Lemma 8 holds. Clearly, we have $z\in Z_{2}$ if and only if
there exists a quasi-certified branch-and-bound tree $(\tilde{T})^{P}$ for
$P(z)$ conforming to $\tilde{T}$. Thus, if we construct a monotone real
circuit $C$ that given values for the $z$ variables decides whether there
exists such a tree $(\tilde{T})^{P}$, then $C$ separates $Z_{1}$ and $Z_{2}$.
We work out the details below:

###### Proof of Theorem 3.

We again assume that variable bounds in (1) are incorporated into the
constraints as above. We begin by applying Theorem 1 to our branch-and-bound
tree $T$ for (1) to obtain a certified branch-and-bound tree $T^{\prime}$ for
(1) with bounded coefficients: Note that the linear programming relaxation of
(1) is contained in the ball $B_{1}^{n}(n)=\\{x\in\mathds{R}^{n}~{}|~{}\lVert
x\rVert_{1}\leq n$}, where $n\coloneqq n_{1}+n_{2}+n_{3}$. Hence, we can
assume that for every disjunction $d^{\top}w\leq\delta\lor
d^{\top}w\geq\delta+1$ used in $T^{\prime}$, we have $\max\\{\lVert
d\rVert_{\infty},\lvert\delta\rvert\\}\leq(10n^{2})^{(n+2)^{2}}$ and moreover
we have $\lvert T^{\prime}\rvert\leq(4n+5)\lvert T\rvert$. Then we fix some
Farkas-certificates for $T^{\prime}$ which thus becomes a certified branch-
and-bound tree.

By fixing the values of $z$ in the disjunctions used in $T^{\prime}$, we
obtain a certified branch-and-bound tree $\tilde{T}$ for $P(z)\times
Q(z)\coloneqq\\{Ax\leq a-Cz\\}\times\\{By\leq b-Dz\\}$. Since $P(z)\times
Q(z)\subseteq[0,1]^{n_{1}}\times[0,1]^{n_{2}}$, we may also consider
$\tilde{T}$ as a quasi-certified branch-and-bound tree for $P(z)\times Q(z)$
relative to $[0,1]^{n_{1}}\times[0,1]^{n_{2}}$.

Let $\mathcal{N}(T^{\prime})$ denote the set of internal nodes of $T^{\prime}$
and let $\gamma\in\mathds{Z}^{\mathcal{N}(T^{\prime})}$. Consider the not
necessarily valid quasi-certified branch-and-bound tree
$\tilde{T}^{P}(\gamma)$ for $P(z)$ relative to $[0,1]^{n_{1}}$, which has the
same underlying directed tree as $\tilde{T}$, and at a node $N$ branches on
the disjunction
$\alpha^{\top}_{N}x\leq\gamma_{N}\lor\alpha^{\top}_{N}x\geq\gamma_{N}+1$, when
$\tilde{T}$ branches at $N$ on the disjunction
$\alpha^{\top}_{N}x+\beta_{N}^{\top}y\leq\delta\lor\alpha^{\top}_{N}x+\beta_{N}^{\top}y\geq\delta_{N}+1$.
Similarly, the Farkas-certificate at a leaf $L$ of $\tilde{T}^{P}(\gamma)$ is
the Farkas-certificate at leaf $L$ of $\tilde{T}$ with the entries
corresponding to constraints from $Q(z)$ removed. We are interested in whether
there exists a choice for $\gamma$ for which $\tilde{T}^{P}(\gamma)$ is a
valid quasi-certified branch-and-bound tree for $P(z)$ relative to
$[0,1]^{n_{1}}$.

For any candidate disjunction
$\alpha^{\top}_{N}x\leq\gamma_{N}\lor\alpha^{\top}_{N}x\geq\gamma_{N}+1$ to be
used at a node $N$ in $\tilde{T}^{P}(\gamma)$, the slab
$\\{x\in\mathds{R}^{n_{1}}\colon\gamma_{N}\leq\alpha^{\top}_{N}x\leq\gamma_{N}+1\\}$
has width
$\frac{1}{\lVert\alpha_{N}\rVert_{2}}\geq\frac{1}{\sqrt{n_{1}}\lVert\alpha_{N}\rVert_{\infty}}$.
Since

$\max\Big{\\{}\Big{(}\frac{\alpha_{N}}{\lVert\alpha_{N}\rVert_{2}}\Big{)}^{\top}x~{}|~{}x\in[0,1]^{n_{1}}\Big{\\}}-\min\Big{\\{}\Big{(}\frac{\alpha_{N}}{\lVert\alpha_{N}\rVert_{2}}\Big{)}^{\top}x~{}|~{}x\in[0,1]^{n_{1}}\Big{\\}}\leq\sqrt{n}_{1},$

we have that at most
$\sqrt{n_{1}}\cdot\sqrt{n_{1}}\lVert\alpha_{N}\rVert_{\infty}+2\leq
n(10n^{2})^{(n+2)^{2}}+2$ of our slabs intersect $[0,1]^{n_{1}}$. Let
$L_{\min}^{N}$ denote the maximal value for $\gamma$ for which
$[0,1]^{n_{1}}\cap\\{\alpha_{N}^{\top}x\leq\gamma\\}=\emptyset$ (cf. Figure
2(a)). Similarly, let $L_{\max}^{N}$ denote the minimal $\gamma$ for which
$[0,1]^{n_{1}}\cap\\{\alpha_{N}^{\top}x\geq\gamma+1\\}=\emptyset$. Moreover,
let $L^{N}\coloneqq L_{\max}^{N}-L_{\min}^{N}$ and
$L\coloneqq\max\\{L^{N}~{}|~{}\text{$N$ internal node of $T^{\prime}$}\\}\leq
n(10n^{2})^{(n+2)^{2}}+2$.

$L_{\min}$$L_{\max}$$L_{\max}+1$$[0,1]^{n_{1}}$ (a) The hyperplanes
$\alpha^{\top}x=\gamma$ for different values of $\gamma$.

for tree=circle, draw, inner sep=0pt, minimum size=14pt, l sep=10pt, s sep =
35pt [$M_{1}$ [$M_{2}$ [,cross] [$M_{3}$ [$N$ [,cross] [$M_{4}$ [,cross]
[,cross] ] ] [,cross] ] ] [,cross] ]

(b) An example for $T^{\prime}$ for which
$\mathcal{V}^{+}(N)=\\{\gamma^{+}_{M_{2}}\\}$,
$\mathcal{V}^{-}(N)=\\{\gamma^{-}_{M_{1}},\gamma^{-}_{M_{3}}\\}$ and
$\mathcal{U}(N)=\\{\gamma^{-}_{N},\gamma^{+}_{N},\gamma^{-}_{M_{4}},\gamma^{+}_{M_{4}}\\}$.

Figure 2: Illustrations of $L_{\min}$, $L_{\max}$, $\mathcal{U}(N)$ and
$\mathcal{V}(N)$.

Then, for every internal node $N$ of $T^{\prime}$, we introduce two variables
$\gamma_{N}^{+}$ and $\gamma_{N}^{-}$. Variable $\gamma_{N}^{+}$ represents
how far the right-hand-side of the disjunction at $N$ is chosen away from the
lower bound $L_{\min}^{N}$, while $\gamma_{N}^{-}$ represents how far the
right-hand-side of the disjunction at $N$ is chosen away from the upper bound
$L_{\max}^{N}$. Thus,
$\gamma_{N}=L_{\min}^{N}+\gamma_{N}^{+}=L_{\max}^{N}-\gamma_{n}^{-}$. Hence,
in order for the pair $(\gamma_{N}^{+},\gamma_{N}^{-})$ to represent a valid
right-hand-side for the node $N$, we must have
$\gamma_{N}^{+}+\gamma_{N}^{-}=L^{N}$. Note that this representation of
$\gamma_{N}$ allows us to work with the usual definition of monotone real
circuits and not deal with the case where a function is non-increasing in an
input variable.

For every node $N$ of $T^{\prime}$, let $\operatorname{anc}(N)$ denote the set
of proper ancestors of $N$ (i.e., excluding $N$). Then define

$\displaystyle\mathcal{V}(N)\coloneqq\mathcal{V}^{+}(N)\cup\mathcal{V}^{-}(N)\coloneqq$
$\displaystyle\hphantom{\cup~{}}\left\\{\gamma_{M}^{+}~{}\Big{|}~{}\text{
\parbox{180.00027pt}{$M\in\operatorname{anc}(N)$ and~{}$N$ is in the subtree
rooted at the $\alpha_{M}^{\top}x\geq\gamma_{M}+1$-child of~{}$M$} }\right\\}$
$\displaystyle\cup\left\\{\gamma_{M}^{-}~{}\Big{|}~{}\text{
\parbox{180.00027pt}{$M\in\operatorname{anc}(N)$ and~{}$N$ is in the subtree
rooted at the $\alpha_{M}^{\top}x\leq\gamma_{M}$-child of~{}$M$} }\right\\}$

and

$\mathcal{U}(N)\coloneqq\\{\gamma_{M}^{-},\gamma_{M}^{+}~{}|~{}M\text{
internal node of $T^{\prime}$ and descendant of }N\\}.$

For this definition, we consider $N$ as a descendant of $N$. See Figure 2(b)
for an example.

Then, for the sake of induction, we strengthen the statement of the theorem
to:

######  Claim.

For every node $N$ of $T^{\prime}$, there exists a monotone real circuit
$C_{N}$ of size $\lvert T^{\prime}(N)\rvert\cdot 2(\lvert
T^{\prime}\rvert+n_{3})\cdot\log(L+1)^{\log\lvert T^{\prime}(N)\rvert}$, which
receives as inputs values for the variables $\mathcal{Z}\cup\mathcal{V}(N)$,
where $\mathcal{Z}\coloneqq\\{z_{1},\dots,z_{n_{3}}\\}$ and decides whether
there exist values for the variables $\mathcal{U}(N)$, which obey
$\gamma_{N}^{+}+\gamma_{N}^{-}=L^{N}$ and choosing

$\displaystyle\gamma_{N}\coloneqq L^{N}_{\min}+\gamma_{N}^{+}$
$\displaystyle\forall\,\gamma^{+}_{N}\in\mathcal{U}(N)\cup\mathcal{V}^{+}(N)\quad\text{and}$
$\displaystyle\gamma_{N}\coloneqq L^{N}_{\max}-\gamma_{N}^{-}$
$\displaystyle\forall\,\gamma^{-}_{N}\in\mathcal{V}^{-}(N)$

turns every $f^{L}$ attached to a leaf $L$ in the corresponding subtree
$\tilde{T}^{P}(\gamma)(N)$ rooted at $N$ in $\tilde{T}^{P}(\gamma)$ into a
valid quasi-Farkas-certificate for $L$ in the branch-and-bound tree
$\tilde{T}^{P}(\gamma)$ for $P(z)$ relative to $[0,1]^{n_{1}}$.

Note that $\gamma$ is only partially defined by the definition given in the
claim; however, all entries of $\gamma$ which are relevant for the validity of
the quasi-Farkas-certificates in $\tilde{T}^{P}(\gamma)(N)$ are defined.

It suffices to show the claim, since then $C\coloneqq C_{r}$ (where $r$
denotes the root of $T^{\prime}$) decides whether there exists a branch-and-
bound tree $(\tilde{T})^{P}$ for $P(z)$ conforming to $\tilde{T}$ and hence
separates $Z_{1}$ and $Z_{2}$.

We begin by noting that for every input $\gamma_{M}^{\pm}$ of such a circuit
$C_{N}$ corresponding to the right-hand-side of the disjunction used at a node
$M$ in $\mathcal{V}(N)$, we have $C_{N}(z,\tilde{\gamma},L^{M})=1$ for all
$(z,\tilde{\gamma})\in\mathds{R}^{\mathcal{Z}\cup(\mathcal{V}(N)\setminus\gamma_{M}^{\pm})}$,
since then the side of the disjunction at $M$ which corresponds to the branch
containing $N$ does not intersect $[0,1]^{n_{1}}$ and hence all vectors
attached to leaves in $\tilde{T}^{P}(\gamma)(N)$ are valid quasi-Farkas-
certificates.

We prove the claim via induction on $\lvert\tilde{T}(N)\rvert$. If
$\lvert\tilde{T}(N)\rvert=1$, then $N$ is a leaf. Hence,
$\mathcal{U}(N)=\emptyset$ and since we are given values for all variables
from $\mathcal{Z}\cup\mathcal{V}(N)$, we are given all right-hand-sides to the
subproblem
$\tilde{T}^{P}(\gamma)_{N}(P(z))\eqqcolon\\{x\in\mathds{R}^{n_{1}}~{}|~{}Ex\leq
e\\}$ associated to the leaf $N$ of the tree $\tilde{T}^{P}(\gamma)$ for
$P(z)$. We have to test whether $f^{N}$ is a valid quasi-Farkas-certificate.
To this end, it suffices to test if $(f^{L})^{\top}e<0$, since we have
$(f^{L})^{\top}E=0$, because $T^{\prime}$ is a valid certified branch-and-
bound tree for $P(z)\times Q(z)$ (see the proof of Lemma 8). Note that
$\tilde{T}^{P}(\gamma)_{N}(P(z))$ contains constraints which are also
contained in $P(z)$ and are indexed with numbers $i\in[m_{1}]$ and constraints
of the form $\alpha_{M}^{\top}x\geq\gamma_{M}+1$ or
$\alpha_{M}^{\top}x\leq\gamma_{M}$ coming from branching, which we will index
with the node $M$ at which they appear in a disjunction. We then calculate:

$\displaystyle(f^{L})^{\top}e$
$\displaystyle=\sum_{i\in[m_{1}]}f^{N}_{i}(a_{i}-C_{i}z)+\sum_{\gamma^{+}_{M}\in\mathcal{V}^{+}(N)}f^{N}_{M}(-L^{M}_{\min}-\gamma^{+}_{M}-1)+\sum_{\gamma^{-}_{M}\in\mathcal{V}^{-}(N)}f^{N}_{M}(L^{M}_{\max}-\gamma_{M}^{-})$
$\displaystyle\eqcolon
k^{N}-\sum_{\tau\in\mathcal{Z}\cup\mathcal{V}(N)}s^{N}_{\tau}\cdot\tau,$

where $C_{i}$ is the $i$-th row of $C$ and the second line is defined by
aggregating variables and constants. We note that the resulting $s^{N}_{\tau}$
are non-negative (recall $C$ is non-negative). Evidently, the sum in the
second line can be computed by a monotone real circuit with inputs
corresponding to the elements of $\mathcal{Z}\cup\mathcal{V}(N)$ and
$\lvert\mathcal{Z}\cup\mathcal{V}(N)\rvert-1$ further gates by iteratively
adding summands. Note that adding $s^{N}_{\tau}$ times the first input to the
second input is a monotone operation, since $s^{N}_{\tau}$ is non-negative. By
post-composing the function applied at the output gate with the function
sending numbers larger than $k^{N}$ to $1$ and numbers at most $k^{N}$ to $0$,
we obtain a monotone real circuit $\hat{C}_{N}$ that decides whether $f^{N}$
is a Farkas-certificate.

We modify $\hat{C}_{N}$ to obtain a monotone real circuit $C_{N}$ which
decides whether $f^{N}$ is a quasi-Farkas-certificate as follows: For every
gate $g$ in $\hat{C}_{N}$ which adds $s^{N}_{\tau}$-times the value of an
input $\gamma_{M}^{+}\in\mathcal{V}(N)$ (or $\gamma_{M}^{-}$) to our sum, we
modify the function applied at this gate such that it adds a very large
constant $K^{N}$ instead, if $\gamma_{M}^{+}\geq L_{M}$ ($\gamma_{M}^{-}\geq
L_{M}$). By our definition of $L_{M}$ and $\gamma_{M}$, this is the case if
and only if the side of the disjunction at the node $M$ corresponding to the
subtree of $M$ containing $N$, does not intersect $[0,1]^{n_{1}}$, which makes
$f^{N}$ a valid quasi-Farkas-certificate relative to $[0,1]^{n_{1}}$ by
definition. Hence, if we choose $K^{N}$ sufficiently large, such that $C_{N}$
will certainly accept in this case, for example $K^{N}\coloneqq k^{N}+1$, then
$C_{N}$ correctly decides whether $f^{N}$ is a valid quasi-Farkas-certificate.
Moreover, $C_{N}$ satisfies the claimed bound on its size.

If $\lvert T^{\prime}(N)\rvert>1$, we appeal to Corollary 10: Let $N_{\leq}$
and $N_{\geq}$ denote the children of $N$. Then, by the induction hypothesis,
there exist circuits $C_{N_{\leq}}$ and $\smash{C_{N_{\geq}}}$ for these nodes
as in the claim. Since
$\mathcal{V}(N_{\leq})=\mathcal{V}(N)\cup\\{\gamma_{N}^{-}\\}=(\mathcal{V}(N_{\geq})\setminus\\{\gamma_{N}^{+}\\})\cup\\{\gamma_{N}^{-}\\}$
and
$\smash{C_{N_{\leq}}(z,\tilde{\gamma},L^{N})=C_{N_{\geq}}(z,\tilde{\gamma},L^{N})}=1$
for all
$(z,\tilde{\gamma})\in\smash{\mathds{R}^{\mathcal{Z}\cup\mathcal{V}(N)}}$, we
may apply Corollary 10 to $C_{N_{\leq}}$ and $C_{N_{\geq}}$ (with
$\smash{\Lambda_{\max}=L^{N}}$, $\Lambda_{\min}=0$ and $\kappa=L^{N}$), in a
way which invokes the larger circuit only once.

To see that $C_{N}$ is no larger than claimed, assume the subtree
$T^{\prime}(N_{\leq})$ of $T^{\prime}$ rooted at $N_{\leq}$ is smaller than
the one rooted at $N_{\geq}$, the other case is analogous. Hence,
$T^{\prime}(N_{\leq})$ has size at most $\lvert T^{\prime}(N)\rvert/2$ while
$T^{\prime}(N_{\geq})$ has size at most $\lvert T^{\prime}(N)\rvert-1$. Then,
compute

$\displaystyle\lvert C_{N}\rvert$ $\displaystyle\leq\lvert
C_{N_{\leq}}\rvert\cdot(\lceil\log(L^{N}+1)\rceil)+\lvert C_{N_{\geq}}\rvert$
$\displaystyle\leq\lvert T^{\prime}(N_{\leq})\rvert\cdot 2(\lvert
T^{\prime}\rvert+n_{3})\cdot(\lceil\log(L+1)\rceil)^{\log(\lvert
T^{\prime}(N)\rvert/2)}\cdot(\lceil\log(L^{N}+1)\rceil)$
$\displaystyle\phantom{\leq}+\lvert T^{\prime}(N_{\geq})\rvert\cdot 2(\lvert
T^{\prime}\rvert+n_{3})\cdot(\lceil\log(L+1)\rceil)^{\log(\lvert
T^{\prime}(N)\rvert-1)}$ $\displaystyle\leq\lvert
T^{\prime}(N_{\leq})\rvert\cdot 2(\lvert
T^{\prime}\rvert+n_{3})\cdot(\lceil\log(L+1)\rceil)^{\log\lvert
T^{\prime}(N)\rvert}$ $\displaystyle\phantom{\leq}+\lvert
T^{\prime}(N_{\geq})\rvert\cdot 2(\lvert
T^{\prime}\rvert+n_{3})\cdot(\lceil\log(L+1)\rceil)^{\log\lvert
T^{\prime}(N)\rvert}$ $\displaystyle\leq\lvert T^{\prime}(N)\rvert\cdot
2(\lvert T^{\prime}\rvert+n_{3})\cdot(\lceil\log(L+1)\rceil)^{\log\lvert
T^{\prime}(N)\rvert}.$

Finally, set $C\coloneqq C_{r}$ for the circuit $C_{r}$ given by the claim for
the root node $r$ of $T^{\prime}$ and note
$\lceil\log(L+1)\rceil=\lceil\log(n(10n^{2})^{(n+2)^{2}}+3)\rceil$ as well as
$\lvert T^{\prime}\rvert\leq(4n+5)\lvert T\rvert$. Hence $C_{r}$ has size at
most

$\displaystyle\lvert T^{\prime}(r)\rvert\cdot 2(\lvert
T^{\prime}\rvert+n_{3})\cdot(\lceil\log(L+1)\rceil)^{\log\lvert
T^{\prime}(r)\rvert}$ $\displaystyle\leq(4n+5)\lvert T\rvert\cdot
2[(4n+5)\lvert T\rvert+n]\cdot[(n+2)^{2}\log(10n^{3}+3)]^{\log((4n+5)\lvert
T\rvert)}$ $\displaystyle\leq 2(5n+5)^{2}\lvert
T\rvert^{2}\cdot[(n+2)^{2}\log(10n^{3}+3)]^{\log((4n+5)\lvert T\rvert)}$
$\displaystyle\leq 50(n+1)^{2}\lvert
T\rvert^{2}\cdot[(n+2)^{2}\log(10n^{3}+3)]^{\log((4n+5)\lvert T\rvert)}.\qed$

The computations bounding the circuit size in the recursive step are taken
from Fleming et al. [11] where they are used to show that branch-and-bound
with really small coefficients can be quasi-polynomially simulated by cutting
planes. A very similar recursive formula already appears in [5], where it is
used to show that branch-and-bound for variable disjunctions is quasi-
automatizable.

###### Proof of Theorem 4.

Assume that we have a family of branch-and-bound trees $T$ for (2), one for
each $r$, such that $\smash{\lvert T\rvert\in 2^{O(n^{1/6-\epsilon})}}$ for
some $\epsilon>0$. Then Theorem 3 gives rise to a family of circuits $C_{n}$
separating the CC-pair of size

$\displaystyle\lvert C_{n}\rvert$ $\displaystyle=50(n+1)^{2}\lvert
T\rvert^{2}\cdot[(n+2)^{2}\log(10n^{3}+3)]^{\log((4n+5)\lvert T\rvert)}$
$\displaystyle=50(n+1)^{2}2^{2O(n^{1/6-\epsilon})}\cdot\left(2^{\log[(n+2)^{2}\log(10n^{3}+3)]}\right)^{\log(4n+5)O(n^{1/6-\epsilon})}$
$\displaystyle=2^{O(n^{1/6-\epsilon})}\cdot
2^{\log[(n+2)^{2}\log(10n^{3}+3)]\cdot\log(4n+5)O(n^{1/6-\epsilon})}$
$\displaystyle=2^{O(n^{1/6-\epsilon})}\cdot 2^{O(n^{\epsilon/2})\cdot
O(n^{1/6-\epsilon})}=2^{O(n^{1/6-\epsilon})}\cdot
2^{O(n^{1/6-\epsilon/2})}=2^{O(n^{1/6-\epsilon/2})}.$

Since we have $n=n_{1}+n_{2}+n_{3}=r\lfloor\frac{1}{8}(r/\log
r)^{2/3}\rfloor+r+(r^{2}-r)/2$ and $n_{3}=r+(r^{2}-r)/2$ we have

$1\leq\frac{n}{n_{3}}=1+\frac{O(r^{5/3})}{\Omega(r^{2})}$

Since $n\rightarrow\infty$ implies $r\rightarrow\infty$, we have
$n_{3}\in\Theta(n)$. But then we have

$\lvert C_{n}\rvert\in
2^{O(n^{1/6-\epsilon/2})}=2^{O(n_{3}^{1/6-\epsilon/2})},$

which contradicts Theorem 2. ∎

## References

  * [1] Alon, N., Boppana, R.B.: The monotone circuit complexity of Boolean functions. Combinatorica 7, 1–22 (1987). doi:10.1007/bf02579196
  * [2] Basu, A., Conforti, M., Di Summa, M., Jiang, H.: Complexity of branch-and-bound and cutting planes in mixed-integer optimization – II. Combinatorica 42(1), 971–996 (Dec 2022). doi:10.1007/s00493-022-4884-7
  * [3] Beale, E., Forrest, J.: Global optimization using special ordered sets. Mathematical Programming 10, 52–69 (1976). doi:10.1007/bf01580653
  * [4] Beame, P., Fleming, N., Impagliazzo, R., Kolokolova, A., Pankratov, D., Pitassi, T., Robere, R.: Stabbing planes. In: Karlin, A.R. (ed.) 9th Innovations in Theoretical Computer Science Conference (ITCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol. 94, pp. 10:1–10:20. Schloss Dagstuhl, Germany, Dagstuhl, Germany (2018). doi:10.4230/LIPIcs.ITCS.2018.10
  * [5] Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: Proceedings of 37th Conference on Foundations of Computer Science (FOCS). pp. 274–282. IEEE (1996). doi:10.1109/sfcs.1996.548486
  * [6] Bonet, M., Pitassi, T., Raz, R.: Lower bounds for cutting planes proofs with small coefficients. The Journal of Symbolic Logic 62(3), 708–728 (1997). doi:10.2307/2275569
  * [7] Dadush, D., Tiwari, S.: On the complexity of branching proofs. In: Saraf, S. (ed.) 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 169, pp. 34:1–34:35. Schloss Dagstuhl, Germany (2020). doi:10.4230/LIPIcs.CCC.2020.34
  * [8] Dantchev, S., Galesi, N., Ghani, A., Martin, B.: Depth lower bounds in stabbing planes for combinatorial principles. In: Berenbrink, P., Monmege, B. (eds.) 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 219, pp. 24:1–24:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2022). doi:10.4230/LIPIcs.STACS.2022.24
  * [9] Derpich, I., Vera, J.R.: Improving the efficiency of the branch and bound algorithm for integer programming based on “flatness” information. European Journal of Operational Research 174(1), 92–101 (2006). doi:10.1016/j.ejor.2005.02.051
  * [10] Dey, S.S., Dubey, Y., Molinaro, M.: Lower bounds on the size of general branch-and-bound trees. Mathematical Programming pp. 1–21 (2022). doi:10.1007/s10107-022-01781-z
  * [11] Fleming, N., Göös, M., Impagliazzo, R., Pitassi, T., Robere, R., Tan, L.Y., Wigderson, A.: On the power and limitations of branch and cut. In: Kabanets, V. (ed.) 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 200, pp. 6:1–6:30. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2021). doi:10.4230/LIPIcs.CCC.2021.6
  * [12] Fleming, N., Pankratov, D., Pitassi, T., Robere, R.: Random $\theta(\log n)$-CNFs are hard for cutting planes. J. ACM 69(3) (jun 2022). doi:10.1145/3486680
  * [13] Gläser, M., Pfetsch, M.E.: On computing small variable disjunction branch-and-bound trees. Mathematical Programming pp. 1–29 (2023). doi:10.1007/s10107-023-01968-y, to appear
  * [14] Grötschel, M., Lovász, L., Schrijver, A.: Geometric algorithms and combinatorial optimization. Springer, Berlin (1988)
  * [15] Haken, A., Cook, S.A.: An exponential lower bound for the size of monotone real circuits. Journal of Computer and System Sciences 58(2), 326–335 (1999). doi:10.1006/jcss.1998.1617
  * [16] Hrubeš, P., Pudlák, P.: Random formulas, monotone circuits, and interpolation. In: 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS). pp. 121–131. IEEE (2017). doi:10.1109/focs.2017.20
  * [17] Kaibel, V., Weltge, S.: Lower bounds on the sizes of integer programs without additional variables. Mathematical Programming 154(1), 407–425 (2015). doi:10.1007/s10107-014-0855-0
  * [18] Krajiček, J.: Lower bounds to the size of constant-depth propositional proofs. The Journal of Symbolic Logic 59(1), 73–86 (1994). doi:10.2307/2275250
  * [19] Krajíček, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic 62(2), 457–486 (1997). doi:10.2307/2275541
  * [20] Lenstra, H.W.: Integer programming with a fixed number of variables. Mathematics of Operations Research 8(4), 538–548 (1983). doi:10.1287/moor.8.4.538
  * [21] Mahmoud, H., Chinneck, J.W.: Achieving MILP feasibility quickly using general disjunctions. Computers & Operations Research 40(8), 2094–2102 (2013). doi:10.1016/j.cor.2013.03.001
  * [22] Ostrowski, J., Linderoth, J., Rossi, F., Smriglio, S.: Orbital branching. Mathematical Programming 126, 147–178 (2011). doi:10.1007/s10107-009-0273-x
  * [23] Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic 62(3), 981–998 (1997). doi:10.2307/2275583
  * [24] Pudlák, P.: On reducibility and symmetry of disjoint NP pairs. Theoretical Computer Science 295(1-3), 323–339 (2003). doi:10.1016/s0304-3975(02)00411-5
  * [25] Razborov, A.A.: Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic. Izvestiya: mathematics 59(1), 205 (1995). doi:10.1070/im1995v059n01abeh000009
  * [26] Wegener, I.: The complexity of Boolean functions. John Wiley & Sons, Inc. (1987)