A proof system for certifying symmetry and optimality reasoning in integer programming
Extracted source text · arXiv 2311.03877
\documentclass[runningheads]{llncs}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[english]{babel}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{mathtools}
\usepackage{nicefrac}
\usepackage{graphicx}
\usepackage{xcolor}
\usepackage{dsfont}
\usepackage{todonotes}
\definecolor{darkred}{RGB}{150, 0, 0}
\definecolor{darkgreen}{RGB}{0, 150, 0}
\definecolor{darkblue}{RGB}{0, 0, 150}
\usepackage[breaklinks=true,colorlinks,citecolor=darkgreen,linkcolor=darkred,urlcolor=darkblue,bookmarks=false]{hyperref}
\usepackage{cleveref}
\Crefname{theorem}{Thm.}{Thms.}
\Crefname{proposition}{Prop.}{Props.}
\Crefname{lemma}{Lem.}{Lems.}
\Crefname{section}{Sec.}{Secs.}
\Crefname{appendix}{Sec.}{Secs.}
\Crefname{definition}{Def.}{Defs.}
\usepackage{enumerate}
\usepackage{tikz}
\usepackage{booktabs}
\usepackage[inline]{enumitem}
\usepackage{xspace}
\usepackage{subcaption}
\usepackage[binary-units=true]{siunitx}
%\usepackage{siunitx} % arxiv fix: enable binary units
\usepackage{cite}
\renewcommand\UrlFont{\color{blue}\rmfamily}
\usepackage{listings}
\lstset{language=Pascal}
\newcommand{\JD}[2][]{\todo[color=orange!20,#1,size=tiny]{JD: #2}}
\newcommand{\JDil}[1]{\JD[inline]{#1}}
\newcommand{\CH}[2][]{\todo[color=blue!20,#1,size=tiny]{CH: #2}}
\newcommand{\CHil}[1]{\CH[inline]{#1}}
\newcommand{\AG}[2][]{\todo[color=green!20!yellow,#1,size=tiny]{AG: #2}}
\newcommand{\AGil}[1]{\AG[inline]{#1}}
\newcommand{\GENERAL}[1]{\todo[color=red!20,size=tiny]{#1}}
\newcommand{\SPACE}[1]{\todo[color=white,size=tiny,textcolor=black!50,bordercolor=black!50]{#1}}
\newcommand{\LE}[2][]{\todo[color=red!40!yellow,#1,size=tiny]{LE: #2}}
\newcommand{\LEil}[1]{\LE[inline]{#1}}
\newcommand{\reals}{\ensuremath{\mathds{R}}}
\newcommand{\Q}{\ensuremath{\mathds{Q}}}
\newcommand{\integers}{\ensuremath{\mathds{Z}}}
\newcommand{\transpose}{\ensuremath{^{\top}}}
\newcommand{\feasregion}{\ensuremath{F}\xspace}
\newcommand{\initcore}{\ensuremath{\mathcal{F}}\xspace}
\newcommand{\relaxedregion}{\ensuremath{\mathrm\Psi}}
\newcommand{\define}{\ensuremath{\coloneqq}}
\newcommand{\scip}{{\tt SCIP}\xspace}
\newcommand{\etal}{et~al.\@\xspace}
\newcommand{\binary}{\ensuremath{\{0, 1\}}}
\newcommand{\symretope}{\ensuremath{\mathcal{X}}\xspace}
\newcommand{\coNP}{\ensuremath{\mathrm{coNP}}}
\newcommand{\NP}{\ensuremath{\mathrm{NP}}}
\newcommand{\bnbtree}{\ensuremath{\mathcal T}\xspace}
\newcommand{\bnbnodes}{\ensuremath{V}\xspace}
\newcommand{\bnbedges}{\ensuremath{E}}
\newcommand{\stab}[2]{\mathrm{stab}(#1, #2)}
\newcommand{\STAB}[2]{\mathrm{STAB}(#1, #2)}
\newcommand{\id}{\ensuremath{\mathrm{id}}}
\newcommand{\ihat}{\ensuremath{\hat\imath}}
\newcommand{\bigo}{\ensuremath{\mathop{\mathcal{O}}}}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\eqreffromto}[2]{(\ref{#1}\nobreakdash--\ref{#2})}
\newcommand{\domain}{\ensuremath{\mathcal{D}}}
\newcommand{\domainrestr}{\ensuremath{\mathcal{D}'}}
\newcommand{\optprob}{\ensuremath{\mathrm{OPT}(f, \feasregion)}\xspace}
\DeclareMathOperator{\supp}{supp}
% constraints
\newcommand{\powset}{\ensuremath{\mathcal{P}}}
\newcommand{\core}{\ensuremath{\mathcal{C}}\xspace}
\newcommand{\derived}{\ensuremath{\mathcal{D}}\xspace}
\newcommand{\derive}{\derived}
\newcommand{\assumed}{\ensuremath{\mathcal{A}}\xspace}
% symmetry
\newcommand{\sym}[1]{\ensuremath{\mathcal{S}_{#1}}}
\newcommand{\perm}{\gamma}
\newcommand{\rowperm}{\pi}
\newcommand{\group}{\Gamma}
\newcommand{\inv}[1]{{#1}^{-1}}
\newcommand{\invperm}{\inv{\perm}}
\newcommand{\orb}[2]{\mathrm{orb}_{#1}\left(#2\right)}
% general math
\newcommand{\T}{^T}
\newcommand{\sprod}[2]{{#1}\T{#2}}
\newcommand{\isomorphismpruning}{IsoPr\xspace}
\newcommand{\orbitalfixing}{OF\xspace}
\newcommand{\SHC}{SHC\xspace}
\newcommand{\SHCs}{\SHC{}s\xspace}
\newcommand{\VDR}{VDR\xspace}
\newcommand{\VDRs}{\VDR{}s\xspace}
\newcommand{\lexfix}{LexFix\xspace}
\newcommand{\lexred}{LexRed\xspace}
\newcommand{\bb}{B\&{}B\xspace}
\newcommand{\bnb}{\bb}
\newcommand{\ie}{i.e.,\xspace}
\newcommand{\eg}{e.g.,\xspace}
\newcommand{\implication}{\rightsquigarrow}
\newcommand{\parent}{\mathop{\delta^{-}}\nolimits}
\newcommand{\children}{\mathop{\delta^{+}}\nolimits}
\newcommand{\firstcommonancestor}{\mathop{\rm fcanc}}
\newcommand{\dcn}{\mathop{\rm dcn}}
\newcommand{\repr}{\mathop{\rm repr}\nolimits}
\newcommand{\bradec}{\ensuremath{\mathcal B}}
\newcommand{\bnbdec}{\ensuremath{B}}
\newcommand{\bnbroot}{r}
\newcommand{\emptylist}{(\,)}
\newcommand{\Cconsistent}{\mbox{$\mathcal{C}$-consistent}\xspace}
\newcommand{\solleaf}{\mathop{\rm leaf}}
\newcommand{\lexgeq}{\succeq}
\newcommand{\stricteps}{\epsilon}
\newcommand{\tgeq}[1][\bnbtree]{\succeq_{\stricteps,#1}}
\newcommand{\lexgt}{\succ}
\newcommand{\lexgteps}{\succ_\stricteps}
\newcommand{\tgt}{\succ_{\stricteps,\bnbtree}}
\newcommand{\prenorm}[1]{\lVert #1 \rVert}
\newcommand{\primbound}{z}
\newcommand{\config}{\ensuremath{\mathfrak{C}}\xspace}
\newcommand{\configdef}{\big(%
\core,
\derived,
g,
\primbound,
\bnbtree,
\stricteps
\big)}
\newcommand{\complem}[1]{\overline{#1}}
\newcommand{\length}[1]{\overbracket[0.5pt][1pt]{#1}}
\newcommand{\sgeq}{\trianglerighteq}
\newcommand{\sleq}{\trianglelefteq}
\newcommand{\TRUE}{\ensuremath{\rm\text{\scshape True}}\xspace}
\newcommand{\FALSE}{\ensuremath{\rm\text{\scshape False}}\xspace}
\newcommand{\card}[1]{|#1|}
\newcommand{\restrict}[2]{
\ensuremath{
#1
\raisebox{-.1ex}{\ensuremath{\big\rvert}}{}_{\smash{#2}}
}}
\newcommand{\concat}{\ensuremath{\mathbin\Vert}}
\newcommand{\with}{\ensuremath{\!\mathop{\restriction}\nolimits}}
\newcommand{\blank}{\ensuremath{\_}}
\newcommand{\red}[1]{\color{red}{#1}}
\newcommand{\mysubsubsection}[1]{
\paragraph{#1}
}
\DeclareMathOperator{\conv}{conv}
\DeclareMathOperator{\proj}{proj}
\DeclareMathOperator{\nmin}{nmin}
\DeclareMathOperator{\lexmin}{lexmin}
\DeclareMathOperator{\lexmax}{lexmax}
\DeclareMathOperator{\sign}{sgn}
\newcommand{\down}[1]{\left\lfloor #1 \right\rfloor}
\newcommand{\up}[1]{\lceil #1 \rceil}
\newcommand{\ourparagraph}[1]{%
\medskip
\noindent\emph{#1}
}
\begin{document}
\title{A proof system for certifying symmetry and optimality reasoning
in integer programming
\thanks{The work for this article has been conducted within the Research Campus Modal funded by the German Federal Ministry of Education and Research (BMBF grant numbers 05M14ZAM, 05M20ZBM).}}
\titlerunning{A proof system for certifying symmetry and optimality reasoning}
\author{Jasper van Doornmalen\inst{1} \and
Leon Eifler\inst{2} \and
Ambros Gleixner\inst{2,3} \and
Christopher Hojny\inst{1}
}
\authorrunning{J.\ van Doornmalen et al.}
\institute{TU Eindhoven, The Netherlands,
\email{\{m.j.v.doornmalen,c.hojny\}@tue.nl}
\and Zuse Institute Berlin, Germany,
\email{eifler@zib.de}
\and HTW Berlin, Germany,
\email{gleixner@htw-berlin.de}
}
\maketitle
\begin{abstract}
We present a proof system for establishing the correctness of results produced by
optimization algorithms, with a focus on mixed-integer programming (MIP).
%
Our system generalizes the seminal work of Bogaerts, Gocht, McCreesh, and Nordström
(2022) for binary programs to handle any additional difficulties arising from unbounded
and continuous variables,
%
and covers a broad range of solving techniques, including
symmetry handling, cutting planes, and presolving reductions.
%
Consistency across all decisions that affect the feasible region is achieved by a pair
of transitive relations on the set of solutions, which relies on the newly introduced
notion of consistent branching trees.
%
Combined with a series of machine-verifiable derivation rules,
%
the resulting framework offers practical solutions to enhance the trust in integer
programming as a methodology for applications where reliability and correctness are key.
\end{abstract}
% \GENERAL{Maybe check the use of all $\cap$ in things like $\bigcap(\core \ldots )$}
\section{Introduction}
\label{sec:intro}
% \begin{itemize}
% \item Set up general problem
% \item Motivate proof-logging in general
% \item Explain missing features of VIPR
% \item Describe contribution
% \item Explain structure of paper
% \end{itemize}
In this paper, we are concerned with general optimization problems of the form
$\optprob \define \min\{ f(x) : x \in \feasregion \}$
for a real-valued function~$f\colon \reals^n \to \reals$
and a feasible region~$\feasregion \subseteq \reals^n$ %, where $\feasregion$ is
defined by a set of constraints.
%
In particular, we are interested in the solution of mixed-integer programs (MIPs) to
optimality, for which state-of-the-art algorithms are composed of a large array
of different solving techniques~\cite{NemhauserWolsey1988,Achterberg2007,ConfortiCornuejolsZambelli2014,AchterbergBixby2019,HojnyPfetsch2019}. %AG{some citations would be good}.
%
Though their correctness is proven \emph{on paper}, with today's tools it seems
prohibitively difficult to verify that they are implemented correctly \emph{in complex
software}.
%
In fact, there have been recurring reports of incorrect results in different types of solvers~\cite{Brummayer_Lonsing_Biere2010,Cook_et_al2013,Akgun2018MetamorphicTO,GillardSD2019}.
%% Although theoretically possible, formally verifying such complex algorithms is unrealistic in practice.
%
Instead of verifying correctness of an implementation, a more viable approach is to supplement the computed result with a \emph{proof of correctness}~\cite{McConnellMehlhornEtAl2011,AlkassarEtAl2011} that % is printed as a certificate file along the final solution and that
can be independently and automatically verified. This approach has long been the standard in the SAT community~\cite{HeuleHuntWetzler2014,Cruz-FilipeHeuleEtAl2017,Cruz-FilipeMarquesEtAl2017,Goldberg2003}, but there also exist proof-logging mechanisms for broader classes of problems such as in SMT solving~\cite{de2008proofs,BarbosaEtal2022}, pseudo-boolean optimization~\cite{Gocht_2019_veripb,ElffersGochtMcCreeshNordstrom_2020}, or exact MIP~\cite{VIPR}.
For MIP, no formal proof system has been developed to this date, and the solving techniques that are certifiable in~\cite{VIPR} are severely limited, not covering any methods that remove parts of the feasible region from the search space, \eg due to symmetry arguments. A seminal paper in this direction is~\cite{bogaerts2023certifiedsymbr}, which describes a proof system to handle symmetry- and redundancy-based reasoning for pseudo-boolean optimization.
%
Our work follows the same paradigm to develop a proof system that addresses the challenges
posed by the presence of unbounded and continuous variables.
%
As a result, we can certify the correctness of a wide range of static and dynamic, global and local symmetry handling methods, and many other state-of-the-art techniques from the MIP literature.
The overall strategy is to define a \emph{configuration} as a snapshot of the derivations during the solving process.
%
A trivial starting configuration is iteratively updated by a series of \emph{rules} that are proven to establish valid derivations, eventually certifying optimality or infeasibility of \optprob.
%
To that end, in \Cref{sec:proofsystem} we introduce the notion of a \emph{consistent branching tree}, which is used to prevent inconsistencies among all derivations that remove parts of the feasible region and to define \emph{validity} of a configuration.
%
Vaguely speaking, any valid configuration admits the same optimal objective value as \optprob.
%
In \Cref{sec:rules}, we present a set of validity-preserving transition rules that make it possible to certify optimality or infeasibility \emph{sequentially}.
%
In \Cref{sec:realization}, we illustrate the framework for many MIP-techniques within LP-based branch-and-bound
%, e.g., symmetry handling, cutting planes, or presolving,
and discuss how certificates could be encoded and verified in practice. We conclude with an outlook in \Cref{sec:outlook}.
% The structure of this paper is as follows. In \cref{sec:proofsystem} we introduce an abstract proof system, and prove results about validity and optimality. In \cref{sec:rules} we present a series of update rules that \emph{preserve} validity of a configuration. In \cref{sec:realization} we present a concrete realization of the abstract framework and show how many of the algorithmic techniques in MIP can be certified in our new proof system.
% A \emph{constraint} is a subset of~$\reals^n$.
% For a set of constraints $\mathcal C$,
% denote $\bigcap \mathcal C \define
% \bigcap_{C \in \mathcal C} C$.
% Likewise, denote $\bigcup \mathcal C \define \bigcup_{C \in \mathcal C} C$.
% This general setting describes constraint programs,
% In this paper, we build a proof system for certifying
% for optimization problems whether they are infeasible,
% or whether solutions with a given objective value exist.
% The certificate of optimality or infeasibility
% is given by a sequence of so-called configurations
% related to the optimization problem.
% If certain conditions for the configuration hold, then we call the configuration \emph{valid}.
% Starting with an initial valid configuration,
% a series of validity-preserving transitions are reported in the \emph{proof log}.
% Eventually, this leads to a valid final configuration for the optimization problem.
% The purpose is, that from validity of this final configuration,
% optimality or infeasibility of the optimization problem is apparent.
% Each step of the proof log must be machine-verifiable,
% so that a verifier can confirm the claimed optimality or infeasibility
% of~\optprob.
% To that end, we inform the verifier of certain \emph{rules},
% which are classes of possible validity-preserving transitions.
%
% Our core contribution is verifiability of symmetry handling reductions.
% To this end, we introduce the notion of \emph{symmetries}
% for optimization problems.
% \begin{definition}
% A bijective map $\gamma \colon \reals^n \to \reals^n$
% is a \emph{symmetry} of \optprob
% if, for any $x \in \reals^n$
% \begin{enumerate*}[label=(\roman*)]
% \item $f(x) = f(\gamma(x))$, and
% \item $x \in \feasregion$ if and only if $\gamma(x) \in \feasregion$.
% \end{enumerate*}
% \end{definition}
% The set of all symmetries of an optimization problem defines a group.
% For the purpose of symmetry handling in this paper, it is not required
% to work with the full symmetry group of the optimization problem.
% Rather, the group properties of symmetries is used,
% e.g., that symmetries can be composed to find new symmetries.
% We address the problem of verifiability of symmetries later.
% In~\cite{doornmalen2023unified}, we show how symmetries can be
% handled in a branch-and-bound setting in the following way.
% At a branch-and-bound tree node, one could propagate that the solutions
% sought for are maximal among their symmetric counterparts,
% where for maximality a particular partial lexicographic ordering is considered.
% In particular, in this work, the ordering can be a different ordering
% in different parts of the branch-and-bound tree,
% which is called a \emph{dynamic variable ordering}.
% Regarding handling symmetries in a machine-verifiable way,
% Bogaerts \etal~\cite{bogaerts2023certifiedsymbr} present a different
% way to handle symmetries, where a variable ordering
% for the lexicographic comparisons is also chosen dynamically,
% but this variable ordering is chosen at a global level.
% \todo[inline]{Idea of Ambros: Mention that we can handle symmetry locally, and that's not done before.}
\section{Trees, Configurations, and Validity}
\label{sec:proofsystem}
The central ingredient of our proof system, as in \cite{bogaerts2023certifiedsymbr}, is a
reflexive and transitive relation on the solution space that defines a consistent
direction for symmetry handling and optimality-based reductions.
%
While in \cite{bogaerts2023certifiedsymbr} this preorder remains mostly abstract, we
provide a concrete construction designed to resolve the additional difficulties
introduced by the presence of continuous and unbounded variables, and to capture the
degrees of freedom due to locality in a branch-and-bound process.
%
We require the following notational conventions.
In the abstract setting of \Cref{sec:proofsystem,sec:rules}, we consider constraints to be
arbitrary subsets $C\in\powset(\reals^n)$, the power set of $\reals^n$;
%
$\complem{C} = \reals^n \setminus C$ denotes its complement.
%
For a set of constraints $\core\subseteq\powset(\reals^n)$, we write $\bigcap\core$ as a
shorthand for $\bigcap_{C\in\core}C$.
%
For $\tau = (i_1, \dots, i_{k})\in\{\pm
1,\ldots,\pm n\}^{k}$, we define by slight abuse of notation % the mapping
\[ \tau\colon\reals^n\to\reals^k, \tau(x) \define \big( \sign(i_1)\,x_{|i_1|}, \dots, \sign(i_{k})\,x_{|i_{k}|} \big), \]
where $\sign(\cdot)$ denotes the sign function,
and $\tau(C) \define \{ \tau(x) : x \in C \}$ for $C \subseteq \reals^n$.
%
We write $\tau \sleq \tau' = (i'_1, \dots, i'_{k'})$
if $i_j=i'_j$ for all $1\leq j \leq k \leq k'$.
% if $k\leq k'$ and $i_j=i'_j$ for all $j \in [k]$.
%
% The set of children of a node $v$ in a directed graph is denoted by~$\children(v)$.
We write~$\children(v)$ for the set of children of a node $v$ in a directed graph, and $[a] \define \{j \in \integers_+ : j \leq a \}$.
\begin{definition}
%% AG: I still thinking that we should avoid the term branching:
%% \Cconsistent tree partition? because essentially $\bnbtree$ is
%% (i.e. its leaves are) a partition of $\reals^n$ with a strong
%% structure endowed by the tree
Let $\core\subseteq\powset(\reals^n)$,
then we call $\bnbtree = (\bnbnodes, \bnbedges, \bnbdec, \sigma)$
a \emph{\Cconsistent branching tree}
if the following conditions hold:
\begin{enumerate}[label={(T\arabic*)}, ref={T\arabic*},left=0pt]
%% AG: Notational convention: u parent, v,w children
%% AG: No mathcal for sets of nodes and arcs; reserve mathcal for sets of sets.
\item
\label{consistent:arborescence}
$(\bnbnodes, \bnbedges)$ is an arborescence with $1 \leq \card{\bnbnodes} < \infty$
and root $\bnbroot\in\bnbnodes$.
\item
\label{consistent:branching}
Each~$v \in \bnbnodes$ has attached a branching constraint $\bnbdec_v \subseteq \reals^n$, and $\bnbdec_\bnbroot = \reals^n$.
\item
\label{consistent:covering}
For all $u \in \bnbnodes$ with $\children(u) \neq \emptyset$ we have
$\bigcap\core \subseteq \bigcup_{v \in \children(u)} \bnbdec_v$.
% i.e., the feasible region of $u$ is covered by the feasible regions of its children.
\item
\label{consistent:dupl}
Each~$v \in \bnbnodes$ has attached a % an ordered removed for line break reasons
list $\sigma_v\in\{\pm 1,\ldots,\pm n\}^{\ell_v}$, $\ell_v \in \{0,1,\ldots,n\}$,
of signed variable indices
without duplicates in $|(\sigma_v)_1|,\ldots,|(\sigma_v)_{\ell_v}|$.
\item
\label{consistent:growing}
For all $u \in \bnbnodes$, $v \in \children(u)$,
we have $\sigma_u \sleq \sigma_v$.
\item
\label{consistent:bounded}
%% AG: Let's have an explicit point about boundedness and not hide it in {consistent:dupl}.
%% I removed \bounded to minimize notation; was not used later.
For all $v \in \bnbnodes$ and $i\in[\ell_v]$,
we have
$
\max\{ \sigma_v(x)_i : x \in \bigcap \core \} < \infty.
$
\item
\label{consistent:packing}
For all $u\in\bnbnodes$ and $v,w \in \children(u)$, $v\not=w$, we have
%% \[
%% \sigma_u\big(\bigcap (\core \cup \bradec_{v})\big)
%% \cap
%% \sigma_u\big(\bigcap (\core \cup \bradec_{w})\big)
%% =\emptyset.
%% \]
$
\sigma_u(\bnbdec_v) \cap \sigma_u(\bnbdec_w) = \emptyset
$.
\end{enumerate}
\end{definition}
%
For a node~$u \in \bnbnodes$ with~$\children(u) \neq \emptyset$,
\eqref{consistent:covering} and~\eqref{consistent:packing} ensure that
the children of $u$ partition the feasible region of $u$;
%
in particular, for every~$x \in \bigcap\core$, there is a unique leaf
of~$(\bnbnodes,\bnbedges)$ whose feasible region contains~$x$, denoted
by $\solleaf(x)$, see \Cref{lemma:uniquechild,lemma:uniqueleaf} in
\Cref{sec:auxresults}.
% \LE{should we turn all such refrences into Crefs?}
%
Hence, for~$x,y\in\bigcap\core$, there exists a \emph{deepest
common node}~$w\eqqcolon\dcn(x,y)$ with $x$ and $y$ both contained in
the feasible region of $w$.
%
% AG: Calling it partitioning instead of packing, because I believe
% that this is clearer for some readers.
The partitioning condition~\eqref{consistent:packing} is stronger and
further implies that all $u\in V$ with $|\children(u)|\geq 2$ have
nontrivial $\sigma_u$.
%
By~\eqref{consistent:growing}, also all successors $v$ have
$\ell_v\geq \ell_u\geq 1$.
%
The boundedness condition~\eqref{consistent:bounded} holds if all
variables contained in at least one $\sigma_v$ have finite upper
(lower) bound if contained with positive (negative) index.
%
%% W.l.o.g. we may assume that all nodes, including the root, have either zero or at least two children.
%% AG: I wanted to write something like ``Leaf nodes~$v$ of parent~$u$ will typically have $\sigma_v=\sigma_u$, but this is not enforced by the definition.'' How is this? Does it make sense to have $\ell_v > \ell_u$? I can imagine that you may view $v$ as a new root node and add symresacks or apply symmetry-based presolving/propagation techniques.
%% CH: In my opinion it doesn't make sense that~$\ell_v > \ell_u$, but it
%% also doesn't hurt because we nowhere make use of~$\sigma_v$ if~$v$ is a leaf.
%% AG: Agreed, it does not make a difference in the current setting. But if we choose ``$\sigma_{v}(x) \lexgeq \sigma_{v}(y) \text{ if } v=\solleaf(x)=\solleaf(y)$'' and ``$\sigma_{v}(x) \lexgteps \sigma_{v}(y) \text{ if } v=\solleaf(x)=\solleaf(y)$'' in the definitions below, then it would influence the comparisons and could be used to apply additional reductions at the leaves. Maybe best to discuss this in a call. It does not change anything for the rest of the paper, so I implemented it now: leaves are compared according to their sigma. This simplifies the definition, because we do not anymore need a case distinction.
\Cref{lem:preorder} in \Cref{sec:auxresults} shows that the relations~$\tgeq$ and $\tgt$
defined next constitute a preorder resp. a strict order on the set of solutions
in~$\bigcap\core$:
%% One can show that~$\tgeq$ defines a preorder and $\tgt$ defines a strict
%% order on~$\bigcap\core$, see \Cref{lem:preorder} in the appendix.
%
\begin{definition}
\label{def:constree}
Let $\bnbtree$ be a \Cconsistent branching tree, $\stricteps > 0$, and~$x, y \in \reals^n$.
%
Let~$\lexgeq$ and $\lexgteps$ denote the standard resp.~a strict lexicographic order given by
\vspace{-1.5ex}
\begin{align*}
x \lexgeq y :\Leftrightarrow\;
&x=y \lor x_i > y_i \text{ for the smallest index $i$ with $x_i\not=y_i$},\\
%\intertext{and let $\lexgteps$ denote a strict lexicographic order defined by}
x \lexgteps y :\Leftrightarrow\;
&x\not=y \land x_i \geq y_i + \stricteps \text{ for the smallest index $i$ with $x_i\not=y_i$}.
\shortintertext{Using $v=\dcn(x,y)$, we then define the relations $\tgeq$ and $\tgt$ over $\bigcap\core$ by}
x \tgeq y :\Leftrightarrow\;
&\sigma_{v}(x) = \sigma_{v}(y) \lor \sigma_{v}(x) \lexgteps \sigma_{v}(y),\\
x \tgt y :\Leftrightarrow\;
&\sigma_{v}(x) \lexgteps \sigma_{v}(y).
\end{align*}
%where $v=\dcn(x,y)$.
\end{definition}
%
With this, we arrive at the following central notion of a \emph{configuration}:
\begin{definition}
\label{def:validconf}
Let $\core,\derived\subseteq\powset(\reals^n)$, $g\colon\reals^n \to \reals, z \in \reals \cup \{\infty\}, \epsilon > 0$,
%
and let $\bnbtree$\! be a branching tree.
A configuration $\configdef$ is called \emph{$(\feasregion, f)$-valid} if:
%the following conditions hold:
\begin{enumerate}[label={(V\arabic*)}, ref={V\arabic*},left=0pt]
\item
\label{cond:consistent}
$\bnbtree$ is \Cconsistent and $\stricteps > 0$.
\item
\label{cond:obj}
If $\primbound < \infty$, there exists an $x \in \feasregion$ with $f(x) \leq \primbound$.
\item
\label{cond:feasC}
% AG: I changed the ' to \hat, because ' is used in many of the rules.
For all $\hat\primbound < \primbound$,
there exists an $x \in \feasregion$
with~$f(x) \leq \hat\primbound$
if and only if
there exists an~$x \in \bigcap\core$
with~$g(x) \leq \hat\primbound$.
\item
\label{cond:derive}
For every $x \in \bigcap\core$ with $g(x) < \primbound$, there exists a $y \in \bigcap (\core \cup \derived)$ with $y \tgeq x$ and $g(y) \leq g(x)$.
\end{enumerate}
\end{definition}
%
As in \cite{bogaerts2023certifiedsymbr}, we call $\core$ the set of \emph{core} and
$\derived$ the set of \emph{derived constraints}.
%
\Cref{thm:goalconfig} states that the goal---to produce a valid configuration containing the
contradiction $\emptyset\in\derived$---yields a certificate of optimality (if
$z < \infty$) or infeasibility (if $z=\infty$).
%
While it seems out of reach to produce such a configuration and check its validity in one
step, \Cref{thm:initvalid} provides a trivially valid starting configuration~$\config^0$.
%
A proof in our system then becomes a \emph{sequence of valid configurations} starting
at~$\config^0$ and transitioning to richer configurations by iteratively applying a set of
\emph{machine-verifiable rules} that are \emph{proven to preserve validity} in~\Cref{sec:rules}.
\begin{theorem}
\label{thm:goalconfig}
Let $\configdef$ be an $(\feasregion, f)$-valid configuration with~$\emptyset \in
\derived$.
%
Then there exists no solution $x \in \feasregion$ with $f(x) < \primbound$.
\end{theorem}
\begin{proof}
Suppose there is an $(\feasregion, f)$-valid configuration
$\configdef$ with $\emptyset \in \derived$, and $x \in \feasregion$ with
$f(x) = \hat\primbound < \primbound$.
%
By~\eqref{cond:feasC}, there is~$\hat x \in \bigcap\core$ with $g(\hat x) \leq
\hat\primbound < \primbound$, and by~\eqref{cond:derive}, there exists a $y \in
\bigcap(\core \cup \derived)$.
%
This contradicts~$\bigcap(\core \cup \derived) \subseteq \bigcap\derived = \emptyset$.
%
\qed
% For the sake of contradiction, let us consider an $(\feasregion, f)$-valid configuration
% $\configdef$ with $\emptyset \in \derived$, while there is an $x \in \feasregion$ with
% $f(x) = \hat\primbound < \primbound$.
% %
% By~\eqref{cond:feasC}, there exists an~$\hat x \in \bigcap\core$ with $g(\hat x) \leq
% \hat\primbound < \primbound$, and by~\eqref{cond:derive}, there exists a $y \in
% \bigcap(\core \cup \derived)$.
% %
% This contradicts~$\bigcap(\core \cup \derived) \subseteq \bigcap\derived = \emptyset$.
% %
% \qed
\end{proof}
\begin{theorem}
\label{thm:initvalid}
Let $\initcore\subseteq\powset(\reals^n)$, $F = \bigcap\initcore$, and
\mbox{$f\colon\reals^n\to\reals$}.
%
Then the \emph{initial configuration} $\config^0\define\big(\initcore, \emptyset, f, \infty, (\{\bnbroot\},
\emptyset, \{\bnbroot\mapsto\reals^n\}, \{\bnbroot\mapsto\emptylist\}),1\big)$ is
$(\feasregion, f)$-valid.
\end{theorem}
\begin{proof}
\eqref{cond:obj} holds due to $\primbound = \infty$ and
%
\eqref{cond:feasC} because~$\bigcap\core = \bigcap\initcore =
\feasregion$ and $g=f$.
%
Since $\derived=\emptyset$, we can always choose $y=x$ to satisfy \eqref{cond:derive}.
%
Finally, the initial tree~$(\{\bnbroot\}, \emptyset, \{\bnbroot\mapsto\reals^n\},
\{\bnbroot\mapsto\emptylist\})$ consists only of a root node~$\bnbroot$ with
$\bnbdec_r=\reals^n$ and empty $\sigma_r = \emptylist$.
%
This tree trivially conforms to \Cref{def:constree}, and $\epsilon=1>0$.
%
\qed
\end{proof}
\section{Validity-Preserving Transition Rules}
\label{sec:rules}
The first two rules feature a special type of constraint called an
\emph{implication}.
%In the first two rules, we make use of a special type of constraint called an
%\emph{implication}.
%
Let $\assumed\subseteq\powset(\reals^n)$ be a collection of \emph{assumptions} and $C\subseteq
\reals^n$, then we define $[\assumed \implication C] \define
\complem{\bigcap \assumed} \cup C$, \ie $x \in [\assumed \implication C]$ if and only if $(\, x
\in \bigcap \assumed \Rightarrow x \in C\, )$. \linebreak In particular, any constraint $C$ can be written as
the implication $[\reals^n \implication C]$.
% We still maintain the new notation for implications, for two reasons. First, it will be necessary in the concrete realization of the abstract framework in \cref{sec:application}. Second, it is more illustrative in the abstract proof system since it helps to distinguish between assumptions and derived constraints, which play different roles in the certificate.
\ourparagraph{Implicational derivation rule.}
%
This first rule allows to derive constraints that preserve
all feasible, improving solutions in a subset of $\reals^n$, i.e., under a (possibly
empty) set of assumptions $\assumed$:
%
\begin{theorem}
\label{thm:implic}
Let $\configdef$ be an $(\feasregion, f)$-valid configuration.
%
Let $C\subseteq\reals^n$ and $\assumed\subseteq\powset(\reals^n)$.
%
Then $\big( \core, \derived \cup \{[\assumed \implication C]\}, g, \primbound, \bnbtree,
\stricteps \big)$ is also $(\feasregion, f)$-valid, if
\begin{align}
\label{cond:implic}
C \supseteq \bigcap (\core \cup \derived \cup \assumed)
\cap
\{ x \in \reals^n : g(x) < \primbound \}.
\end{align}
\end{theorem}
\ourparagraph{Resolution rule.}
%
A particular form of the implicational derivation rule allows to
derive new constraints by a disjunctive argument.
\begin{corollary}
\label{cor:resolution}
Let $\configdef$ be an $(\feasregion, f)$-valid configuration.
%
Consider sets $A_1$,$A_2$,$C_1$,$C_2\subseteq\reals^n$,
and let $\assumed_1,\assumed_2$
be sets of constraints with
\begin{equation}
\label{cond:resolution}
\left[\left(\assumed_1 \cup \{A_1\}\right) \implication C_1\right],
\left[\left(\assumed_2 \cup \{A_2\}\right) \implication C_2\right]
\in\core\cup\derived
\,\land\,
A_1 \cup A_2 \supseteq \bigcap(\core\cup\derived).
\end{equation}
Then $\big( \core, \derived \cup \{ \left[(\assumed_1 \cup \assumed_2) \implication (C_1 \cup C_2)\right] \}, g, \primbound, \bnbtree,
\stricteps \big)$ is also $(\feasregion, f)$-valid.
\end{corollary}
%
A typical example for resolution is the case where
$\assumed_1=\assumed_2$ contains the branching decisions up to a parent node
in a search tree with exactly two children, and $C_1=C_2$ is a constraint
derived previously for both children.
%
%% \SPACE{Optional sentence: Note that this corresponds to the \emph{unsplitting rule} in \cite{VIPR}.}
\ourparagraph{Objective bound update rule.}
%
When an improving solution is known, this rule allows to update the value of $z$ in a
configuration:
\begin{theorem}
\label{thm:objbound}
Let $\configdef$ be an $(\feasregion, f)$-valid configuration and
$x\in\bigcap\core$ with $g(x) = \primbound' < \primbound$.
%
Then $\big( \core, \derived, g, \primbound', \bnbtree, \stricteps \big)$ is also
$(\feasregion, f)$-valid.
\end{theorem}
\ourparagraph{Objective function update rule.}
%
If the constraints imply equations, it may be desirable to substitute variables and update
the objective function accordingly:
%
% This is allowed by the following rule:
%% AG: I don't know how to prove it with the weaker condition $\{ x \in \reals^n :
%% g'(x) = g(x) \} \supseteq \bigcap \core$, but it somehow makes sense that you would need
%% to include the reasons for the update in $\core$ because it affects symmetry/witness
%% definition.}
\begin{theorem}
\label{thm:objfunc}
Let $\configdef$ be an $(\feasregion, f)$-valid configuration and
$g'\colon \reals^n\to\reals^n$.
%
If
$
%
%\begin{align}
%\label{cond:objfunc}
\bigcap \core \subseteq \{ x \in \reals^n : g'(x) = g(x) \},
%\end{align}
$
then $\big( \core, \derived, g', \primbound, \bnbtree, \stricteps \big)$ is also
$(\feasregion, f)$-valid.
\end{theorem}
\ourparagraph{Redundance-based strengthening rule.}
%
The implicational derivation rule allows the removal of suboptimal solutions only once
$\primbound < \infty$ has been established by the objective bound update rule.
%
The following rule allows the removal of feasible solutions
independently of the objective bound if a so-called \emph{witness}
$\omega$ is known:
\begin{theorem}
\label{thm:redundance}
Let $\config=\configdef$ be an $(\feasregion, f)$-valid configuration and let $C \subseteq
\reals^n$.
%
If there exists an $\omega\colon\reals^n\to\reals^n$ such that
\begin{equation}
\label{eq:redruleimp}
\begin{aligned}
x \in \bigcap (\core \cup \derived)
\land
x\not\in C
\Rightarrow
\;\omega(x) \in \bigcap (\core \cup \derived \cup \{C\})
\;\land&\;\\
\omega(x) \tgeq x
\;\land&\;
g(\omega(x)) \leq g(x)
\end{aligned}
\end{equation}
holds for all $x\in\reals^n$,
%
then $\big( \core, \derived \cup \{C\}, g, \primbound, \bnbtree,
\stricteps \big)$ is also $(\feasregion, f)$-valid.
\end{theorem}
\begin{proof}
% Replacing~$\derive$ by~$\derive \cup \{C\}$ keeps
\eqref{cond:consistent},
\eqref{cond:obj}, and~\eqref{cond:feasC} are invariant.
%
To show that also~\eqref{cond:derive} continues to hold,
%
let~$x \in \bigcap\core$ with~$g(x) < z$.
%
We need to prove that there is a~$y \in \bigcap(\core\cup\derive\cup\{C\})$ with~$y
\tgeq x$ and~$g(y) \leq g(x)$.
%
By \eqref{cond:derive} for \config, there is~$x' \in \bigcap(\core\cup\derive)$
with~$x' \tgeq x$ and~$g(x') \leq g(x)$.
%
If~${x'\in C}$, we can choose $y=x'$.
%
Otherwise, choose $y=\omega(x')$.
%
Then \eqref{eq:redruleimp} guarantees that
$
y \in \bigcap (\core \cup \derived \cup \{C\})
$,
$y \tgeq x' \tgeq x$,
and $g(y) \leq g(x') \leq g(x)$.
%
By transitivity of $\tgeq$, this concludes the proof.
%
\qed
\end{proof}
\ourparagraph{Dominance-based strengthening rule.}
%
\Cref{thm:redundance} %Redundance-based strengthening
is limited to cases where a single witness can repair
removed solutions in one step such that they satisfy all core and
derived constraints at once. The next rule allows more complex reasoning:
\begin{theorem}
\label{thm:dominance}
Let $\config=\configdef$ be an $(\feasregion, f)$-valid configuration and let $C \subseteq \reals^n$.
%
If there exists an $\omega\colon\reals^n\to\reals^n$ such that
\begin{equation}
\label{eq:symruleimp}
\begin{aligned}
x \in \bigcap (\core \cup \derived)
\land
x\not\in C
\Rightarrow
\;\omega(x) \in \bigcap\core
\;\land\;
\;\omega(x) \tgt x
\;\land\;
g(\omega(x)) \leq g(x)
\end{aligned}
\end{equation}
holds for all $x\in\reals^n$,
%
then $\big( \core, \derived \cup \{C\}, g, \primbound, \bnbtree,
\stricteps \big)$ is also $(\feasregion, f)$-valid.
\end{theorem}
%
\begin{proof}
Note that adding~$C$ to~$\derive$ keeps \eqref{cond:consistent}, \eqref{cond:obj},
and~\eqref{cond:feasC} invariant.
To prove that~\eqref{cond:derive} holds if one
replaces~$\derive$ by~$\derive' = \derive \cup \{C\}$,
let~$x^0 \in \bigcap\core$ with~$g(x^0) < z$.
We need to show that there is~$y \in \bigcap(\core\cup\derive')$
with~$y \tgeq x^0$ and~$g(y) \leq g(x^0)$.
We establish this by creating a (potentially infinite) sequence~$(x^i)_{i = 1}^k$ with
\[
x^i \define
\begin{cases}
y^i, & \text{if } i \text{ is odd for some~$y^i$
from~\eqref{cond:derive} for~$x=x^{i-1}$ in~$\config$},\\
\omega(x^{i-1}), & \text{if~$i$ is even},
\end{cases}
\]
where~$k = \inf\{i \in \integers_+ : x^i \in
\bigcap(\core\cup\derive\cup\{C\})\}$.
%
This sequence is well-defined, which can be shown via induction by alternatingly applying~\eqref{cond:derive} and~\eqref{eq:symruleimp}.
It suffices to prove~$k < \infty$ as the alternating application
of~\eqref{cond:derive} and~\eqref{eq:symruleimp}
guarantees~$x^k \tgeq x^{k-1} \tgeq \dots \tgeq x^0$
and~$g(x^k) \leq g(x^{k-1}) \leq \dots \leq g(x^0)$, so we can choose $y=x^k$.
%
To show finiteness, first note that~\eqref{cond:derive} and~\eqref{eq:symruleimp} imply
\[
x^{2i}
\tgt
x^{2i-1}
\tgeq
x^{2i-2}
\tgt
\dots
\tgeq
x^2
\tgt
x^1
\tgeq
x^0
\]
for all~$i \in [\nicefrac{k}{2}] = \{j\in\integers_+:j \leq \nicefrac{k}{2}\}$.
Thus, \Cref{lem:doubleTrans} in the appendix shows $x^{2i} \tgt
x^{2i-2}$ for all~$i \in [\nicefrac{k}{2}]$,
i.e., for each~$i \in [\nicefrac{k}{2}]$, there is a~$u_i \in \bnbnodes$
with~$\sigma_{u_i}(x^{2i}) \lexgteps \sigma_{u_i}(x^{2i-2})$.
For the sake of contradiction, suppose~$k = \infty$.
Since~$V$ in $\bnbtree$ is finite, also $\{\sigma_v : v \in
\bnbnodes\}$ is finite.
Transitivity of~$\tgt$ and~$k = \infty$ then implies that there
exists~$u \in \bnbnodes$ and a subsequence~$(x^{i_j})_{j = 1}^\infty$
with~$\sigma_u(x^{i_{j+1}}) \tgt \sigma_u(x^{i_j})$
and\linebreak $i_{j+1} > i_j\in 2\integers$ for all $j\in\integers_+$.
%
% Each~$x^{i_j}=\omega(x^{i_j-1})$.
%
Hence, for all~$j \in \integers_+$, there is~$t_j \in [\ell_u]$ such
that
\[
\sigma_u(x^{i_{j+1}})_{t_j} \geq \sigma_u(x^{i_j})_{t_j} + \stricteps
\,\land\,
\sigma_u(x^{i_{j+1}})_s = \sigma_u(x^{i_j})_s
\text{ for all } s \in [t_j-1].
\]
Since~$\ell_u$ is finite, there exists an index~$t$
that infinitely often determines the lexicographic difference.
Among all such indices~$t$, let~$t'$ be the smallest one.
By \eqref{consistent:bounded}, all entries in~$\sigma_u(x)$, $x\in\bigcap\core$, are
bounded from above.
%
Hence, there must exist infinitely many~$j$
with~$\sigma_u(x^{i_{j+1}})_{t'} < \sigma_u(x^{i_j})_{t'}$;
%% AG: I believe infinitely many decreases of $\stricteps/2$ would suffice, e.g.
otherwise, we would have $\lim_{j\to\infty} \sigma_u(x^{i_j})_{t'} = \infty$.
%
For all such $j$, due to~$\sigma_u(x^{i_{j+1}}) \tgt
\sigma_u(x^{i_j})$, there must exist $s \in [t'-1]$ with
$\sigma_u(x^{i_{j+1}})_s \geq \sigma_u(x^{i_j})_s + \stricteps$.
%
This is a contradiction to~$t'$ being minimal.
Consequently, $k < \infty$.
This concludes the proof.
\qed
\end{proof}
%
In comparison to redundance-based strengthening, dominance-based
strengthening is both weaker in the sense that $\omega(x)$ does not
need to satisfy $\derived$ and $C$ directly, and stricter in the sense that
$\omega$ must result in an increase w.r.t. the strict order~$\tgt$.
%
Note that in both rules, $C$ may be an implication $[\assumed \implication
C]$, e.g., a locally valid symmetry-breaking constraint for some node $v\in\bnbnodes$.
%% AG: keep thinking about the right name; not sure how shrinking/shrinkage sounds to a native speaker, and googling gives me some negative connotations; tightening because it allows you to derive tighter constraints; epsilon weakening would allude to the weakening of the dominance and redundance rules; reduction would be most precise, but boring; update is too generic; decrease?
\ourparagraph{Epsilon shrinkage rule.}
%
The presence of $\stricteps$ in \eqref{cond:derive} ensures consistent progress in
the proof of \Cref{thm:dominance}.
%
It needs to be fixed for each dominance-based strengthening, but intermediately, $\stricteps$ can be decreased to an
arbitrarily small, positive value:
\begin{theorem}
\label{thm:epsupdate}
Let $\configdef$ be an $(\feasregion, f)$-valid configuration.
%
If $0 < \stricteps' < \stricteps$, then $\big( \core, \derived, g,
\primbound, \bnbtree, \stricteps' \big)$ is also $(\feasregion,
f)$-valid.
\end{theorem}
\ourparagraph{Transfer rule.}
%
Derived constraints can be upgraded to core constraints. % at any point.
%
This may restrict future applications of dominance-based strengthening, but can be useful to
facilitate an objective function update or the tree exchange rule below:
\begin{theorem}
\label{thm:transfer}
Let $\configdef$ be an $(\feasregion, f)$-valid configuration and let
$C\in\derived$.
%
Then $\big( \core \cup \{ C\}, \derived \setminus \{ C\}, g, \primbound, \bnbtree,
\stricteps \big)$ is also $(\feasregion, f)$-valid.
\end{theorem}
\ourparagraph{Deletion rule.}
%
%% This rule allows to remove derived constraints and core constraints that can be certified
%% to be redundant:
This rule allows to remove derived and redundant core constraints:
\begin{theorem}
\label{thm:delete}
Let $\configdef$ be an $(\feasregion, f)$-valid configuration, let
$\core'\subseteq\core$ and $\derived'\subseteq\derived$.
%
Then $\big( \core', \derived', g, \primbound, \bnbtree, \stricteps \big)$ is also
$(\feasregion, f)$-valid, if %it holds that
\begin{enumerate*}[label=(\alph*)]
\item $\core'=\core$, or
% AG: I avoid the concrete rule here, because that involves assumptions and C is not
% the finally derived constraint
\item \mbox{$\core' = \core \setminus \{ C \}$} for %some constraint
$C\supseteq\bigcap\core'$,
or
\item \mbox{$\core' = \core \setminus \{ C \}$},\! $\sigma_v=\emptylist$ for all $v\in\bnbnodes$,\! %in $\bnbtree$
and $C\subseteq\reals^n$ is derivable from %configuration
% $\config^\emptyset=
$\big(\core', \emptyset, g, z, \bnbtree, \stricteps \big)$ by redundance-based
strengthening.
\end{enumerate*}
\end{theorem}
\ourparagraph{Tree exchange rule.}
%
The preorder $\tgeq$ based on the tree $\bnbtree$ is essential in
guaranteeing that a valid configuration cannot contain contradictory
derivations across different applications of redundance- or
dominance-based strengthening.
%
The following rule allows to install a new tree before any constraints
have been derived, or when all derived constraints have been deleted
or transferred to \core:
%% (according to \Cref{thm:transfer} or \Cref{thm:delete}):
\begin{theorem}
\label{thm:treeexchange}
Let $\big( \core, \emptyset, g, \primbound, \bnbtree, \stricteps
\big)$ be an $(\feasregion, f)$-valid configuration and let
$\bnbtree'$ be a \Cconsistent branching tree.
%
Then $\big( \core, \emptyset, g, \primbound, \bnbtree', \stricteps
\big)$ is also $(\feasregion, f)$-valid.
\end{theorem}
%% \ourparagraph{Sigma refinement and node refinement rule.}
%% %
%% The tree exchange rule closely resembles the order change rule of
%% \cite{bogaerts2023certifiedsymbr}.
%% %
%% However, the necessity to clear the set of derived constraints
%% beforehand is quite restrictive in light of a dynamically
%% evolving branch-and-bound process.
%% %
%% Hence, we prove two additional rules that allow to certify that a refinement of the
%% preorder-defining tree preserves validity:
%% % AG: I can imagine a version where you can extend the sigma at inner
%% % nodes, if all their children have the same sigma extension already
%% % present, but that would be an overkill for the conference version of
%% % the paper.
%% \begin{theorem}
%% \label{thm:sigmarefine}
%% Let $\config=\configdef$ be an $(\feasregion, f)$-valid configuration
%% with $\bnbtree=(V,E,B,\sigma)$ and choose
%% %% a leaf $u\in V$, $\children(u)=\emptyset$, with $\sigma_u$ of length~$\ell_u$.
%% %% %
%% %% Let $\bnbtree'=(V,E,B,\sigma')$
%% a leaf $u\in V$, $\children(u)=\emptyset$, with $\sigma_u=(i_1,\ldots,i_{\ell_u})$.
%% %
%% Let $\bnbtree'=(V,E,B,\sigma')$
%% with $\sigma'_v = \sigma_v$ for all~$v\in V\setminus\{u\}$
%% and $\sigma'_u = (i_1,\ldots,i_{\ell_u},j)$ satisfying \eqref{consistent:dupl} and \eqref{consistent:bounded}.
%% %
%% If there exists an $\omega\colon\reals^n\to\reals^n$ such that
%% \begin{subequations}
%% \begin{align}
%% \label{cond:sigmarefine:a}
%% %x \in \bigcap (\core \cup \bradec_u) \setminus \bigcap \derived
%% x \in \bigcap (\core \cup \bradec_u)
%% &\,\land\,
%% x \not\in \bigcap \derived
%% \,\land\,
%% y \in \bigcap (\core \cup \bradec_u \cup \derived)
%% \,\land\,
%% g(y) \leq g(x) < z\\
%% \label{cond:sigmarefine:b}
%% %% &\,\land\,
%% %% \sigma_u(y) = \sigma_u(x)
%% %% \,\land\,
%% %% \sigma'_u(y)_{\ell_u+1} \not= \sigma'_u(x)_{\ell_u+1}
%% %% \,\land\,
%% %% \sigma'_u(y)_{\ell_u+1} < \sigma'_u(x)_{\ell_u+1} + \stricteps\\
%% &\,\land\,
%% \sigma_u(y) = \sigma_u(x)
%% \,\land\,
%% y_{j} \not= x_{j}
%% \,\land\,
%% \sign(j) y_{|j|} < \sign(j) x_{|j|} + \stricteps\\
%% \label{cond:sigmarefine:c}
%% &\Rightarrow
%% \,\omega(y) \in \bigcap (\core \cup \derived)
%% \,\land\,
%% g(\omega(y)) \leq g(x)
%% \,\land\,
%% \omega(y) \tgeq[\bnbtree'] x
%% \end{align}
%% \end{subequations}
%% holds for all $x,y\in\reals^n$,
%% %
%% then $\config'=\big( \core, \derived, g, \primbound, \bnbtree', \stricteps
%% \big)$ is also $(\feasregion, f)$-valid.
%% \end{theorem}
%% %
%% Due to $x\not\in\bigcap\derived$ in~\eqref{cond:sigmarefine:a}, the above holds when
%% $\derived=\emptyset$ or $\bigcap\derived\supseteq\bigcap(\core\cup\bradec_u\cup\{g(x)<z\})$.
%% %
%% Hence, together with node refinement below, this rule clearly allows to create a
%% nontrivial preorder as long as no redundance- or dominance-based strengthening has been
%% used.
%% %
%% The conditions in~\eqref{cond:sigmarefine:b} express that
%% $y\tgeq x$ holds, but not $y\tgeq[\bnbtree'] x$, in which case $\omega$ is provided to
%% certify \eqref{cond:derive} holds also for $\bnbtree'$.
%% \begin{theorem}
%% \label{thm:noderefine}
%% Let $\config=\configdef$ be an $(\feasregion, f)$-valid configuration with
%% $\bnbtree=(V,E,B,\sigma)$.
%% %
%% Choose a leaf $u\in V$, $\children(u)=\emptyset$, and
%% $\bnbdec_{v_1},\ldots,\bnbdec_{v_k}\subseteq\reals^n$
%% for nodes $v_1,\ldots,v_k\not\in\bnbnodes$
%% such that
%% $\sigma_u(B_{v_1}),\ldots,\sigma_u(B_{v_k})$ are pairwise disjoint and
%% $\bigcap\core\subseteq\bigcup_{i=1}^k B_{v_i}$.
%% %
%% Let $\bnbtree'=(V',E',B',\sigma')$ with
%% $\bnbnodes'=\bnbnodes\cup\{v_1,\ldots,v_k\}$,
%% $\bnbedges'=\bnbedges\cup\{(u,v_1),\ldots,(u,v_k)\}$,
%% $\bnbdec'=\bnbdec\cup\{\bnbdec_{v_1},\ldots,\bnbdec_{v_k}\}$,
%% $\sigma'_v=\sigma_v$ for all $v\in\bnbnodes$,
%% $\sigma'_{v_i}=\sigma_u$ for all $i\in[k]$.
%% %
%% Then $\config'=\big( \core, \derived, g, \primbound, \bnbtree', \stricteps
%% \big)$ is also $(\feasregion, f)$-valid.
%% \end{theorem}
\ourparagraph{Dimension extension rule.}
%
Last, but not least, the dimension of the problem can be increased by introducing new
variables that (initially) do not feature in any of the constraints,
the objective function, or the preorder-defining tree:
\begin{theorem}
\label{thm:dimext}
Let $\configdef$ be an $(\feasregion, f)$-valid configuration and let
%\linebreak
$\core' = \{ C\times\reals : C\in\core \}$,
$\derived' = \{ C\times\reals : C\in\derived \}$,
$g'\colon\reals^{n+1}\to\reals, g'(x_1,\ldots,x_{n+1})=g(x_1,\ldots,x_n)$,
and $\bnbtree' = (V,E,B',\sigma)$ with $B'_v = \bnbdec_v\times\reals$ for all $v\in V$.
%
Then $\big( \core', \derived', g', \primbound, \bnbtree',
\stricteps \big)$ is also $(\feasregion, f)$-valid.
\end{theorem}
%
This allows to create extended formulations that help to derive new
constraints, typically by redundance-based strengthening, as discussed
in the next section.
\section{Certificates for mixed-integer programs}
\label{sec:realization}
% \GENERAL{consistently use periods at end of paragraph environment}
Let (P) denote a mixed-integer program
%
$
\min \{ \sprod{c}{x} : Ax \leq b,\; x \in \integers^p \times \reals^{n-p}\},
$
%
where~$m,p,n \geq 0$ are integers,~$p \leq n$, $A \in
\Q^{m\times n}$, $b \in \Q^m$, and~$c \in \Q^n$.
%
In the following section,
we show how many popular MIP techniques can be certified within the framework of \Cref{sec:proofsystem,sec:rules}
and automatically verified.
Constraints in the abstract proof system were left to
be arbitrary subsets of~$\reals^n$.
In the MIP setting, the sets of core constraints~$\core$ and
derived constraints~$\derived$ consist of integrality restrictions on variables and linear inequalities or implications $[\mathcal A \implication C]$, where~$C$ and each $A \in \mathcal A$ is a linear inequality.
% Moreover, $\core$ contains the restriction of variables to the integers.
%
In the initial configuration of \Cref{thm:initvalid}, $\core=\initcore$ contains the rows of $Ax \le b$, as well as $x_j \in \integers$ for all $j \in [p]$.
% where the core constraint set $\core$
% consists of
% linear inequality or implications
% \JD{Or, also implications. The choice doesn't really matter},
% \LE{I don´t think we should ever have implications in the core constraints,
% I know it is possible, but why would we want to do that?}
% \JD{The rule that moves constraints from $\derived$ to $\core$ can be in the way of this!}
% \LE{Yeah, I know, I just think you would never actually apply that rule to an implication, but I will change the wording.}
% and of variable restrictions to the integers.
% The derived constraint set $\derived$
% consists of implications $[\mathcal A \implication C]$,
% where $C$ is a linear constraint,
% and $\mathcal A$ a (potentially empty) set of linear constraints.
The objective function is a linear function $f(x) = \sprod{c}{x}$.
In $\bnbtree$, the branching decisions $\bnbdec_v$, $v\in\bnbnodes$,
are also linear inequalities.
% In the following, a configuration with these
% restrictions is called
% a \emph{MIP-configuration}.\AG{this is never used, is it?}
While a configuration does not explicitly contain the value of a dual bound, it is
natural that an LP-based branch-and-bound solver would maintain in $\derived$ a set of
implications $[\assumed \implication g(x)\geq d_\assumed]$ per subproblem $\assumed$,
derived by the implicational derivation rule using aggregation of constraints with dual multipliers, and apply the resolution rule
in order to derive globally valid dual bounds from these, much like in~\cite{VIPR}.
\subsection{Presolving, Propagation, and Branch-and-Cut}
A \emph{cutting plane} for (P) is an inequality $\sprod{\alpha}{x} \le \beta$ that is valid for the feasible region of (P), while separating some infeasible point $x^*$. Cuts that are not valid globally can be represented as an implication $[\mathcal A \implication C]$, where $\mathcal{A}$ contains the local constraints for which the cut is valid. Hence, it is clear that any cutting plane can---in the abstract proof system---be certified using the implication rule presented in \Cref{thm:implic}. However, the complexity of this in general as hard as solving (P)~\cite{GroetschelLovaszShrijver1988}. Still, for a wide variety of cutting planes, efficient verification is possible if some additional information is provided.
\ourparagraph{Aggregation.} If there exist multipliers $\lambda_i \ge 0$ such that $C \equiv \sum_{i}\lambda_i C_i$ for some linear constraints $C_i$, then $C$ is redundant, and therefore the implication is trivially satisfied. It is clear that if the indices and multipliers are specified, a verifier can efficiently check that $C\equiv \sum_{i} \lambda_i C_i$ holds. If the multipliers are not specified, a verifier can solve an LP to find the correct multipliers and indices~\cite{EiflerGleixner2023}. Therefore, we can efficiently verify the validity of cuts that are derived by aggregation.
\ourparagraph{Disjunctive cuts.} A disjunctive cut is a cut $\sprod{\alpha}{x} \le \beta$ for which there exists a disjunction $(\sprod{\pi}{x} \le \pi_0) \lor (\sprod{\pi}{x} \ge \pi_0 + 1)$ such that the inequality is valid for both $\{x : Ax \le b, \sprod{\pi}{x} \le \pi_0\}$ and $\{x : Ax \le b, \sprod{\pi}{x} \ge \pi_0 +1\}$~\cite{Jereslow1977, Balas1979, CookKananShrijver1990}. Moreover, for all variables $x_i$ that are not integer $\pi_i$ is required to be $0$. The verification for this type of cut is possible if the correct disjunction is provided in the certificate, which allows for a proof by aggregation for both sides of the disjunction. Afterwards, the validity of the complete cut can be verified by applying the resolution rule, see~\cite{EiflerGleixner2023} for details.
As shown in~\cite{CournejolsLi2001}, an efficient procedure for verifying disjunctive cuts allows to verify many families of cuts including Chv\'atal-Gomory cuts~\cite{Chvatal1973}, Gomory mixed-integer cuts~\cite{Gomory1960}, mixed-integer rounding cuts\cite{NemhauserWolsey1990}, or lift-and-project cuts~\cite{BalasCeriaCournejols1993}.
In the appendix, we also provide examples for verification of simple knapsack~\cite{Balas1975} and flowcover cuts~\cite{Padberg1985}.
% \JD{Reference to Ambros' earlier work?}
\ourparagraph{Extended Formulations.} There are other types of cuts that cannot be characterized as a split cut, \eg reformulation-linearization cuts~\cite{SheraliAdams1990}. However, using the dimension extension rule in combination with conic combinations of constraints, the needed extended formulation can be produced in the certificate.
% \AG{The two sentences could be removed in my mind:
% Providing a complete list of verification techniques for all types of general-purpose cuts for MIP is beyond the scope of this paper. We believe though that the techniques presented above cover a sizable part of the most prominent ones and can serve as a guideline for strategies to verify other types of cutting planes.
% }
\ourparagraph{Presolving and Propagation.}
Presolving is a vital part of solving MIPs~\cite{AchterbergBixby2019,Savelsbergh1994,Fuegenschuh2005}, and often certifying a presolving step is straightforward. For example, if a variable bound is tightened by \emph{constraint propagation}~\cite{Savelsbergh1994}, the new variable bound can be verified by aggregation of existing constraints.
Concretely, given some constraint $\sprod{\alpha}{x} \le \beta$, and assume finite bounds on all variables $\ell_i \le x_i \le u_i, i \in [n]$, an activity-based upper bound for $x_i$ (assuming $\alpha_i > 0$) can be computed as
%\begin{equation*}
$
x_i \le \nicefrac{(\beta - \sum_{\alpha_j \ge 0, j \neq i}\alpha_j \ell_j - \sum_{\alpha_j < 0, j \neq i}\alpha_ju_j)}{\alpha_i}
$.
%\end{equation*}
An automatically verifiable proof by implicational derivation is to aggregate the original inequality $\sprod{\alpha}{x} \le \beta$ with $-\alpha_j(x_j \le u_j)$ for $\alpha_j < 0$ and with $\alpha_j(x_j \ge \ell_j)$ for $\alpha_j \ge 0$. Scaling the resulting inequality by~$1/\alpha_i$ yields a proof of the new bound. %pot
% Then, as the new bound is a valid linear combination of existing core constraints, it can be added to the core constraints. Since it is tighter than the previous bound, it is possible to delete the old constraint using the deletion rule.
Similar arguments can be made for many other presolving reductions, e.g., probing~\cite{AchterbergBixby2019}. % (aggregation in combination with adding assumptions and using the resolution rule)\CH{Replace explanation by a reference?}.
In the following, we mention several key presolving techniques that actively exclude feasible solutions of the original problem \optprob.
\ourparagraph{Reduced cost fixing.}
This core technique dates back to the seminal paper of Dantzig, Fulkerson, and Johnson on the traveling salesman problem~\cite{dantzig1954tsp}, and allows to tighten the bounds of a variable using information about the primal bound, the LP objective value, and the dual multipliers of the variable's bound constraints. Reduced cost fixing can be verified using implicational derivation (with $\primbound < \infty$), see \Cref{sec:appendix3}.
\ourparagraph{Dominated columns.}
Dominated columns presolving~\cite{GamrathKochEtAl2015,Andersen1995} fixes
a variable~$x_k$ to one of its bounds, if there is another variable $x_j$
with $c_j \le c_k$, $a_{*j} \le a_{*k}$, and $x_j$ is integer whenever $x_k$ is. If additionally local (\ie derived) constraints need to be considered,
we assume that they were added to $A\leq b$ for the sake of this paragraph. Such a fixing can be certified by the redundance-based strengthening rule. For the sake of simplicity, assume that~$x_j$ and~$x_k$ are bounded below by $0$ and that $x_j$ has no upper bound; in general, any lower bound and an implied upper bound is possible. Then, a witness is given by $\omega\colon\reals^n \to \reals^n$ with
\begin{equation*}
\omega(x)_i = \begin{cases}
x_i, &\text{if } i \notin \{j,k\}, \\
0 , &\text{if } i = k, \\
x_i+x_k , &\text{if } i = j.
\end{cases}
\end{equation*}
To verify that \eqref{eq:redruleimp} of~\Cref{thm:redundance} is satisfied for $\omega$, it is straightforward to check that $\sprod{c}{\omega(x)} \le \sprod{c}{x}$. As $a_{*j} \le a_{*j}$, holds, any constraint satisfied by~$x$ is also satisfied by~$\omega(x)$. This can be automatically verified with an aggregation proof similar as for constraint propagation. Furthermore, $\omega(x)$ trivially satisfies the new constraint $x_k = 0$. In presolving the tree $\bnbtree$ will typically be the initial tree, hence~$\omega(x)\tgeq x$ is a tautology.
% \ourparagraph{Dual fixing.}
% Let~$x_k$ be a variable with non-negative coefficients for all constraints in the current configuration, and~$c_k \geq 0$.\CH{Don't we need the derived constraints here, too?}
% \LE{yes, reworded it to avoid the matrix, but I think we should just delete dual fixing}
% In the simplest case of dual fixing, $x_k$ is fixed to its lower bound. In fact, this is a special case of a dominated column, where the dominating column is zero and has zero objective. The more advanced cases described in~\cite{AchterbergBixby2019} can be certified by a disjunctive proof, using aggregation and the previous simple case as subroutines.
\subsection{Symmetry Handling}
%% AG@CH: Here we should also show that the branching schemes admit to create $\bnbtree$
%% dynamically via sigma and node refinement: what are the witnesses?}
%% CH@AG: I am afraid that there is no simple witness.
%% The only thing that I can come up with is to have an~$\omega$ that
%% depends on~$y$. That is, for
%% the~$y$ from \Cref{thm:sigmarefine}, let~$\omega(y) = \gamma_y(y)$ for
%% some~$\gamma_y \in \Gamma$ with~$\sigma'_u(\gamma_y(y))$ is
%% lexicographically maximal in~$\{\sigma'_u(\gamma(y)) : \gamma\in \Gamma\}$.
%% If the checker is allowed to work with such an abstract function (i.e., we
%% are allowed to symbolically work with the set of formulation symmetries), it can
%% conclude that, for the old~$\sigma$, we have~$\sigma_u(\omega(y)) \lexgeq
%% \sigma_u(\gamma(\omega(y)))$ for all~$\gamma \in \Gamma$ since~$\sigma'_u$
%% extends~$\sigma_u$ and~$\omega(y)$ is lexmax.
%% Consequently, since~$y$ was feasible at~$u$, also~$\omega(y)$ must be
%% feasible at~$u$ as both have the same value w.r.t.~$\sigma_u$.
%% The checker can then verify that~$\omega(y) \tgeq y$
%% since~$\sigma'_u(\omega(y)) \lexgeq \sigma'_u(\gamma(\omega(y)))$ for
%% all~$\gamma\in\Gamma$ by assumption and thus in particular for~$\gamma = \inv{\gamma}_y$
%% finds~$\sigma'_u(\omega(y)) \lexgeq \sigma'_u(\gamma(\omega(y))) =
%% \sigma'_u(y)$.\\
%% If the checker then knows that all previous reductions have been derived by
%% the dominance-based strengthening rule for some formulation symmetry, and
%% all other reductions are not based on the dominance- or redundancy-based
%% rule, it can hypothetically verify that the extension of~$\sigma$ is
%% fine.\\
%% For binary programs, one can do better, but this might not allow to
%% always extend~$\sigma_u$:
%% For the sake of simplicitly, assume~$\sign(j) = +1$.
%% If~$\sign(j)y_{|j|} < \sign(j)x_{|j|} + \stricteps$ and~$\stricteps \leq
%% 1$, then~$y_j = 0$ and~$x_j = 1$; for~$\sign(j) = -1$, one can argue
%% analogously.
%% Let~$F^1_u$ and~$F^0_u$ be the sets of variable indices such that the
%% corresponding variables are fixed to~$1$ and~$0$, respectively, at
%% node~$u$.
%% If there exists~$\gamma\in\Gamma$ such that~$\gamma(j) \in F^0_u$ and there
%% exists~$k \in F^1_u$ such that~$\gamma(F^1_u) = (F^1_u \cup \{j\})
%% \setminus \{k\}$, then~$\sigma_u$ can be extended by~$j$.
%% We claim that selecting~$\omega = \gamma$ is a witness if branching
%% decisions are variable-branchings and all derived constraints are
%% variable fixings:\\
%% If all branching decisions are variable-branchings, then the condition
%% on~$\omega = \gamma$ ensures that~$\omega(y)$ is also feasible at~$u$.
%% Moreover, by the properties of how~$\omega$ acts on~$F^0_u$ and~$F^1_u$,
%% we have~$\sigma_u(\omega(y)) \lexgt \sigma_u(y)$.
%% Since~$\omega$ is a symmetry, also the objective remains unchanged.
%% If all derived constraints are variable fixings, then~$\omega(y)$ also
%% adheres to them by definition.
%% For general derived constraints, it's difficult though and I do not have
%% a good argument.
%% }
Let~$\perm$ be a permutation of~$[n]$.
For~$x \in \reals^n$, let~$\gamma(x) =
(x_{\invperm(1)},\dots,x_{\invperm(n)})$.
A permutation~$\perm$ is a \emph{symmetry} of a MIP~(P) if~$x \in \reals^n$ is feasible for~(P) if
and only if~$\perm(x)$ is feasible, and~$\sprod{c}{x} =
\sprod{c}{\perm(x)}$.
The symmetries of a MIP form a group~$\group$, which is a subgroup of the
symmetric group on~$[n]$, denoted by~$\sym{n}$.
Although this definition of symmetries is natural,
finding all such symmetries is NP-hard~\cite{margot2010symmetry}.
One therefore usually restricts to symmetries that keep the MIP formulation
invariant.
That is, $\perm \in \sym{n}$ is a \emph{formulation symmetry} if there
is a permutation~$\rowperm \in \sym{m}$ of the constraints such
that~$\rowperm(b) = b$, $\perm(c) = c$,
$A_{\inv\rowperm(i),\invperm(j)} = A_{i,j}$ for all~$(i,j) \in [m]
\times [n]$, and the variable types are preserved.
They have the advantage that it is easy to verify if a
pair~$(\perm,\rowperm)$ defines a formulation symmetry, i.e., we can use
them for verifying symmetry reductions.
To handle (formulation) symmetries~$\group$, many techniques have been
discussed~\cite{doornmalenhojny2022cyclicsymmetries,FischettiLiberti2012,HojnyPfetsch2019,Hojny2020,kaibel2008packing,Liberti2012a,Margot2002,Margot2003,OstrowskiAnjosVannelli2015},
and we show that four popular symmetry handling techniques can be derived via our framework:
orbital branching~\cite{OstrowskiEtAl2011}, orbitopal
reduction~\cite{BendottiEtAl2021,KaibelEtAl2011}, Schreier-Sims
cuts (SST cuts)~\cite{LibertiOstrowski2014,Salvagnin2018}, and
lexicographic order based reductions~\cite{SCIP8,Friedman2007}.
As shown in~\cite{doornmalen2023unified}, these methods are
compatible with adding constraints~$\sigma_v(x) \lexgeq
\sigma_v(\perm(x))$ for all~$\perm\in\group$ at the nodes~$v$ of a
consistent branching tree~$\bnbtree$, the entries of~$\sigma_v$ being positive.
Thus, to show that the aforementioned methods fit into our framework, it is
sufficient to derive a representation of~$\sigma_v(x) \lexgeq \sigma_v(\perm(x))$ via linear
inequalities for suitable~$\sigma_v$.
There are many degrees of freedom when building~$\sigma_v$, $v \in V$.
One can select, e.g., (a) some permutation~$\pi$ of~$[n]$ and
assign~$\sigma_v = \pi$ for all $v \in V$, or (b)~if~${v \in V \setminus \{r\}}$ arises from its parent~$u$
by branching on~$x_i$, one can extend~$\sigma_u$ by~$i$ if~$i$ is
not present in~$\sigma_u$, yet.
Approach~(a) creates globally valid symmetry handling inequalities (SHIs);
approach~(b) generates local SHIs that are adapted to the branching history, allowing
to derive reductions earlier, cf.\ the discussion in~\cite{margot2010symmetry}.
As long as the tree is \Cconsistent, all choices of~$\sigma_v$ allow to
handle symmetries.
Specialized symmetry handling methods might require a special structure
of~$\sigma_v$ though, see below.
\ourparagraph{Lexicographic order based reduction.}
A classic approach to handle symmetries is to compute only solutions being
lexicographic maximal representatives among a class of symmetric solutions.
This can be enforced by deriving reductions from the relation~$\sigma_v(x)
\lexgeq \sigma_v(\perm(x))$.
For integer variables with bounded domain contained in~$[L,U]$
of size~$D = U - L$, this relation can be linearly expressed as
%
\begin{equation}
\label{eq:FDgen}
\sum_{i = 1}^{\ell_v} (D + 1)^{\ell_v - i} \cdot \sigma_v(x)_i
\geq
\sum_{i = 1}^{\ell_v} (D + 1)^{\ell_v - i} \cdot \sigma_v(\perm(x))_i,
\end{equation}
%
see, e.g., \cite{Friedman2007}.
\Cref{prop:FD} in \Cref{sec:auxresults} shows that~\eqref{eq:FDgen} can be
derived as local constraint at node~$v$ within our framework via
dominance-based strengthening by selecting~$\omega = \perm$.
Denote the corresponding derived constraint as~$C_v^\perm = [\bradec_v
\rightsquigarrow \eqref{eq:FDgen}]$, where~$\bradec_v = \{B_u : u \text{ is a node on the $r$-$v$-path in~$\bnbtree$}\}$.
Typical reductions that are derived from~$\sigma_v(x)
\lexgeq \sigma_v(\perm(x))$ are variable fixings in the binary case
or variable bound tightenings in the integer case.
Both type of reductions can be encoded as linear constraints.
If a solver finds a lexicographic order based reduction at node~$v$,
e.g., $x_i \leq u_i$ for some~$i \in [n]$ and~$u_i \in \integers$, then
this is the case because there is no~$\bar{x}$ that is feasible for the MIP
and satisfies~$\bar{x}_i \geq u_i + 1$ and~\eqref{eq:FDgen}.
Such a reduction can be derived in our framework by first
deriving~$C_v^\perm$.
In a second step, a CG-proof can be used to show that
\[
\left\{x \in \integers^p \times \reals^{n-p} \cap \bigcap\bradec_v:
Ax \leq b,\; x_i \geq u_i + 1,\; x \text{ satisfies~\eqref{eq:FDgen}}\right\}
=
\emptyset.
\]
As CG-proofs are compatible with our framework, also~$x_i \leq u_i$
can be derived.
\ourparagraph{Orbitopal reduction.}
While the previously discussed reductions are based on a single
permutation, orbitopal reduction handles symmetries of an entire
specially structured group~$\group$.
Orbitopal reduction assumes the integer variables of a MIP to be
arranged in an~$s\times t$ matrix~$X$ and~$\group$ to operate on the
variables by exchanging the columns of~$X$,
i.e., $\group$ acts on the columns like~$\sym{t}$.
As lexicographic order based reductions, orbitopal reduction derives
variable domain reductions.
In~\cite{doornmalen2023unified}, we discuss that orbitopal reduction is implied by~$\sigma_v(x)
\lexgeq \sigma_v(\perm(x))$ for all~$\perm\in\group$,
if~$\sigma_v$ can be partitioned into consecutive blocks of length~$t$ such
that each block corresponds to exactly one row of~$X$.
Variable domain reductions, e.g., $X_{i,j} \leq
u_{i,j}$ for some~$(i,j) \in [s] \times [t]$ with~$(i,j) \in \sigma_v$, can
be derived as above:
If all variables in~$X$ are bounded and integer,
we derive~\eqref{eq:FDgen} for all~$\perm\in\group$ and use a CG-proof to
show that no MIP solution satisfies~$X_{i,j} \geq u_{i,j} + 1$.
Deriving all inequalities~\eqref{eq:FDgen} is intractable though
as~$\group$ contains~$t!$ permutations.
But, in fact, it is sufficient to derive~\eqref{eq:FDgen} for the~$t-1$
permutations that swap variables of adjacent columns to derive the
reductions of orbitopal reduction, see~\cite{HojnyPfetsch2019}.
\ourparagraph{SST cuts.}
Let~$i \in [n]$ and~$\orb{\group}{i} = \{\perm(i) : \perm\in\group\}$
be its \emph{orbit}.
Simple SHIs are~$x_i \geq x_j$ for~$j \in
\orb{\group}{i}$~\cite{Liberti2012a}, but SHIs for different orbits can
be incompatible.
Compatibility can be ensured by adding these SHIs in
rounds~${i \in [n]}$ for different~$\group_i$ per round~\cite{LibertiOstrowski2014,Salvagnin2018}.
For~$\hat\sigma \in \sym{n}$, round~$i$ adds~$x_{\hat\sigma(i)} \geq x_{j}$ for all $j \in\orb{\group_i}{\hat\sigma(i)}$, and~$\group_i = \{\perm\in\group_{i-1} :
\perm(\hat\sigma(j)) = \hat\sigma(j),\; j \in [i-1] \}$, where~$\group_0 = \group$.
These SHIs (called SST cuts) can be derived from~$\hat\sigma(x) \lexgeq \hat\sigma(\perm(x))$, $\perm\in\group$~\cite{doornmalen2023unified}.
% Let~$i \in [n]$ and let~$\orb{\group}{i} = \{\perm(i) : \perm\in\group\}$
% denote its \emph{orbit}.
% A simple symmetry handling inequality is~$x_i \geq x_j$ for~$j \in
% \orb{\group}{i}$, see~\cite{Liberti2012a}, but inequalities for different orbits might
% not be compatible.
% To ensure compatibility, \cite{LibertiOstrowski2014,Salvagnin2018}
% add these inequalities in
% rounds~$i \in [n]$ with different groups~$\group_i$ per round.
% Given a variable ordering~$\sigma_\star$, round~$i$ adds~$x_{\sigma_\star(i)} \geq x_{j}$ for all~$j \in
% \orb{\group_i}{\sigma_\star(i)}$, and~$\group_i = \{\perm\in\group_{i-1} :
% \perm(\sigma_\star(j)) = \sigma_\star(j),\; j \in [i-1] \}$, where~$\group_0 = \group$.
% One can show that, for each of these inequalities, there
% exists~$\perm\in\group$ such that the inequality can be derived from the
% relation~$\sigma_\star(x) \lexgeq \sigma_\star(\perm(x))$.
SST cuts can be defined for arbitrary variable types.
Via dominance-based strengthening a slightly
weaker family of constraints, namely~$x_i \geq x_j - \stricteps$ instead
of~$x_i \geq x_j$, can be derived.
If~$\stricteps < 1$ and the involved variables are integral, a rounding
argument can be used to also derive~$x_i \geq x_j$.
For continuous variables, $x_i \geq x_j - \stricteps$
can be gradually made stronger by the epsilon shrinkage rule.
\ourparagraph{Orbital branching.}
To handle symmetries in binary programs, this branching rule
creates two child nodes~\cite{OstrowskiEtAl2011}.
In one node, it enforces~$x_i = 1$ for some~$i \in
[n]$;
in the other node, it enforces~$x_j = 0$ for all~$j \in
\orb{\group'}{i}$ for some subgroup~$\group'$ of~$\group$.
These reductions can be derived from SST cuts~\cite{doornmalen2023unified}
if~$\sigma_v$ is adapted to the branching decisions (cf. the discussion on~$\sigma$ above).
Since SST cuts can be derived in our framework, so can the reductions
by orbital branching.
\subsection{Encoding and Verification}
\label{sec:encoding}
For pure binary programming, the feasibility of implementing and applying the seminal
proof system in~\cite{bogaerts2023certifiedsymbr}, which is the foundation of our work,
has already been demonstrated with great success~\cite{Gocht_2019_veripb,Gocht_et_al2021_isomorphism,ElffersGochtMcCreeshNordstrom_2020, Gocht_et_al2022_CNF, Gocht_et_al2020_clique, Gocht_Nordstroem_2021}.
% \AG{@LE: Can you gather all references
% from this paper (update to journal version everywhere!) and collect all papers that use
% VeriPB, including a reference for \url{https://gitlab.com/MIAOresearch/software/VeriPB}}
%
For general MIP, the certificate system~\cite{VIPR} provides a blueprint for
encoding and verifying feasibility
reasoning~\cite{EiflerGleixnerPulaj2022_Asafecomputational,EiflerGleixner2023_Acomputational,EiflerGleixner2023}.
%
In the following, let us point out differences (and similarities) to both of these that
need to be addressed when approaching an actual implementation of a verifier for MIP.
Both types of constraints in MIP are easily encoded: linear inequalities
and integrality conditions.
%
The latter may be part of the original model or derived from equations (represented natively or as pairs of inequalities)
via integrality of coefficients and right-hand sides.
%
But unlike in the pure binary case, locally valid inequalities over unbounded
variables cannot generally be recast as globally valid inequalities.
%
A suitable verifier hence needs a native notion of implications
$[\mathcal{A} \implication C]$ as in~\cite{VIPR}.
%
As witnesses~$\omega$, affine maps $x \mapsto Qx+q$, $Q\in\Q^{n\times n}$, $q\in\Q^n$, are both
sufficient and easy to encode.
%
In many cases, $Q$ will be a sparse permutation matrix, for which only
off-diagonal elements need to be specified.
As described in~\cite{bogaerts2023certifiedsymbr}, a preorder $x \lexgeq y$ on binary
vectors can be elegantly encoded and verified as a system of linear inequalities in $x$
and $y$.
%
This is not possible in the presence of continuous and unbounded variables.
%
Instead, the branching tree $\bnbtree=(\bnbnodes,\bnbedges,\bnbdec,\sigma)$ must be
encoded as a generic graph structure with unique identifiers for $\bnbdec_v$ and
$\sigma_v$ attached to the nodes $v\in \bnbnodes$.
%
To verify $\core$-consistency, checking \eqref{consistent:arborescence},
\eqref{consistent:branching}, \eqref{consistent:dupl}, and \eqref{consistent:growing} is
elementary.
%
Checking \eqref{consistent:covering} and \eqref{consistent:packing} is also simple when
$\bnbdec_v$ are halfspaces given by linear inequalities.
%
If the boundedness condition~\eqref{consistent:bounded} does not follow trivially from
bounds on the variables, then it is the task of the certifier to provide
derivations for the boundedness and transfer them to the core before
installing the tree via \Cref{thm:treeexchange}.
The tree is then used to evaluate $\omega(x)\tgeq x$ in \eqref{eq:redruleimp}
and \eqref{eq:symruleimp}.
%
This can be performed by starting at the root node and diving in the branching tree as
long as $x$ and $\omega(x)$ are known to be contained in the same child.
%
Here, $x$ is a partial solution with fixed values or tightened bounds according to the
precondition $x \in \bigcap (\core \cup \derived) \land x\not\in C$ and elementary
propagations of these constraints.
%
If all variables $x$ are fixed, then $\dcn(x,\omega(x))$ and the result of $\omega(x)\tgeq
x$ can always be determined.
%
For partial solutions, this evaluation may fail, but all techniques discussed in
\Cref{sec:realization} allow for a witness $\omega$ such that it succeeds.
%
Some of these techniques may require so-called subproofs, \ie preliminary derivations to
strengthen the preconditions, which can afterwards be deleted again from $\derived$.
%
One example is the inductive derivation of~\eqref{eq:FDgen} %by dominance-based strengthening
given in \Cref{prop:FD} in \Cref{sec:auxresults}.
Finally, in its most basic form, a verifier may require the certifier to provide
detailed justification for each derivation.
%
In an advanced implementation, finding some of these justifications can be automated by
techniques like reverse unit propagation~\cite{GoldbergNovikov2003,ElffersGochtMcCreeshNordstrom_2020},
computing dual multipliers by a rational LP solver~\cite{EiflerGleixner2023}, or
heuristically detecting witnesses from the variable indices in the encoding of
$\sigma$.
% \begin{itemize}
% \item We denote by~$\Gamma \leq \sym{n}$ a group of symmetries
% of the MIP.
% Suppose~$\Gamma = \bigotimes_{i = 1}^k \Gamma_i$, i.e., a product group
% such that we can handle each factor (component) independently.
% \JD[inline]{I was thinking of adding another note for this action point, but it feels out-of-place. We should say something along the lines of ``We are free to choose the variable ordering $\sigma$ in $\bnbtree$ in any way, and we have given some sufficient conditions. If we have different components of the symmetry group $\Gamma$, then we can make different choices.''
% But, we can make different choices even within the same component. And, this section is about encoding, and we only use $\Gamma$ symbolically throughout the document.}
% \end{itemize}
\section{Outlook}
\label{sec:outlook}
In \Cref{sec:realization}, we have outlined how the proof system
presented in \Cref{sec:proofsystem,sec:rules} covers a wide range of important
methods implemented in state-of-the-art MIP solvers today, having to
stop short only of a discussion of lifting techniques and
infeasibility analysis, both of which typically require just
implicational reasoning.
Beyond this, we are convinced that this system can be generalized further to
make it more convenient to use and potentially (dis)cover different
algorithms:
%
\begin{enumerate*}[label=(\alph*)]
\item The $\sigma_v$ may contain duplicate entries, and more generally
could signify any set of dimension-reducing mappings for which a suitably
generalized extension relation~$\sgeq$ holds.
%
\item The lexicographic order $\lexgeq$ used to compare $\sigma_v(x)$
could become any preorder with an $\stricteps$-strict version
that allows only finitely many strict increases on the bounded image
spaces of the $\sigma_v$.
%
\item The need to install a fixed branching tree only known
\emph{after} solving could be eliminated by providing an update rule
that certifies a dynamic refinement of $\bnbtree$ \emph{while}
solving.
\end{enumerate*}
%
We know that such a rule in the style of
\Cref{thm:redundance} can be proven and works for the most common scenario of binary
variable-based branching schemes, but a more general version seems to need
inductive reasoning as in \Cref{thm:dominance} and requires further
research.
%% When solving a problem with branch-and-bound,
%% the eventual branch-and-bound tree is not known
%% up until the end of the solving procedure.
%% In this paper, we present a sequence of
%% validity-preserving configurations.
%% This tree can be changed by
%% the tree exchange rule of
%% \cref{thm:treeexchange},
%% but we believe that this rule is rather restrictive.
%% A question of interest is whether
%% less restrictive branch-and-bound tree update rules
%% can be devised.
%TODO for preprint: Add funding information (MODAL SynLab)
\medskip
\noindent
\textbf{Acknowledgements.}
%
We wish to thank Alexander Hoen, Andy Oertel, and Jakob Nordstr\"om for many patient and
insightful discussions on proof logging for binary programs.
\bibliographystyle{splncs04}
\bibliography{../bibliography}
\clearpage
\appendix
\section{Auxiliary Results and Technical Proofs}
In this appendix, we provide auxiliary results as well as the technical
proofs that we had deferred in the main part of the article.
\subsection{Auxiliary Results}
\label{sec:auxresults}
The first two results state that \Cconsistent branching trees have the
properties that one would expect from a tree generated by a
branch-and-bound algorithm.
That is, the children of a node~$u$ partition the feasible region of the
subproblem at node~$u$, and, for every feasible solution, we find exactly
one leaf of the tree in which the solution is feasible.
In the following results, we use the notation $\bradec_v \define \{B_u : u \text{ is a node on the $r$-$v$-path in~$\bnbtree$}\}$.
\begin{lemma}
\label{lemma:uniquechild}
Let $\bnbtree$ be a \Cconsistent branching tree and $u \in \bnbnodes$ with $\children(u)\not=\emptyset$. Then for all $x \in \bigcap (\core \cup \bradec_{u})$ there is exactly one $v \in \children(u)$ with
$
x \in \bigcap (\core \cup \bradec_{v}).
$
\end{lemma}
%
\begin{proof}
Let~$u \in \bnbnodes$ with~$\children(u) \neq \emptyset~$ and let~$x \in
\bigcap(\core \cup \bradec_u)$.
By~\eqref{consistent:covering}, there is~$v \in \children(u)$ with~$x \in
\bigcap(\core \cup \bradec_v)$.
In particular, for every such~$v \in \children(u)$ we have~$\sigma_u(x)
\in \sigma_u(\bigcap(\core \cup \bradec_v))\subseteq\sigma_u(B_v)$.
Uniqueness of~$v \in \children(u)$ thus follows
from~\eqref{consistent:packing}.
\qed
\end{proof}
\begin{lemma}\label{lemma:uniqueleaf}
Let~$\bnbtree$ be a \Cconsistent branching tree.
Then for all $x \in \bigcap \core$, there is exactly one leaf~$v \in
\bnbnodes$ with~$x \in \bigcap(\core \cup \bradec_v)$.
\end{lemma}
%
\begin{proof}
Because of $\bnbdec_\bnbroot=\reals^n$, $x \in \bigcap (\core \cup \bradec_\bnbroot)$.
%
The result follows by induction from \Cref{lemma:uniquechild} and finiteness
of~$V$ in~$\bnbtree$, see~\eqref{consistent:arborescence}.
\qed
\end{proof}
A crucial component of an~$(F,f)$-valid configuration as defined in
\Cref{def:validconf} is the relation induced by a branching tree~\bnbtree.
The next results state that this relation and the corresponding strict
relation define a preorder and strict order, respectively.
Afterwards, we also show that a transitivity property between these two
relations exists.
\begin{lemma}
\label{lem:preorder}
Let~$\bnbtree$ be a \Cconsistent branching tree.
Then $\tgeq$ defines a preorder and $\tgt$ defines a strict order on $\bigcap\core$.
\end{lemma}
%
\begin{proof}
Recall that~$\tgeq$ defines a preorder, if it is reflexive and transitive.
Reflexivity holds as~$\sigma_{\dcn(x,x)}(x) = \sigma_{\dcn(x,x)}(x)$.
For transitivity, let~$x,y,z \in \bigcap\core$ with~$y \tgeq x$ and~$z
\tgeq y$.
If~$v = \dcn(x,y) = \dcn(x,z) = \dcn(y,z)$,
transitivity follows by transitivity of~$=$ and~$\lexgteps$.
In the following, we thus may assume that not all deepest common nodes
are the same.
Hence w.l.o.g. we can select pairwise distinct~$i,j,k \in \{x,y,z\}$
such that~$\dcn(i,k) = \dcn(j,k)$ and~$\dcn(i,j)$ is a proper successor
of~$\dcn(i,k)$.
We call this proper successor the \emph{deepest node} and distinguish
whether~$\dcn(x,y)$, $\dcn(x,z)$, or~$\dcn(y,z)$ is the deepest node:
%
\newcommand{\threetree}[3]{%
\raisebox{-4mm}{%
\begin{tikzpicture}[anchor=north,scale=2,x=1mm, y=-1.5mm, font=\small]
%\clip (-3,0) rectangle (3,3.5);
\draw[-] (0, 0)--(2, 2);
\draw[-] (0, 0)--(-2, 2);
\draw[-] (-1, 1)--(0, 2);
\draw (-2, 2) node {$#1$};
\draw (0, 2) node {$#2$};
\draw (2, 2) node {$#3$};
\end{tikzpicture}}
}
\[
\threetree{i}{j}{k}
\;\Leftrightarrow\;
\threetree{x}{y}{z}
\;\lor\;
\threetree{x}{z}{y}
\;\lor\;
\threetree{y}{z}{x}
\]
First, let~$v = \dcn(x,y)$ be the deepest node and~$u = \dcn(x,z)
= \dcn(y,z)$.
Then, $y \tgeq x$ implies~$\sigma_v(y) = \sigma_v(x) \lor \sigma_v(y)
\lexgteps \sigma_v(x)$, which in turn yields that~$\sigma_u(y) = \sigma_u(x)\lor\sigma_u(y)
\lexgteps \sigma_u(x)$ by~\eqref{consistent:growing} because~$u$ is an
ancestor of~$v$.
Together with~$z \tgeq y \Leftrightarrow \sigma_u(z) = \sigma_u(y)\lor\sigma_u(z)
\lexgteps \sigma_u(y)$, this shows~$z \tgeq x$.
Second, let~$v = \dcn(x,z)$ be the deepest node and~$u = \dcn(y,z)
= \dcn(x,y)$.
Then, $y \tgeq x$ implies~$\sigma_u(y) = \sigma_u(x) \lor \sigma_u(y)
\lexgteps \sigma_u(x)$, and
$z \tgeq y$ yields that~$\sigma_u(z) = \sigma_u(y) \lor \sigma_u(z)
\lexgteps \sigma_u(y)$.
In fact, we claim that for both relations~$\sigma_u(y) = \sigma_u(x)$
and~$\sigma_u(z) = \sigma_u(y)$ cannot hold.
If we are able to show this, $\sigma_u(y) \lexgteps \sigma_u(x)$ and
$\sigma_u(z) \lexgteps \sigma_u(y)$ imply~$\sigma_v(y) \lexgteps
\sigma_v(x)$ and~$\sigma_v(z) \lexgteps \sigma_v(y)$, respectively,
by~\eqref{consistent:growing}.
Relation~$z \tgeq x$ then follows from transitivity of~$\lexgteps$.
To prove that~$\sigma_u(y) = \sigma_u(x)$ cannot hold, observe that~$u$
is not a leaf as~$v$ is a proper successor of~$u$.
Since~$u = \dcn(x,y)$, solutions~$x$ and~$y$ must be feasible at
different children of~$u$.
By~\eqref{consistent:packing}, we conclude~$\sigma_u(y) \neq
\sigma_u(x)$, and analogously, $\sigma_u(z) \neq \sigma_u(y)$.
Third, let~$v = \dcn(y,z)$ be the deepest node and~$u = \dcn(x,y)
= \dcn(x,z)$.
Then, $z \tgeq y$ implies~$\sigma_v(z) = \sigma_v(y) \lor \sigma_v(z)
\lexgteps \sigma_v(y)$.
As in the first case, this yields~$\sigma_u(z) = \sigma_u(y) \lor
\sigma_u(z) \lexgteps \sigma_u(y)$ by~\eqref{consistent:growing} because~$u$ is an
ancestor of~$v$.
Together with~$y \tgeq x$, this shows~$z \tgeq x$, concluding the proof
that~$\tgeq$ is a preorder on~$\bigcap\core$.
\smallskip
To prove that~$\tgt$ is a strict order on~$\bigcap\core$, we need to show
that it is irreflexive, antisymmetric, and transitive.
Irreflexivity and antisymmetry follow from irreflexivity and antisymmetry
of~$\lexgteps$.
For transitivity, let~$x,y,z \in \bigcap\core$ with~$y \tgt x$ and~$z
\tgt y$.
We pursue a similar strategy as above.
If we have~${v = \dcn(x,y) = \dcn(x,z) = \dcn(y,z)}$, then~$z \tgt x$ follows from
transitivity of~$\lexgteps$ and that~$\sigma_v$ is used in all comparisons.
Otherwise, we again distinguish the three cases above.
First, let~$v = \dcn(x,y)$ be the deepest node and~$u = \dcn(x,z)
= \dcn(y,z)$.
Then, $y \tgt x$ yields~$\sigma_v(y)
\lexgteps \sigma_v(x)$.
Thus, $\sigma_u(y) = \sigma_u(x) \lor \sigma_u(y) \lexgteps \sigma_u(x)$
by~\eqref{consistent:growing}.
From~$z \tgt y$, we get~$\sigma_u(z) \tgt \sigma_u(y)$.
Combining this shows~${z \tgt x}$.
Second, let~$v = \dcn(x,z)$ be the deepest node and~$u = \dcn(y,z)
= \dcn(x,y)$.
As above, $y \tgt x$ implies~$\sigma_u(y) \lexgteps \sigma_u(x)$,
and $z \tgt y$ yields~$\sigma_u(z) \lexgteps \sigma_u(y)$.
Transitivity of~$\lexgteps$ then implies~$\sigma_u(z) \lexgteps \sigma_u(x)$.
Since~$u$ is an ancestor of~$v$, \eqref{consistent:growing}
implies~$\sigma_v(z) \lexgteps \sigma_v(x)$, i.e, $z \tgt x$ holds.
Third, let~$v = \dcn(y,z)$ be the deepest node and~$u = \dcn(x,y)
= \dcn(x,z)$.
Then, $z \tgt y$ implies~$\sigma_v(z) \lexgteps \sigma_v(y)$, which again
implies~$\sigma_u(z) = \sigma_u(y) \lor \sigma_u(z) \lexgteps
\sigma_u(y)$.
From~$y \tgt x$, we derive~$\sigma_u(y) \lexgteps \sigma_u(x)$.
Transitivity
of~$\lexgteps$ yields~$z \tgt x$.
Relation~$\tgt$ therefore defines a strict order.
\qed
\end{proof}
\begin{lemma}\label{lem:doubleTrans}
Let~$\bnbtree$ be \Cconsistent and let~$x,y,z \in \bigcap\core$
be such that~$z \tgt y$ and~$y \tgeq x$ hold.
Then, $z \tgt x$.
\end{lemma}
\begin{proof}
If~$v = \dcn(x,y) = \dcn(x,z) = \dcn(y,z)$,
then the chain $z \tgt y \tgeq x$ implies~$\sigma_v(z) \lexgteps \sigma_v(y) =
\sigma_v(x) \lor \sigma_v(z) \lexgteps \sigma_v(y) \lexgteps
\sigma_v(x)$.
In the former case, $z \tgt x$ follows immediately, and in the latter
case it follows from transitivity of~$\lexgteps$.
In the remainder of the proof, we follow the same strategy and
terminology as in the proof of \Cref{lem:preorder}.
First, let~$v = \dcn(x,y)$ be the deepest node and~$u = \dcn(x,z)
= \dcn(y,z)$.
Then, $z \tgt y$ implies~$\sigma_u(z) \lexgteps \sigma_u(y)$, and~$y
\tgeq x$ yields~$\sigma_v(y) = \sigma_v(x) \lor \sigma_v(y) \lexgteps
\sigma_v(x)$.
Condition~\eqref{consistent:growing} then implies~$\sigma_u(y) =
\sigma_u(x) \lor \sigma_u(y) \lexgteps \sigma_u(x)$.
Combining this with~$\sigma_u(z) \lexgteps \sigma_u(y)$ shows~$z \tgt x$.
Second, let~$v = \dcn(x,z)$ be the deepest node and~$u = \dcn(y,z)
= \dcn(x,y)$.
From~$z \tgt y$, we derive~$\sigma_u(z) \lexgteps \sigma_u(y)$, which
implies~$\sigma_v(z) \lexgteps \sigma_v(y)$
by~\eqref{consistent:growing}.
Moreover, analogously to the proof of \cref{lem:preorder}, we can
show that~$y \tgeq x$ implies~$\sigma_u(y) \lexgteps \sigma_u(x)$, i.e.,
$\sigma_u(y) = \sigma_u(x)$ cannot hold.
Again by~\eqref{consistent:growing}, this implies~$\sigma_v(y) \lexgteps
\sigma_v(x)$.
Transitivity of~$\lexgteps$ then shows that~$\sigma_v(z) \lexgteps
\sigma_v(x)$, and thus, $z \tgt x$ holds.
Third, let~$v = \dcn(y,z)$ be the deepest node and~$u = \dcn(x,y)
= \dcn(x,z)$.
From~$y \tgeq x$, we conclude~$\sigma_u(y) = \sigma_u(x) \lor \sigma_u(y)
\lexgteps \sigma_u(x)$.
As above, $\sigma_u(y) = \sigma_u(x)$ cannot hold due to~\eqref{consistent:packing},
thus $\sigma_u(y) \lexgteps \sigma_u(x)$ follows.
By~\eqref{consistent:growing}, we obtain $\sigma_v(y) \lexgteps
\sigma_v(x)$.
Combining this with~$z \tgt y\Leftrightarrow\sigma_v(z) \lexgteps \sigma_v(y)$, we conclude that~$z \tgt x$ holds.
\qed
\end{proof}
The next lemma shows that $\core$-consistency of a branching tree is preserved if
the set~$\core$ of core constraints is extended.
\begin{lemma}
\label{lem:treecons}
Let $\bnbtree$ be a \Cconsistent branching tree and $C \subseteq \reals^n$.
%
Then $\bnbtree$ is also $\core\cup\{C\}$-consistent.
\end{lemma}
\begin{proof}
\eqref{consistent:arborescence}, \eqref{consistent:branching}, \eqref{consistent:dupl}, \eqref{consistent:growing},
\eqref{consistent:packing} do not involve \core.
%
Because $\bigcap\core$ is additionally intersected with $C$, the boundedness in
\eqref{consistent:bounded} continues
to hold.
%
Condition \eqref{consistent:covering} follows immediately,
as~$\bigcap(\core \cup \{C\}) \subseteq \bigcap\core$.
\qed
\end{proof}
To be able to show that symmetry reductions for MIPs can be derived within
our framework, we require that a linear representation of the lexicographic
order can be derived from our framework, which is achieved by the following
result.
\begin{proposition}
\label{prop:FD}
Let~$\configdef$ be an~$(F,f)$-valid configuration with branching tree~$\bnbtree =
(\bnbnodes, \bnbedges, \bnbdec, \sigma)$ such that all entries
of~$\sigma_v$, $v \in V$, are positive.
Let~$\gamma$ be a symmetry of~$(\bigcap\core, g)$ and~$L \leq U$ be integers.
Let~$v \in \bnbnodes$ be such that~$x_i$, $i \in \sigma_v$, is an integer variable with~$L \leq x_i \leq U$.
If~$\stricteps \leq 1$, via dominance-based strengthening, one can derive
the validity of inequality
%
\begin{align}
\label{eq:FD}
\sum_{i = 1}^{\ell_v} (U-L+1)^{\ell_v - 1} \sigma_v(x)_i
\geq
\sum_{i = 1}^{\ell_v} (U-L+1)^{\ell_v - 1} \sigma_v(\gamma(x))_i
\end{align}
%
at~$v$.
That is, if~$C' = \{x \in \reals^n : x \text{
satisfies~\eqref{eq:FD}}\}$, one can derive~$C = [\bradec_v
\rightsquigarrow C']$.
\end{proposition}
%
We have designed the following proof in such a way that it is
machine-verifiable.
To keep the presentation simple, we do not mention explicitly how the
different steps can be verified.
But the idea is that case distinctions can be implemented as ``subproofs''
in which we add some assumptions characterizing the case.
By using simple arguments in estimations, such as replacing a variable by
their upper or lower bound, these subproofs either prove the desired
statement or lead to a contradiction, showing thus the opposite statement.
%
\begin{proof}
To prove that we can derive~$C$ via dominance-based strengthening, we
need to show that, if~$x \in \bigcap(\core\cup\derived)$ and~$x \notin C$, then
there exists~$\omega\colon\reals^n\to\reals^n$ with~$g(\omega(x)) \leq
g(x)$, $\omega(x) \in \bigcap\core$, and~$\omega(x) \tgt x$.
We claim that~$\omega = \gamma$ serves as a witness.
Instead of proving the statement just for~$C$, we show a stronger result.
Let~$\Delta = U - L + 1$ and
%
\begin{align}
\label{eq:FDrec}
\sum_{i = 1}^{k} \Delta^{k - 1} \sigma_u(x)_i
&\geq
\sum_{i = 1}^{k} \Delta^{k - 1} \sigma_u(\gamma(x))_i,
&&
k \in [\ell_v].
\end{align}
%
Let~$\hat{C}^j_v = \{x \in \reals^n : x \text{ satisfies~\eqref{eq:FDrec} for } k = j\}$ and~$C^j_v =
[\bradec_v\rightsquigarrow \hat{C}^j_u]$.
We claim that we can derive~$C^j_v$ via dominance-based strengthening.
If we can establish this claim, the assertion follows as~$C =
C^{\ell_v}_v$.
To prove this claim, we proceed by induction.
Our induction hypothesis is that we can show, for all proper
ancestors~$u$ of~$v$, that we can derive~$C^j_u$ for all~$j \in
[\ell_u]$, and for node~$v$, we can derive~$C^j_v$ for all~$j \in [k-1]$
where~$k < \ell_v$.
Our goal is to show that we can also derive~$C^k_v$.
Note that the induction base case corresponds to~$k = 1$.
That is, the proof of the base case and the inductive step is the same.
Moreover, as~\eqref{eq:FDrec} is invariant under shifting the variable
domains, we may assume w.l.o.g.\ that~$L = 0$, which will simplify
notation in the following.
In the inductive step, by the hypothesis, we may assume that, for all
proper ancestors~$u$ of~$v$ and~$j \in [\ell_u]$, we have~$C^j_u \in
\derived$, and~$C^j_v \in \derived$ for all~$j \in [k-1]$.\footnote{This
assumption is only needed in the proof.
In practice, one would remove the previously derived constraints
from~$\derived$ via the deletion rule after adding~$C^k_v$.
}
To apply dominance-based strengthening,
let~$\bar{x} \in \bigcap(\core\cup\derived)$ with~$\bar{x} \notin C^k_v$.
Since~$\gamma$ is a symmetry of~$(\bigcap\core,g)$, we have~$\gamma(\bar{x})
\in \bigcap\core$ and~$g(\gamma(\bar{x})) = g(\bar{x})$.
Thus, it remains to show~$\gamma(\bar{x}) \tgt \bar{x}$.
Let~$w = \dcn(\bar{x}, \gamma(\bar{x}))$.
Following the definition of~$\tgt$,
we need to show that~$\sigma_w(\gamma(\bar{x})) \lexgteps \sigma_w(\bar{x})$.
Since~$\bar{x} \notin C^k_v$, we have~$\bar{x} \in \bigcap\bradec_v$
and~$\bar{x} \notin \hat{C}^k_v$.
By the former, $w$ and~$v$ lie on a common rooted path in~$\bnbtree$.
We distinguish whether~$w$ is a proper ancestor of~$v$ or not.
In the latter case, note that~$\sigma_w(\gamma(\bar{x})) \lexgteps \sigma_w(\bar{x})$
follows from~\eqref{consistent:growing} if we can
show~$\sigma_v(\gamma(\bar{x})) \lexgteps \sigma_v(\bar{x})$.
First, suppose~$w$ is not a proper ancestor of~$v$.
By the induction hypothesis, $C^j_u \in \derived$ for all~$j \in
[\ell_u]$ and proper ancestors~$u$ of~$v$, as well as~$C^j_v \in
\derived$ for all~$j \in [k-1]$.
For all~$j \in [k-1]$,
this in particular means that~$\bar{x} \in \hat{C}^j_v$, because~$\bar{x} \in
\bigcap\bradec_v$.
Suppose that there is one~$j' \in [k-1]$ such that the inequality
in~$\hat{C}^{j'}_v$ is strictly satisfied.
Among all such~$j'$, let~$j$ be the one that is minimal.
Then, since all variables are non-negative by the assumption~$L = 0$,
%
\begin{align*}
\sum_{i = 1}^{k}\Delta^{k-i}\sigma_v(\bar{x})_i
\geq&
\sum_{i = 1}^{j-1}\Delta^{k-i}\sigma_v(\bar{x})_i
+
\Delta^{k-j} \sigma_v(\bar{x})_j\\
=&
\sum_{i = 1}^{j-1}\Delta^{k-i}\sigma_v(\gamma(\bar{x}))_i
+
\Delta^{k-j} \sigma_v(\bar{x})_j\\
\geq&
\sum_{i = 1}^{j-1}\Delta^{k-i}\sigma_v(\gamma(\bar{x}))_i
+
\Delta^{k-j} \sigma_v(\gamma(\bar{x}))_j
+ \Delta^{k-j}\\
\geq&
1 + \sum_{i = 1}^{k}\Delta^{k-i}\sigma_v(\gamma(\bar{x}))_i.
\end{align*}
%
Here, the first inequality is due to~$L = 0$.
The third inequality holds as geometric sums satisfy~$\Delta^{k-j} = 1 + \sum_{i=j+1}^k(\Delta
- 1)\Delta^i$, and~$\sigma_v(\gamma(\bar{x}))_j
\leq (U - L) = {\Delta - 1}$.
The second estimation holds as~$j$ is the smallest index for
which~\eqref{eq:FDrec} is a strict inequality; its inequality~\eqref{eq:FDrec} thus reduces
to~$\sigma_v(\bar{x})_j > \sigma_v(\gamma(\bar{x}))_j$, which implies~$\sigma_v(\bar{x})_j
\geq 1 + \sigma_v(\gamma(\bar{x}))_j$ by integrality.
This inequality chain, however, is a contradiction to~$\bar{x} \notin C^k_v$.
Consequently, all inequalities in~$\hat{C}^1_v,\dots,\hat{C}^{k-1}_v$
must be satisfied by~$\bar{x}$ with equality.
The inequality in~$\hat{C}^k_v$ then reduces to~$\sigma_v(x)_k \geq
\sigma_v(\gamma(x))_v$.
As such, since~$\bar{x} \notin \hat{C}^k_v$, we have~$\sigma_v(\gamma(\bar{x}))_k
> \sigma_v(\bar{x})_k$.
Again, by integrality, this implies
\[
\sigma_v(\gamma(\bar{x}))_k
\geq
1 + \sigma_v(\bar{x})_k
\geq
\stricteps + \sigma_v(\bar{x})_k.
\]
As a consequence, $\sigma_v(\gamma(\bar{x})) \lexgteps \sigma_v(\bar{x})$
follows.
It remains to consider the case that~$w$ is a proper predecessor of~$v$.
In this case, $\bar{x}$ and~$\gamma(\bar{x})$ must be feasible at
different children of~$w$ as~$w$ is the deepest common node.
By~\eqref{consistent:packing}, $\sigma_w(\gamma(\bar{x}))_{\ell_w} < \sigma_w(\bar{x})_{\ell_w}$
or~$\sigma_w(\gamma(\bar{x}))_{\ell_w} > \sigma_w(\bar{x})_{\ell_w}$.
In the former case, exactly the same arguments as above can be used to
show
\[
\sum_{i = 1}^{k}\Delta^{k-i}\sigma_v(\bar{x})_i
\geq
\sum_{i = 1}^{k}\Delta^{k-i}\sigma_v(\gamma(\bar{x}))_i,
\]
as~$\sigma_v$ is an extension of~$\sigma_w$
by~\eqref{consistent:growing}, which is a contradiction to~$\bar{x} \notin C^k_v$.
In the latter case, we find (again using the same arguments)
that~$\sigma_w(\gamma(\bar{x})) \lexgteps \sigma_w(\bar{x})$.
After considering all cases, $\gamma(\bar{x}) \tgt \bar{x}$ thus follows.
\qed
\end{proof}
\subsection{Technical Proofs}
This section provides the missing technical proofs of the rules that allow
to adapt configurations while preserving their~$(F,f)$-validity.
\subsubsection{Proof of \Cref{thm:implic} (Implicational Derivation Rule)}
Let $\config=\configdef$ be the previously given configuration.
%
\eqref{cond:consistent}, \eqref{cond:obj}, and~\eqref{cond:feasC} are trivially
preserved since they do not depend on the set of derived constraints.
%
For \eqref{cond:derive}, let $x \in \bigcap\core$ with $g(x) < \primbound$.
%
By validity of \config, there exists a $y \in \bigcap (\core \cup \derived)$ with $y
\tgeq x$ and $g(y) \leq g(x) < \primbound$.
%
It suffices to show $y \in [\assumed\implication C] = \complem{\bigcap\assumed}
\cup C$.
%
If $y\not\in\bigcap\assumed$, this holds trivially.
%
If $y\in\bigcap\assumed$, then Condition \eqref{cond:implic} implies
\[
y\in \bigcap (\core \cup \derived \cup \assumed) \cap \{ x \in \reals^n :
g(x) < \primbound \} \subseteq C \subseteq [\assumed\implication C].
\]
%
In either case, \eqref{cond:derive} is satisfied for the updated configuration.
%
\qed
\subsubsection{Proof of \Cref{cor:resolution} (Resolution Rule)}
First, careful rewriting yields
%
\begin{align*}
\bigcap(\core\cup\derived)
&\subseteq
\left[\left(\assumed_1 \cup \{A_1\}\right) \implication C_1\right]
\cap
\left[\left(\assumed_2 \cup \{A_2\}\right) \implication C_2\right]\\
&=
\Big(\,\complem{\bigcap(\assumed_1 \cup \{A_1\})} \cup C_1\Big)
\cap
\Big(\,\complem{\bigcap(\assumed_2 \cup \{A_2\})} \cup C_2\Big)\\
&\subseteq
\Big(\,\complem{\bigcap(\assumed_1 \cup \{A_1\})} \cup C_1 \cup C_2\Big)
\cap
\Big(\,\complem{\bigcap(\assumed_2 \cup \{A_2\})} \cup C_1 \cup C_2\Big)\\
&=
\Big(\,\complem{\bigcap(\assumed_1 \cup \{A_1\})}
\,\cap\,
\complem{\bigcap(\assumed_2 \cup \{A_2\})} \Big)
\cup (C_1 \cup C_2)\\
&=
\Big(\Big(\,\complem{\bigcap\assumed_1} \,\cup\, \complem{A_1} \Big)
\,\cap\,
\Big(\,\complem{\bigcap\assumed_2} \,\cup\, \complem{A_2} \Big) \Big)
\cup (C_1 \cup C_2).
\end{align*}
%
By this, every $x\in\bigcap(\core\cup\derived)\subseteq A_1\cup A_2$ is
contained in at least one of the following three sets:
%
in $C_1\cup C_2$ or in $\complem{\bigcap\assumed_1}$
(if $x\in A_1\setminus(C_1\cup C_2)$) or in $\complem{\bigcap\assumed_2}$ (if $x\in A_2\setminus(C_1\cup C_2)$),
i.e.,
%
\begin{align*}
x
%% =
%% \complem{\bigcap( \assumed_1\cup\assumed_2 )}
%% \cup (C \cup D)
\in
\complem{\bigcap\assumed_1} \,\cup\, \complem{\bigcap\assumed_2}
\cup (C_1 \cup C_2)
=
\left[(\assumed_1 \cup \assumed_2) \implication (C_1 \cup C_2)\right] \eqqcolon C.
\end{align*}
Hence, $C$ satisfies \eqref{cond:implic} for $\assumed=\emptyset$ and
any value of $\primbound$ (including the value in the current configuration),
and can be added to $\derived$, preserving
validity of the configuration.
%
\qed
\subsubsection{Proof of \Cref{thm:objbound} (Objective Bound Update Rule)}
Let $\config=\configdef$ be the previously given configuration.
%
\eqref{cond:consistent} is preserved because it does not involve the objective bound.
%
Since $\primbound' < \infty$, for \eqref{cond:obj} we need to show that there exists an
$x\in\feasregion$ with $f(x) \leq \primbound'$.
%
This is a direct consequence of \eqref{cond:feasC} for \config.
%
\eqref{cond:feasC} and \eqref{cond:derive} continue to hold for the updated
configuration because the objective bound becomes stricter and thus their statements become weaker.
%
\qed
\subsubsection{Proof of \Cref{thm:objfunc} (Objective Function Update Rule)}
Assume that the previously given configuration is $\config=\configdef$.
%
\eqref{cond:consistent} and \eqref{cond:obj} are not affected by the update of $g$.
%
For~\eqref{cond:feasC} let $\hat\primbound < \primbound$.
First, assume we have $x\in\feasregion$ with $f(x) \leq \hat\primbound$.
%
\eqref{cond:feasC} for \config ensures that there also exists $\hat x\in\bigcap\core$ with
$g(\hat x) \leq \hat\primbound < \primbound$, and \eqref{cond:derive} for \config gives us a
$y\in\bigcap(\core\cup\derived)$ with $g(y) \leq g(\hat x) \leq \hat\primbound$.
%
The condition of the theorem implies that $g'(y)=g(y)$.
%
All in all, $y\in\bigcap\core$ and $g'(y) \leq \hat z$, so the forward implication in
\eqref{cond:feasC} is preserved.
For the reverse direction, assume we have $x\in\bigcap\core$ with $g'(x) \leq
\hat\primbound < \primbound$.
%
Then $g(x) = g'(x) \leq \hat\primbound$ holds by the condition of the theorem.
%
Now \eqref{cond:feasC} for \config ensures that there exists $x\in\feasregion$ with
$f(x) \leq \hat\primbound$.
To show \eqref{cond:derive} for the updated configuration, let $x \in \bigcap\core$ with
$g'(x) < \primbound$.
%
Again, the condition of the theorem implies $g(x) = g'(x) < \primbound$.
%
\eqref{cond:derive} for \config yields a $y \in \bigcap (\core \cup \derived)$ with $y
\tgeq x$ and $g(y) \leq g(x)$.
%
Finally $g'(y) = g(y) \leq g(x) = g'(x)$ follows from the condition of the theorem.
%
Hence, \eqref{cond:derive} also holds for the updated configuration.
%
\qed
\subsubsection{Proof of \Cref{thm:epsupdate} (Epsilon Shrinkage Rule)}
\eqref{cond:consistent} is trivially satisfied due to $\stricteps' > 0$.
%
\eqref{cond:obj} and \eqref{cond:feasC} are not affected when changing $\stricteps$ to
$\stricteps'$.
%
\eqref{cond:derive} becomes a weaker statement due to $\stricteps' < \stricteps$.
%
\qed
\subsubsection{Proof of \Cref{thm:transfer} (Transfer Rule)}
Let $\config=\configdef$ be the previously given configuration.
%
\eqref{cond:consistent} is preserved according to \Cref{lem:treecons},
%
\eqref{cond:obj} does not depend on \core and \derived, and
%
\eqref{cond:derive} is preserved because $\bigcap(\core\cup\{C\}) \subseteq
\bigcap\core$ and
\[
\bigcap\big((\core\cup\{C\})\cup(\derived\setminus\{C\}) \big) =
\bigcap(\core\cup\derived).
\]
%
For~\eqref{cond:feasC} let $\primbound' < \primbound$.
%
First, assume we have $x\in\feasregion$ with $f(x) \leq \primbound'$.
%
\eqref{cond:feasC} for \config yields $x'\in\bigcap\core$ with $g(x') \leq \primbound' <
z$, and \eqref{cond:derive} for \config gives us a $y\in\bigcap(\core\cup\derived)
\subseteq \bigcap(\core\cup\{C\})$ with $g(y) \leq g(x') \leq \primbound'$.
%
Hence, the forward implication in \eqref{cond:feasC} is preserved.
%
For the reverse direction, assume we have $x\in\bigcap(\core\cup\{C\}) \subseteq
\bigcap\core$ with $g(x) \leq \primbound'$.
%
Now \eqref{cond:feasC} for \config directly yields an $x\in\feasregion$ with $f(x) \leq
\primbound'$.
%
\qed
\subsubsection{Proof of \Cref{thm:delete} (Deletion Rule)}
Let $\config=\configdef$ be the previously given configuration.
%
For (a), \eqref{cond:consistent}, \eqref{cond:obj}, and \eqref{cond:feasC} are invariant.
%
\eqref{cond:derive} becomes weaker, since
$\bigcap(\core\cup\derived')\supseteq\bigcap(\core\cup\derived)$.
For (b) and (c), it suffices to show that $\big( \core', \derived, g, \primbound,
\bnbtree, \stricteps \big)$ is valid; then the validity of the derived constraint deletion
follows from~(a).
%
The proof for (b) is trivial, since $\bigcap\core'$ and $\bigcap\core$ define the same set.
For proving~(c), note that \eqref{cond:obj} is invariant, and \eqref{cond:consistent} is trivially preserved since all $\sigma_v$ are empty and the tree cannot have nodes with more than one child (and $\epsilon>0$ is unchanged).
The forward direction of \eqref{cond:feasC} is trivial, since
$\bigcap\core\subseteq\bigcap\core'$.
%
For the reverse direction, we need to show that for any $\hat z < z$, if $x \in \bigcap
\core'$ with $g(x) \le \hat z$ then there exists $y \in \feasregion$ with $f(y) \le
\hat z$.
%
If $x\in C$, then $x\in\bigcap\core$ and \eqref{cond:feasC} for $\config$ guarantees us a
suitable~$y$.
%
If $x\not\in C$, then let $\omega$ be the witness provided alongside the application of
the redundance-based strengthening rule.
%
By~\eqref{eq:redruleimp} applied to~$\big(\core', \emptyset, g, z, \bnbtree, \stricteps \big)$, \ie with $\core=\core'$ and
$\derived=\emptyset$, we know that $\omega(x)\in \bigcap(\core'\cup\{C\})=\bigcap\core$
and $g(\omega(x)) \leq g(x) \leq \hat z$.
%
Now again, \eqref{cond:feasC} for $\config$ guarantees us a suitable~$y$.
For \eqref{cond:derive}, if $x \in C$ then the condition immediately follows from the validity of the previous configuration $\config$ since $\bigcap(\core'\cup\derived) \supseteq \bigcap(\core\cup\derived)$. If $x \notin C$, then we can once again apply $\omega(x)\in\bigcap\core$ and $g(\omega(x)) \leq g(x) \leq \hat z$, hence the condition immediately follows from \eqref{cond:derive} for $\config$.
%
\qed
\subsubsection{Proof of \Cref{thm:treeexchange} (Tree Exchange Rule)}
\eqref{cond:consistent} holds because $\bnbtree'$ is assumed to be
\Cconsistent and $\stricteps > 0$.
%
\eqref{cond:obj} and \eqref{cond:feasC} are independent of the tree.
%
Due to $\derived=\emptyset$ and the reflexivity of the preorders,
\eqref{cond:derive} holds trivially for $y=x$, independently of the
tree.
%
\qed
%% \subsubsection{Proof of \Cref{thm:sigmarefine} (Sigma Refinement Rule)}
%% \eqref{cond:consistent} is preserved because $\stricteps > 0$ is not changed and
%% $\bnbtree'$ stays \Cconsistent, in particular \eqref{consistent:packing}, since $u$ is a
%% leaf of $(V,E)$, and \eqref{consistent:dupl} and \eqref{consistent:bounded} by choice of
%% the appended variable index $|j|$ such that no duplicates are introduced and $x_{|j|}$
%% is bounded from above (if $j > 0$) or below (if $j < 0$).
%% %
%% \eqref{cond:obj} and \eqref{cond:feasC} are invariant.
%% To show that~\eqref{cond:derive} continues to hold for $\config'$, suppose $x\in\core$
%% and $g(x) < z$.
%% %
%% If $x\in\bigcap\derived$, then~\eqref{cond:derive} holds trivially.
%% %
%% If $x\not\in\bigcap\derived$, then~\eqref{cond:derive} for $\config$ yields a $y\in\bigcap(\core\cup\derived)$ with
%% $g(y)\leq g(x)$ and $y\tgeq x$.
%% %
%% If also $y\tgeq[\bnbtree'] x$ holds, then~\eqref{cond:derive} is again satisfied.
%% Otherwise, note that the difference in comparison between $\tgeq$ and $\tgeq[\bnbtree']$
%% can only be explained by $\sigma'_u$, hence we must have
%% $\solleaf(x)=\solleaf(y)=\dcn(x,y)=u$ and $x,y\in\bradec_u$.
%% %
%% With this, the conditions in~\eqref{cond:sigmarefine:a} are satisfied.
%% Furthermore, $\sigma'_u(x)$ and $\sigma'_u(y)$ must be identical in the first $\ell_u$
%% entries, they must differ in the last entry, and their difference must be such that $y\tgeq[\bnbtree'] x$ does \emph{not} hold, i.e., $\sign(j) y_{|j|} < \sign(j) x_{|j|} + \stricteps$.
%% %
%% Hence, also the conditions in~\eqref{cond:sigmarefine:b} are satisfied,
%% and~\eqref{cond:sigmarefine:c} follows.
%% %
%% Then $y$ can be replaced by $\omega(y)$ to see that~\eqref{cond:derive} holds also for
%% the new configuration~$\config'$.
%% %
%% \qed
%% \subsubsection{Proof of \Cref{thm:noderefine} (Node Refinement Rule)}
%% \eqref{cond:consistent} is preserved because $\stricteps > 0$ is not changed and
%% $\bnbtree'$ remains \Cconsistent by construction, in particular \eqref{consistent:growing}
%% and \eqref{consistent:bounded} because the new nodes receive the $\sigma_u$ of their
%% parent and no new variables need to be bounded, as well as the partitioning conditions
%% \eqref{consistent:covering} and~\eqref{consistent:packing}.
%% %
%% \eqref{cond:obj} and \eqref{cond:feasC} are invariant.
%% For~\eqref{cond:derive} it suffices to show that $\tgeq$ and $\tgeq[\bnbtree']$ define the
%% same preorder, since $\core$, $\derived$, and $g$ remain the same.
%% %
%% Let $x,y\in\bigcap\core$, then we want to show $y\tgeq x\Leftrightarrow y\tgeq[\bnbtree']
%% x$.
%% %
%% If $x,y\in\bigcap(\core\cup\bradec_u)$, then their deepest common node is either $u$ or
%% one of $v_1,\ldots,v_k$.
%% %
%% In all cases $x$ and $y$ are compared via the same
%% $\sigma_u=\sigma'_u=\sigma'_{v_1}=\ldots=\sigma'_{v_k}$.
%% %
%% If one of $x,y\not\in\bigcap(\core\cup\bradec_u)$, then they are compared via a
%% $\sigma_v$, $v\in \bnbnodes\cap\bnbnodes'\setminus\{u\}$, i.e., by construction via
%% the same $\sigma'_v=\sigma_v$ in both preorders.
%% %
%% \qed
\subsubsection{Proof of \Cref{thm:dimext} (Dimension Extension Rule)}
\eqref{cond:consistent} and \eqref{cond:obj} are invariant under extension of the
dimension.
%
\eqref{cond:feasC} and \eqref{cond:derive} on the new configuration are equivalent to
\eqref{cond:feasC} and \eqref{cond:derive} on the previous configuration after projecting
out the newly added variable.
%
\qed
\subsection{Auxiliary examples of verification}
\label{sec:appendix3}
We provide several more detailed examples of automatic verification of cutting planes.
\paragraph*{Chv\'atal-Gomory cuts~\cite{Chvatal1973}.}
Given a valid inequality $\sprod{\alpha}{x} \le \beta$ with $\alpha_i = 0$, for all $i > p$, it is valid to round down all coefficients, while also rounding down the right-hand-side, \ie $\sum_{i=1}^p \down{\alpha_i}x_i \le \down{\beta}$ is valid. This is a special case of a disjunctive cut, where the disjunction is given by $\sum_{i=1}^p \down{\alpha_i}x_i \le \down{\beta} \lor \sum_{i=1}^p \down{\alpha_i}x_i \ge \down{\beta} + 1$ and the greater or equal part of the disjunction contains no points in the feasible region. In the previously existing certificate format for MIP called VIPR~\cite{VIPR}, CG-cuts are directly verified by checking the correctness of the rounding, as well as the integrality requirements. We point out that the interpretation as split cuts allows to verify a CG-cut without knowing the original inequality $\sprod{\alpha}{x} \le \beta$, by solving an auxiliary LP to find the correct Farkas multipliers to show infeasibility of $\sum_{i=1}^p \down{\alpha_i}x_i \ge \down{\beta} + 1$.
\paragraph*{Knapsack cover cuts~\cite{Balas1975}.}
% \CH{Do we need the ``simple'' here?}
Given a knapsack constraint $\sum_{j=1}^n a_j x_j \le b$, where $x \in \{0,1\}^n, b \in \integers_{>0}, a_j \in \integers_{>0}$ for all~$j \in [n]$, a \emph{cover} is a subset $C \subseteq [n]$ such that $\sum_{j \in C} a_j > b$. The corresponding cover inequality is $\sum_{j \in C} x_j \le |C| - 1$.
Any cover inequality can be verified as a split cut. We define the split disjunction $\sum_{j \in C} x_j \le |C| -1 \lor \sum_{j \in C} x_j \ge |C|$. For the first part of the disjunction, the cover inequality is trivially valid. For the second part, $\sum_{j \in C} x_j \ge |C|$ can be used to derive $x_j \ge 1$ for every~$j \in C$ by a simple aggregation proof. Then $x_j \ge 1$ for all~$j \in C$ can be aggregated using multipliers $a_j$ to derive $\sum_{j \in C} a_j x_j \ge \sum_{j \in C} a_j > b$, which is a trivially verifiable contradiction to the knapsack constraint. Applying the resolution rule certifies the cover inequality as valid.
\paragraph*{Flowcover cuts~\cite{Padberg1985}.}
Flowcover cuts make use of a structure commonly found inside a MIP model, namely single-node flow sets, defined as
\begin{align*}
T \coloneqq \left\{(x,y) \in \{0,1\}^n \times \reals^n_+ : \sum_{j=1}^n y_j \le b, y_j \le a_jx_j \text{ for } j \in [n] \right\}
\end{align*}
with $0 < a_j \le b$ for all $j \in [n]$. A set $C \subseteq \{1,\ldots,n\}$ is a \emph{flow cover} of $T$ if $\sum_{j \in C} a_j > b$.
We denote by~$(\cdot)^+ = \max\{0, \cdot\}$.
The corresponding flow cover inequality is $\sum_{j \in C} y_j + \sum_{j \in C}(a_j - \lambda)^+(1-x_j) \le b$, where $\lambda = \sum_{j \in C} a_j - b$.
We can verify a flow cover inequality as a split cut with the disjunction $\sum_{j \in C, a_j \ge \lambda}(1-x_j) \le 0 \lor \sum_{j \in C, a_j \ge \lambda}(1-x_j) \ge 1$. In the first case, the inequality reduces to $\sum_{j=1}^n y_j \le b$, which is valid by definition of $T$. In the second case, we can derive the following intermediate inequality:
\begin{align}
\label{eq:flowcover-inter1}
& \sum_{j \in C} (a_j-\lambda)^+(1-x_j) = \sum_{j \in C, a_j \ge \lambda} a_j(1-x_j) - \lambda\sum_{j \in C, a_j \ge \lambda}(1-x_j) \\
&\le \sum_{j \in C} a_j(1-x_j) - \lambda = b - \sum_{j \in C} a_j x_j
\le \left(b - \sum_{j \in C} a_j x_j\right)^+ \notag
\end{align}
The inequality holds, since $\sum_{j \in C, a_j \ge \lambda}(1-x_j) \ge 1$ by assumption, and since $a_j (1-x_j) \ge 0$.
Then we derive the flow cover inequality using the additional disjunction $\sum_{j \in C} a_jx_j \le b \lor \sum_{j \in C} a_jx_j \ge b + 1$.
In the first case, we find $\sum_{j \in C} y_j \le \sum_{j \in C} a_jx_j = b - (b-\sum_{j \in C} a_jx_j)^+$, and adding the intermediate inequality \eqref{eq:flowcover-inter1} gives the flow cover inequality. In the second case, the inequality $\sum_{j \in C} y_j \le b = b - (b-\sum_{j \in C} a_jx_j)^+$ holds and again adding the intermediate inequality \eqref{eq:flowcover-inter1} gives the flow cover inequality.
\paragraph*{Reduced cost fixing.}
Assume we solved the LP relaxation of (P), with optimal objective value $z_{MIP}$, and assume that we already found an integer feasible solution with objective value $z_I < \infty$. Let $x_j$ be a nonbasic variable at its lower bound, and for the sake of simplicity assume that $x_j \ge 0$ with reduced cost $\bar c_j \neq 0$. Then reduced cost fixing~\cite{conforti2014integer} states that the following inequality is valid:
\begin{equation*}
x_j \le \down{\frac{z_{MIP}-z_{LP}}{\bar c_j}}
\end{equation*}
Assume that $x_j$ is an integer variable, and for the sake of simplicity, assume that all variables $x_i \ge 0$. The reduction of reduced cost fixing can be proven in the setting of our proof system using the implication rule. We make a simple aggregation proof, adding $\sprod{c}{x} \le z_{MIP}$ and $-(\sprod{y}{A})x \le z_{LP}$, where $y$ are the dual multipliers of the LP solution.
This yields~$(c-\sprod{y}{A})x \le z_{MIP}-z_{LP}$. Since the LP has been solved to optimality, we can aggregate out all variables except~$x_j$ and the inequality stays valid. Dividing by $\bar c_j = c_j - \sprod{y}{A_j}$ yields the desired inequality.
An analogous construction can be used to prove the validity of reduced cost fixing for variables at their upper bound.
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
\begin{thebibliography}{10}
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\urlprefix}{URL }
\providecommand{\doi}[1]{https://doi.org/#1}
\bibitem{Achterberg2007}
Achterberg, T.: Constraint Integer Programming. Doctoral thesis, Technische
Universit\"at Berlin, Fakult\"at II - Mathematik und Naturwissenschaften,
Berlin (2007). \doi{10.14279/depositonce-1634}
\bibitem{AchterbergBixby2019}
Achterberg, T., Bixby, R., Gu, Z., Rothberg, E., Weninger, D.: Presolve
reductions in mixed integer programming. INFORMS Journal on Computing
\textbf{32}, 473--506 (2019). \doi{10.1287/ijoc.2018.0857}
\bibitem{Akgun2018MetamorphicTO}
Akgun, O., Gent, I.P., Jefferson, C., Miguel, I., Nightingale, P.: Metamorphic
testing of constraint solvers. In: International Conference on Principles and
Practice of Constraint Programming (2018). \doi{10.1007/978-3-319-98334-9_46}
\bibitem{AlkassarEtAl2011}
Alkassar, E., Böhme, S., Mehlhorn, K., Rizkallah, C., Schweitzer, P.: An
introduction to certifying algorithms. it - Information Technology
\textbf{53}(6), 287--293 (2011). \doi{10.1524/itit.2011.0655}
\bibitem{Andersen1995}
Andersen, E.D., Andersen, K.D.: Presolving in linear programming. Math.
Program. \textbf{71}(2), 221–245 (1995). \doi{10.1007/BF01586000}
\bibitem{Balas1975}
Balas, E.: Facets of the knapsack polytope. Mathematical Programming
\textbf{8}, 146--164 (1975). \doi{10.1007/BF01580440}
\bibitem{Balas1979}
Balas, E.: Disjunctive programming. In: Hammer, P., Johnson, E., Korte, B.
(eds.) Discrete Optimization II, Annals of Discrete Mathematics, vol.~5, pp.
3--51. Elsevier (1979). \doi{10.1016/S0167-5060(08)70342-X}
\bibitem{BalasCeriaCournejols1993}
Balas, E., Ceria, S., Cornu\'{e}jols, G.: A lift-and-project cutting plane
algorithm for mixed 0-1 programs. Math. Program. \textbf{58}(3), 295--324
(1993)
\bibitem{BarbosaEtal2022}
Barbosa, H., Reynolds, A., Kremer, G., Lachnitt, H., Niemetz, A., N{\"o}tzli,
A., Ozdemir, A., Preiner, M., Viswanathan, A., Viteri, S., Zohar, Y.,
Tinelli, C., Barrett, C.: Flexible proof production in an industrial-strength
{SMT} solver. In: Blanchette, J., Kov{\'a}cs, L., Pattinson, D. (eds.)
Automated Reasoning. pp. 15--35. Springer, Cham (2022).
\doi{10.1007/978-3-031-10769-6_3}
\bibitem{BendottiEtAl2021}
Bendotti, P., Fouilhoux, P., Rottner, C.: Orbitopal fixing for the full
(sub-)orbitope and application to the unit commitment problem. Mathematical
Programming \textbf{186}, 337--372 (2021). \doi{10.1007/s10107-019-01457-1}
\bibitem{SCIP8}
Bestuzheva, K., Besan\c{c}on, M., Chen, W.K., Chmiela, A., Donkiewicz, T., van
Doornmalen, J., Eifler, L., Gaul, O., Gamrath, G., Gleixner, A., Gottwald,
L., Graczyk, C., Halbig, K., Hoen, A., Hojny, C., van~der Hulst, R., Koch,
T., L\"{u}bbecke, M., Maher, S.J., Matter, F., M\"{u}hmer, E., M\"{u}ller,
B., Pfetsch, M.E., Rehfeldt, D., Schlein, S., Schl\"{o}sser, F., Serrano, F.,
Shinano, Y., Sofranac, B., Turner, M., Vigerske, S., Wegscheider, F.,
Wellner, P., Weninger, D., Witzig, J.: Enabling research through the {SCIP
Optimization Suite} 8.0. ACM Trans. Math. Softw. \textbf{49}(2) (2023).
\doi{10.1145/3585516}
\bibitem{bogaerts2023certifiedsymbr}
Bogaerts, B., Gocht, S., McCreesh, C., Nordstr{\"{o}}m, J.: Certified dominance
and symmetry breaking for combinatorial optimisation. J. Artif. Intell. Res.
\textbf{77}, 1539--1589 (2023). \doi{10.1613/JAIR.1.14296}
\bibitem{Brummayer_Lonsing_Biere2010}
Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of {SAT}
and {QBF} solvers. In: Proceedings of the 13th International Conference on
Theory and Applications of Satisfiability Testing. p. 44–57. SAT'10,
Springer-Verlag, Berlin, Heidelberg (2010). \doi{10.1007/978-3-642-14186-7_6}
\bibitem{VIPR}
Cheung, K.K.H., Gleixner, A., Steffy, D.E.: Verifying integer programming
results. In: Eisenbrand, F., Koenemann, J. (eds.) Integer Programming and
Combinatorial Optimization. pp. 148--160. Springer International Publishing,
Cham (2017)
\bibitem{Chvatal1973}
Chv\'{a}tal, V.: Edmonds polytopes and a hierarchy of combinatorial problems.
Discrete Math. \textbf{4}(4), 305–337 (1973).
\doi{10.1016/0012-365X(73)90167-2}
\bibitem{ConfortiCornuejolsZambelli2014}
Conforti, M., Cornu\'ejols, G., Zambelli, G.: Integer Programming. Springer
(2014). \doi{10.1007/978-3-319-11008-0}
\bibitem{conforti2014integer}
Conforti, M., Cornu{\'e}jols, G., Zambelli, G.: Integer programming, vol.~271.
Springer (2014). \doi{10.1007/978-3-319-11008-0}
\bibitem{CookKananShrijver1990}
Cook, W., Kannan, R., Schrijver, A.: Chv\'atal closures for mixed integer
programming problems. Math. Program. \textbf{47}(2), 155–174 (1990).
\doi{10.1007/BF01580858}
\bibitem{Cook_et_al2013}
Cook, W.J., Koch, T., Steffy, D.E., Wolter, K.: A hybrid branch-and-bound
approach for exact rational mixed-integer programming. Math. Program. Comput.
\textbf{5}(3), 305--344 (2013). \doi{10.1007/S12532-013-0055-6}
\bibitem{CournejolsLi2001}
Cornuéjols, G., Li, Y.: Elementary closures for integer programs. Operations
Research Letters \textbf{28}(1), ~1--8 (2001).
\doi{10.1016/S0167-6377(00)00067-5}
\bibitem{Cruz-FilipeHeuleEtAl2017}
Cruz-Filipe, L., Heule, M.J.H., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P.:
Efficient certified {RAT} verification. In: de~Moura, L. (ed.) Automated
Deduction -- CADE 26. pp. 220--236. Springer International Publishing, Cham
(2017)
\bibitem{Cruz-FilipeMarquesEtAl2017}
Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified
resolution proof checking. In: Proceedings, Part I, of the 23rd International
Conference on Tools and Algorithms for the Construction and Analysis of
Systems - Volume 10205. p. 118–135. Springer-Verlag, Berlin, Heidelberg
(2017). \doi{10.1007/978-3-662-54577-5_7}
\bibitem{dantzig1954tsp}
Dantzig, G., Fulkerson, R., Johnson, S.: Solution of a large-scale
traveling-salesman problem. Journal of the Operations Research Society of
America \textbf{2}(4), 393--410 (1954). \doi{10.1287/opre.2.4.393}
\bibitem{doornmalenhojny2022cyclicsymmetries}
van Doornmalen, J., Hojny, C.: Efficient propagation techniques for handling
cyclic symmetries in binary programs (2022), (preprint at
\url{https://arxiv.org/abs/2203.00992})
\bibitem{doornmalen2023unified}
van Doornmalen, J., Hojny, C.: A unified framework for symmetry handling
(2023). \doi{10.48550/arXiv.2211.01295}
\bibitem{EiflerGleixner2023_Acomputational}
Eifler, L., Gleixner, A.: A computational status update for exact rational
mixed integer programming. Mathematical Programming \textbf{197}, 793--812
(2023). \doi{10.1007/s10107-021-01749-5}
\bibitem{EiflerGleixner2023}
Eifler, L., Gleixner, A.: Safe and verified {Gomory} mixed integer cuts in a
rational {MIP} framework (2023), accepted for SIAM Journal on Optimization.
\bibitem{EiflerGleixnerPulaj2022_Asafecomputational}
Eifler, L., Gleixner, A., Pulaj, J.: A safe computational framework for integer
programming applied to {Chv\'{a}tal's} conjecture. ACM Transactions on
Mathematical Software \textbf{48}(2), 1--12 (2022). \doi{10.1145/3485630}
\bibitem{ElffersGochtMcCreeshNordstrom_2020}
Elffers, J., Gocht, S., McCreesh, C., Nordström, J.: Justifying all
differences using pseudo-boolean reasoning. Proceedings of the AAAI
Conference on Artificial Intelligence \textbf{34}(02), 1486--1494 (2020).
\doi{10.1609/aaai.v34i02.5507}
\bibitem{FischettiLiberti2012}
Fischetti, M., Liberti, L.: Orbital shrinking. In: Mahjoub, A.R., Markakis, V.,
Milis, I., Paschos, V.T. (eds.) Combinatorial Optimization, Lecture Notes in
Computer Science, vol.~7422, pp. 48--58. Springer Berlin Heidelberg (2012)
\bibitem{Friedman2007}
Friedman, E.J.: Fundamental domains for integer programs with symmetries. In:
Dress, A., Xu, Y., Zhu, B. (eds.) Combinatorial Optimization and
Applications, Lecture Notes in Computer Science, vol.~4616, pp. 146--153.
Springer Berlin Heidelberg (2007). \doi{10.1007/978-3-540-73556-4_17}
\bibitem{Fuegenschuh2005}
Fügenschuh, A., Martin, A.: Computational integer programming and cutting
planes. In: Aardal, K., Nemhauser, G., Weismantel, R. (eds.) Discrete
Optimization, Handbooks in Operations Research and Management Science,
vol.~12, pp. 69--121. Elsevier (2005). \doi{10.1016/S0927-0507(05)12002-7}
\bibitem{GamrathKochEtAl2015}
Gamrath, G., Koch, T., Martin, A., Miltenberger, M., Weninger, D.: Progress in
presolving for mixed integer programming. Mathematical Programming
Computation \textbf{7}, 367--398 (2015). \doi{10.1007/s12532-015-0083-5}
\bibitem{GillardSD2019}
Gillard, X., Schaus, P., Deville, Y.: Solvercheck: Declarative testing of
constraints. In: Schiex, T., de~Givry, S. (eds.) Principles and Practice of
Constraint Programming - 25th International Conference, {CP} 2019, Stamford,
CT, USA, September 30 - October 4, 2019, Proceedings. Lecture Notes in
Computer Science, vol. 11802, pp. 565--582. Springer (2019).
\doi{10.1007/978-3-030-30048-7\_33}
\bibitem{Gocht_2019_veripb}
Gocht, S.: {VeriPB}. 10.5281/zenodo.3548582 (2019), version 0.1.0
\bibitem{Gocht_et_al2022_CNF}
Gocht, S., Martins, R., Nordstr\"{o}m, J., Oertel, A.: {Certified CNF
Translations for Pseudo-Boolean Solving}. In: Meel, K.S., Strichman, O.
(eds.) 25th International Conference on Theory and Applications of
Satisfiability Testing (SAT 2022). Leibniz International Proceedings in
Informatics (LIPIcs), vol.~236, pp. 16:1--16:25. Schloss Dagstuhl --
Leibniz-Zentrum f{\"u}r Informatik, Dagstuhl, Germany (2022).
\doi{10.4230/LIPIcs.SAT.2022.16}
\bibitem{Gocht_et_al2020_clique}
Gocht, S., McBride, R., McCreesh, C., Nordstr{\"o}m, J., Prosser, P., Trimble,
J.: Certifying solvers for clique and maximum common (connected) subgraph
problems. In: Simonis, H. (ed.) Principles and Practice of Constraint
Programming - 26th International Conference, CP 2020, Proceedings. pp.
338--357. Lecture Notes in Computer Science, Springer (2020).
\doi{10.1007/978-3-030-58475-7_20}
\bibitem{Gocht_et_al2021_isomorphism}
Gocht, S., McCreesh, C., Nordstr\"{o}m, J.: Subgraph isomorphism meets cutting
planes: Solving with certified solutions. In: Proceedings of the Twenty-Ninth
International Joint Conference on Artificial Intelligence. IJCAI'20 (2021)
\bibitem{Gocht_Nordstroem_2021}
Gocht, S., Nordström, J.: Certifying parity reasoning efficiently using
pseudo-boolean proofs. Proceedings of the AAAI Conference on Artificial
Intelligence \textbf{35}(5), 3768--3777 (2021).
\doi{10.1609/aaai.v35i5.16494}
\bibitem{Goldberg2003}
Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for {CNF}
formulas. In: Proceedings of the Conference on Design, Automation and Test in
Europe - Volume 1. p. 10886. DATE '03, IEEE Computer Society, USA (2003)
\bibitem{GoldbergNovikov2003}
Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for cnf
formulas. In: Proceedings of the Conference on Design, Automation and Test in
Europe - Volume 1. p. 10886. DATE '03, IEEE Computer Society, USA (2003)
\bibitem{Gomory1960}
Gomory, R.E.: An algorithm for the mixed integer problem. Tech. rep., RAND
Corporation, Santa Monica, CA (1960)
\bibitem{GroetschelLovaszShrijver1988}
Gr{\"{o}}tschel, M., Lov{\'{a}}sz, L., Schrijver, A.: Geometric Algorithms and
Combinatorial Optimization, Algorithms and Combinatorics, vol.~2. Springer
(1988). \doi{10.1007/978-3-642-97881-4}
\bibitem{Hojny2020}
Hojny, C.: Packing, partitioning, and covering symresacks. Discrete Applied
Mathematics \textbf{283}, 689--717 (2020). \doi{10.1016/j.dam.2020.03.002}
\bibitem{HojnyPfetsch2019}
Hojny, C., Pfetsch, M.E.: Polytopes associated with symmetry handling.
Mathematical Programming \textbf{175}, 197--240 (2019).
\doi{10.1007/s10107-018-1239-7}
\bibitem{Jereslow1977}
Jeroslow, R.: Cutting-plane theory: Disjunctive methods. In: Hammer, P.,
Johnson, E., Korte, B., Nemhauser, G. (eds.) Studies in Integer Programming,
Annals of Discrete Mathematics, vol.~1, pp. 293--330. Elsevier (1977).
\doi{10.1016/S0167-5060(08)70741-6}
\bibitem{KaibelEtAl2011}
Kaibel, V., Peinhardt, M., Pfetsch, M.E.: Orbitopal fixing. Discrete
Optimization \textbf{8}(4), 595--610 (2011).
\doi{http://dx.doi.org/10.1016/j.disopt.2011.07.001}
\bibitem{kaibel2008packing}
Kaibel, V., Pfetsch, M.: Packing and partitioning orbitopes. Mathematical
Programming \textbf{114}(1), 1--36 (2008)
\bibitem{Liberti2012a}
Liberti, L.: Reformulations in mathematical programming: automatic symmetry
detection and exploitation. Mathematical Programming \textbf{131}(1-2),
273--304 (2012). \doi{10.1007/s10107-010-0351-0}
\bibitem{LibertiOstrowski2014}
Liberti, L., Ostrowski, J.: Stabilizer-based symmetry breaking constraints for
mathematical programs. Journal of Global Optimization \textbf{60}, 183--194
(2014)
\bibitem{Margot2002}
Margot, F.: Pruning by isomorphism in branch-and-cut. Mathematical Programming
\textbf{94}(1), 71--90 (2002). \doi{10.1007/s10107-002-0358-2}
\bibitem{Margot2003}
Margot, F.: Exploiting orbits in symmetric {ILP}. Mathematical Programming
\textbf{98}(1--3), 3--21 (2003). \doi{10.1007/s10107-003-0394-6}
\bibitem{margot2010symmetry}
Margot, F.: Symmetry in integer linear programming. 50 Years of Integer
Programming 1958--2008 pp. 647--686 (2010)
\bibitem{McConnellMehlhornEtAl2011}
McConnell, R.M., Mehlhorn, K., N{\"a}her, S., Schweitzer, P.: Survey:
Certifying algorithms. Computer Science Review \textbf{5}(2), 119--161
(2011), \url{https://publications.cispa.saarland/940/}
\bibitem{de2008proofs}
de~Moura, L.M., Bj{\o}rner, N.S.: Proofs and refutations, and {Z3}. In: LPAR
Workshops. vol.~418, pp. 123--132. Doha, Qatar (2008)
\bibitem{NemhauserWolsey1990}
Nemhauser, G.L., Wolsey, L.A.: A recursive procedure to generate all cuts for
0-1 mixed integer programs. Math. Program. \textbf{46}(3), 379–390
(1990). \doi{10.1007/BF01585752}
\bibitem{NemhauserWolsey1988}
Nemhauser, G., Wolsey, L.: Integer and Combinatorial Optimization. John Wiley
\& Sons, Ltd (1988). \doi{10.1002/9781118627372.ch1}
\bibitem{OstrowskiAnjosVannelli2015}
Ostrowski, J., Anjos, M.F., Vannelli, A.: Modified orbital branching for
structured symmetry with an application to unit commitment. Mathematical
Programming \textbf{150}(1), 99--129 (2015).
\doi{10.1007/s10107-014-0812-y}
\bibitem{OstrowskiEtAl2011}
Ostrowski, J., Linderoth, J., Rossi, F., Smriglio, S.: Orbital branching.
Mathematical Programming \textbf{126}(1), 147--178 (2011).
\doi{10.1007/s10107-009-0273-x}
\bibitem{Padberg1985}
Padberg, M.W., Roy, T.J.V., Wolsey, L.A.: Valid linear inequalities for fixed
charge problems. Oper. Res. \textbf{33}, 842--861 (1985),
\url{https://api.semanticscholar.org/CorpusID:29308357}
\bibitem{Salvagnin2018}
Salvagnin, D.: Symmetry breaking inequalities from the {Schreier-Sims} table.
In: van Hoeve, W.J. (ed.) Integration of Constraint Programming, Artificial
Intelligence, and Operations Research. pp. 521--529. Springer International
Publishing, Cham (2018)
\bibitem{Savelsbergh1994}
Savelsbergh, M.: Preprocessing and probing techniques for mixed integer
programming problems. ORSA Journal on Computing \textbf{6} (11 1994).
\doi{10.1287/ijoc.6.4.445}
\bibitem{SheraliAdams1990}
Sherali, H.D., Adams, W.P.: A hierarchy of relaxations between the continuous
and convex hull representations for zero-one programming problems. SIAM
Journal on Discrete Mathematics \textbf{3}(3), 411--430 (1990).
\doi{10.1137/0403036}
\bibitem{HeuleHuntWetzler2014}
Wetzler, N., Heule, M., Jr., W.A.H.: {DRAT}-trim: Efficient checking and
trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.)
Theory and Applications of Satisfiability Testing - {SAT} 2014 - 17th
International Conference, Held as Part of the Vienna Summer of Logic, {VSL}
2014, Vienna, Austria, July 14-17, 2014. Proceedings. Lecture Notes in
Computer Science, vol.~8561, pp. 422--429. Springer (2014).
\doi{10.1007/978-3-319-09284-3\_31}
\end{thebibliography}