Satisfiability modulo theories for verifying MILP certificates (2024)

Runtian ZhouDavidson College
Davidson, NC 28035
dazhou@davidson.edu Haoze WuStanford University
Stanford, CA 94305
haozewu@stanford.edu Hammurabi MendesDavidson College
Davidson, NC 28035
hamendes@davidson.edu Jonad PulajDavidson College
Davidson, NC 28035
jopulaj@davidson.edu

Abstract

Correctness of results returned from mixed-integer linear programming (MILP) solvers is highly desirable, particularly in the context of applications such as hardware verification, compiler optimization, or machine-assisted theorem proving. To this end, VIPR is the first recently proposed certificate format for answers produced by MILP solvers.We design a schema to encode VIPR’s inference rules as Satisfiability Modulo Theories (SMT) instances and show the equivalence of the certificates’ correctness and the satisfiability of the corresponding SMT instances. In addition, we implement this schema with and without parallelization in a checker for VIPR certificates and test the viability of this approach on benchmark instances found in the literature with the cvc5 solver.

Index Terms:

MILP, verification, SMT, proof checking.

I Introduction

Computational mixed-integer linear programing (MILP) is widely considered a successful blend of algorithmic improvement with advancements in hardware and compilers[1], where current state-of-the-art MILP solvers can solve problems with millions of variables and constraints[2].

Demand for MILP solvers is largely driven by applications in industry, hence the underlying numerical computations typically rely on floating-point arithmetic for efficiency. For most such applications, in order to achieve a high degree of numerical stability, floating point computations are combined with numerical error tolerances. However, MILP solvers are also used in experimental mathematics to find counterexamples[3, 4] or provide numerical evidence[5, 6]. In such theorem proving applications, correctness is tantamount and additional safeguards are needed to counter the use of inexact floating-point arithmetic and/or programming or algorithmic errors. The best known example in this case is the verification in Isabelle/HOL of the infeasibility of thousands of linear programs involved in the proof of Kepler’s conjecture [7].

Another set of tools that have been successfully deployed in automated theorem proving tasks are Boolean Satisfiability (SAT) solvers and Satisfiability Modulo Theories (SMT) solvers[8]. For example, SAT solvers have had success in settling a number of long-standing mathematical problems including the Erdos discrepancy conjecture[9], the Boolean Pythagorean triples conjecture[10], and the determination of the fifth Schur number[11]. On the other hand, SMT solvers are increasingly used as subroutines for proof assistants[12, 13] to automatically resolve proof goals. In those applications, SAT/SMT solvers are often required to produce proofs, which can be independently checked by proof checkers to guarantee the correctness of the solver outputs. One theory particularly relevant to MILP is the theory of Linear Real Arithmetic, for which proof production is supported in state-of-the-art SMT solvers such as Z3, cvc5, and MathSAT5.

Although verification of answers returned by MILP solvers is not as well-established as in analogous solvers in the SAT/SMT community, significant steps forward have been made. VIPR is the first, recently proposed branch-and-cut certificate format for MILP instances, designed with simplicity in mind, which is composed of a list of statements that can be sequentially verified using a limited number of inference rules [14, 15]. This certificate format was used in the proof of special cases of Chvátal’s conjecture [16], and in the proof of the 3-sets conjecture[17]. The VIPR certificate format is currently implemented in the latest versions of exact SCIP[18], together with a checker (written in C++) for the corresponding certificates.

The motivation for this work is leveraging advances in SMT solvers for the verification of certificates for MILP instances, in order to provide a viable alternative to the existing checker.Our key observation is that a VIPR certificate is valid if and only if a corresponding quantifier-free SMT formula is satisfiable. To this end, we design a checker for VIPR certificates by encoding the format’s inference rules as SMT instances. As a by-product of our experimental evaluation, we also implement a straightforward transformation from MILP instances to SMT instances. All associated code with this project is freely available on GitHub ¹¹1https://github.com/zhoum929/Satisfiability-modulo-theories-for-verifying-MILP-certificates.

In particular, our main contributions are:

•
We describe the logic of transforming VIPR certificates into SMT instances in SMT2 format[20]. In addition, we describe the logic of transforming MILP instances in MPS format[19] into SMT instances in SMT2 format.
•
We show the equivalence of VIPR certificates and the transformed SMT instances, and evaluate the viability of our certificate checker based on benchmarks instances used in the literature[14].

The rest of this paper is organized as follows. Section II presents the logic of transformation from VIPR certificates to SMT instances. Section III proves the equivalence of VIPR certificates and the transformed SMT instances. Section IV presents an evaluation of our design tested on known benchmarks. Section V concludes the paper, and the Appendix contains more proof details of Section III, and the schema of transforming MILP instances into SMT instances.

II Methodology

In this section, we describe the design of the checker for VIPR certificates. At a high level, a VIPR certificate contains two main parts: a system part that describes the original MILP problem (constraints, variable types, etc.) and an inference part that describes the reasoning of the certificate (assumptions and inferenced constraints). As part of our checker design we declare a fixed variable in SMT2 format for each constant (coefficient) specified in the corresponding VIPR certificate, so that the symbolic computation of the inferenced reasoning can be wholly captured in an SMT solver.

When transforming the system part into an SMT instance, we don’t use assert statements to determine whether each constraint of the original MILP instance holds. Instead we encode each coefficient in a given constraint as a fixed variable. Furthermore when transforming the inference part, we also encode every coefficient in each inferenced constraint. Finally, the reasoning part of each inferenced constraint is transformed into several assert statements which check inequalities between constants.

In short, our transformation ensures that SMT solvers are only burdened with the work involved in the symbolic computation of the reasoning of the certificate. Thus we seek to reduce the computational burden of SMT solvers by mainly checking formulas with fixed variables. ²²2A relatively expensive operation we encode in our checker is Chvátal-Gomory rounding. Since the SMT2 format doesn’t natively provide a rounding operation, we enforce it by encoding several assert statements.

A standard VIPR certificate file contains $7$ sections: VAR, INT, CON, RTP, SOL, OBJ, and DER. Figure 1 provides an overview of the logic of transformation from these sections to SMT statements. The VAR and INT sections are transformed into assert and declare-fun statements specifying types of variables in the original MILP problem. The CON section is transformed into assert and declare-fun statements specifying type, rhs (right hand side value), and coefficients of each constraint in the original MILP problem. The SOL section is transformed into assert and declare-fun statements specifying variable assignment in each solution given by the MILP solver, and assert statements verifying that these variable assignments do satisfy the constraints specified in the CON section. The OBJ section is transformed into assert and declare-fun statements specifying the coefficients of each variable in the objection function. The DER section is transformed into assert and declare-fun statements specifying the type, rhs, and coefficients used in each inferenced (derived) constraint and the reasoning of that constraint. In addition, RTP, SOL, OBJ, and DER sections together contribute to the assert statement specifying the lower and upper bounds of the optimum value of the objective function, when they exist.³³3For further details on the VIPR format, please refer to[14].

In AppendixV-A, we provide additional details with respect to the transformation of each sections of the VIPR certificate. Furthermore, in AppendixV-C we describe a straightforward transformation from MPS to SMT2 format.

III Validity of VIPR transformation

The design of the derivations in the VIPR certificates, which in turn aim to verify the result returned by a MILP solver, is based on well-understood principles in the MILP domain such as the branch-and-cut method and split cuts[14]. The VIPR certificate format “flattens” the associated branch-and-bound tree explored by MILP solvers and renders it into a series of statements (corresponding to lines) that can be verified sequentially.

We provide the reader with a high level idea of our arguments’ structure. Please see AppendixV-B for a full, general proof and all its corresponding details.

Here we assume that the OBJ section begins with $\texttt{OBJ min},$ which states that the VIPR certificate is verifying a minimization problem. We also assume that the the RTP section begins with $\texttt{RTP lb ub},$ where $lb,ub$ are real numbers, which states that the VIPR certificate is verifying the upperbound of $ub$ and the lowerbound of $lb$ for the objective function.

Definition 1.

The part inside the $\{\}$ of a line in the DER section is called the reasoning of that line.

Definition 2.

The constraint presented in a line in the DER section is called valid, if it

1.
is an “assumption” (represented by reasoning of $\{asm\}$ );
2.
or, is not an assumption (represented by reasoning other than $\{asm\}$ ) but is implied by rounding and linear combinations of previous constraints. These previous constraints are called the dependencies of this line.

Definition 3.

The DER section begins with the line

DER

m

followed by $m$ lines of derived constraints. The DER section is called valid, if

1.
Each line of the DER section is valid;
2.
The last constraint in the DER section is derived only from the MILP constraints in the CON section.
3.
The last constraint in the DER section proves $lb$ is an lower bound of the optimum value.

Lemma 1.

The DER section is valid, if and only if the transcribed SMT formula is satisfiable.

Definition 4.

Each line of the SOL section presents a solution, i.e. assignments of values to variables, to the MILP problem. Such a line is called valid if it satisfies all the constraints of the MILP problem presented in the CON section.

Definition 5.

The SOL section begins with the line

SOL

m

followed by $m$ lines of solutions. The SOL section is called valid, if

1.
Each line of the SOL section is valid;
2.
At least one line of the SOL section provides a solution that proves $ub$ is an upper bound of the optimum value.

Lemma 2.

The SOL section is valid, if and only if the transcribed SMT formula is satisfiable.

Definition 6.

A VIPR certificate is called valid, if its SOL section and DER section are valid.

Note that by definition of SOL and DER being valid, a VIPR certificate being valid means the lower and upper bound of the optimum value presented in the RTP section is verified.

Theorem 1.

A VIPR certificate is valid, if and only if the transcribed SMT formula is satisfiable.

Theorem1 follows from Lemma2 and Lemma1.

IV Experiments

In this section, we evaluate the proposed proof-checking workflow on MILP benchmarks studied by the authors of VIPR[14].We focus on each of the benchmarks that meets the following criterion: 1) a certificate (of either infeasibility or both lower and upper bounds) is produced; 2) the corresponding MPS (i.e., a standard format for MILP problem) file is publicly available. This amounts to 55 benchmarks in total. Following the strategy in the original paper, we partition the benchmark set into “easy” and “hard”, which contain 46 and 9 instances, respectively.

We compare the following four strategies:

1.
Checking the VIPR certificate with the original proof checker[14];
2.
Checking the VIPR certificate by viprsmtchk, the VIPR checker designed by us that transform lines of a VIPR certificate sequentially and check by SMT solver cvc5[22], without parallelization;
3.
Checking the VIPR proof by viprsmtchk with parallelization;
4.
Checking the VIPR certificate by transforming the whole file into an SMT instance and check by SMT solver cvc5. Spefically, two programs are provided: vipr $\_$ to $\_$ smt tranforms a VIPR certificate into an SMT instance in SMT2 format, and normalize_num transforms numbers in a SMT2 file into cvc5 format (for instance, encodes $-5$ as $(-$ $5)$ ).

In addition, we also provide a MPS2SMT transformer that converts MPS files into SMT instances. Our programs are all written in C++. We run experiments in $3$ Intel Xeon Gold 6226R running at $2.90$ GHz, each with $32$ CPUs available (and each CPU supports $2$ hyperthreads). Experimental results for Strategy 1,2, and 3 are aggregated in TableII. Experimental results for Strategy 4 are aggregated in TableI.

Test Set	Inst	$T_{trans}$	$T_{cvc5}$	$S_{vipr}$	$S_{smt2}$
Easy-all	$46$	$522.9$	N/A	$711.3$	$14567.0$
Easy-solved	$31$	$30.8$	$854.9$	$101.7$	$1229.0$
Easy-memout	$15$	$1631.8$	N/A	$1971.1$	$42132.1$
Hard-all	$9$	$150.5$	N/A	$378.0$	$4422.6$
Hard-solved	$7$	$59.1$	$1176.0$	$147.6$	$1619.1$
Hard-memout	$2$	$470.3$	N/A	$1185.0$	$14234.5$

In Table I, the inst column shows the number of tests in each test set. The $T_{trans}$ and $T_{cvc5}$ columns show the average time (in second) vipr $\_$ to $\_$ smt needs to transform VIPR certificates into SMT2 format and the average time cvc5 needs to check the transformed SMT2 file. The $S_{vipr}$ and $S_{smt2}$ columns show the average size (in MB) of the original VIPR certificate and the transformed SMT2 file. For rows labeled “memout”, it contains tests where cvc5 solver requires more than $256$ GB RAM.

We observe that the size ratio between $S_{vipr}$ and $S_{smt2}$ of each test set does not exhibit significant difference. This implies the transformation from VIPR certificates to SMT2 format generates a linear increase in the file size, as expected. We also observe that $17$ benchmarks, all of which have VIPR file size at least $200$ MB, cannot be checked with Strategy 4 within space limit of $256$ GB, showing the need for sequential transformation as shown in Strategy 2 and 3. For all the test cases solved by cvc5 within the space limit, they give the same results as the results from the C++ checker provided in [14], showing that all VIPR certificates are valid.

Since a VIPR certificate contains all the reasoning to deduce the answer to a MILP problem, it is often much larger than the file containing the original MILP problem (usually encoded in MPS or LP format). As a result, if we transform all the information of a VIPR certificate into an equivalent SMT instance it may simply be too large for an SMT solver to handle directly.

For this reason, we implement a sequential version of the transformation schema in our VIPR checker, which allows SMT solvers to check most VIPR certificates within time and space limit. Specifically, we observe that the validity of each line of the DER section is independent on the lines that directly below it (see formal proof in the AppendixV-B) so its transformation can be encoded independently. Hence we can transform several lines of a VIPR certificate, called a “block”, to an SMT instance, check it with SMT solver, then delete it and transform the next sequential lines of the VIPR file. We use block size to denote the largest number of lines of a VIPR certificate that are checked each time. We also provide an option to check blocks in parallel which further enhances the efficiency of our checker.

Note that the encoding size of different lines in VIPR certificates can be very different. To ensure the SMT solver does not run into memories issues, we also set up a limit for the actual size of blocks: if over $3,000,000$ statements have been encoded in the current SMT instance, we will close the block immediately after the encoding of the current constraint.

Test Set	Inst	$T_{1}$	$T_{2,B=50}$	$T_{3,B=50}$	$S_{vipr}$
Easy	$46$	$155.6$	$12566.6$	$825.4$	$711.3$
Hard	$9$	$34.6$	$3031.6$	$232.9$	$378.0$

In Table II, the $T_{1},T_{2,B=50},$ and $T_{3,B=50}$ columns show the average time Strategy 1,2, and 3 need to check the transformed SMT instances. Here, $B=50$ is the setup of block size in viprsmtchk : at most $50$ lines of the VIPR certificate is encoded in each SMT instance.

As expected, with sequential transformation (Strategy 2 and 3), viprsmtchk is able to check each of the $55$ benchmarks and it gives the same results as the C++ checker provided in [14], showing that all VIPR certificates are valid. We also make the observation that, with parallelization (Strategy 3), viprsmtchk could check each of the $55$ benchmarks within $2$ hours, which is not too far away from the time used by the C++ checker provided in [14] (Strategy 1). We expect this performance gap can be further closed by additional optimizations in our parallelization scheme.

In addition, we test Strategy 2 and 3 on other block sizes ( $B=12,25,50,100$ ) and in all cases, $B=50$ or $100$ is the best choice. For more details of these experiments and parallelization, please see AppendixV-D.

We also perform these $55$ tests on our program of direct transformation from MILP problems in MPS format to SMT instances in SMT2 format. In comparison to transformation from VIPR certificates, directly transforming MPS format to SMT2 format is much faster, since the major work performed is parsing and no special data structures are needed. For SMT2 files transformed as a whole (non-sequentially) from VIPR certificates of the $55$ tests, $38$ can be solved by cvc5 in $4$ hours. In comparison, for the SMT2 files transformed from MPS format of the $55$ tests, only $18$ can be solved by cvc5 in $4$ hours. As expected, the time needed for an SMT solver to check the SMT2 file transformed from MPS format is often much longer than the time needed for SMT2 files transformed from VIPR certificates.

V Conclusions

In this work we seek to leverage advances in SMT solvers to verify VIPR certificates for MILP solvers. Thus we design a VIPR certificate checker that transforms the logic of the VIPR certificate into an equivalent SMT instance. We test the viability of our checker on $55$ benchmark instances, and compare between different implemented strategies. For future directions we seek to introduce further optimizations in our parallel implementation, and possibly leverage SMT solvers’ incremental techniques to improve the efficiency of our approach.

References

[1]R.E. Bixby, “A brief history of linear and mixed-integer programmingcomputation,” Documenta Mathematica, vol. 2012, pp. 107–121, 2012.
[2]T.Koch, T.Berthold, J.Pedersen, and C.Vanaret, “Progress in mathematicalprogramming solvers from 2001 to 2020,” EURO Journal on ComputationalOptimization, vol.10, p. 100031, 2022.
[3]G.Lancia, E.Pippia, and F.Rinaldi, “Using integer programming to search forcounterexamples: A case study,” in International Conference onMathematical Optimization Theory and Operations Research.Springer, 2020, pp. 69–84.
[4]J.Pulaj, “Cutting planes for families implying frankl’s conjecture,”Mathematics of Computation, vol.89, no. 322, pp. 829–857, 2020.
[5]D.Stolee, “A linear programming approach to the manickam-miklos-singhiconjecture,” 2013.
[6]F.Kenter and D.Skipper, “Integer-programming bounds on pebbling numbers ofcartesian-product graphs,” in International Conference onCombinatorial Optimization and Applications.Springer, 2018, pp. 681–695.
[7]T.C. Hales, “A proof of the kepler conjecture,” Annals ofmathematics, pp. 1065–1185, 2005.
[8]L.DeMoura and N.Bjørner, “Satisfiability modulo theories: Anappetizer,” in Brazilian Symposium on Formal Methods.Springer, 2009, pp. 23–36.
[9]B.Konev and A.Lisitsa, “Computer-aided proof of erdős discrepancyproperties,” Artificial Intelligence, vol. 224, pp. 103–118, 2015.
[10]M.J. Heule, O.Kullmann, and V.W. Marek, “Solving and verifying the booleanpythagorean triples problem via cube-and-conquer,” in InternationalConference on Theory and Applications of Satisfiability Testing.Springer, 2016, pp. 228–245.
[11]M.Heule, “Schur number five,” in Proceedings of the AAAI Conference onArtificial Intelligence, vol.32, no.1, 2018.
[12]S.Böhme and T.Nipkow, “Sledgehammer: judgement day,” in AutomatedReasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK,July 16-19, 2010. Proceedings 5.Springer, 2010, pp. 107–121.
[13]B.Ekici, A.Mebsout, C.Tinelli, C.Keller, G.Katz, A.Reynolds, andC.Barrett, “Smtcoq: A plug-in for integrating smt solvers into coq,” inComputer Aiåded Verification: 29th International Conference, CAV 2017,Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II 30.Springer, 2017, pp. 126–133.
[14]K.K. Cheung, A.Gleixner, and D.E. Steffy, “Verifying integer programmingresults,” in Integer Programming and Combinatorial Optimization: 19thInternational Conference, IPCO 2017, Waterloo, ON, Canada, June 26-28, 2017,Proceedings 19.Springer, 2017, pp.148–160.
[15]L.Eifler and A.Gleixner, “Safe and verified gomory mixed integer cuts in arational mip framework,” arXiv preprint arXiv:2303.12365, 2023.
[16]L.Eifler, A.Gleixner, and J.Pulaj, “A safe computational framework forinteger programming applied to chvátal’s conjecture,” ACMTransactions on Mathematical Software (TOMS), vol.48, no.2, pp. 1–12,2022.
[17]J.Pulaj, “Characterizing 3-sets in union-closed families,”Experimental Mathematics, vol.32, no.2, pp. 350–361, 2023.
[18]W.Cook, T.Koch, D.E. Steffy, and K.Wolter, “An exact rationalmixed-integer programming solver,” in Integer Programming andCombinatoral Optimization: 15th International Conference, IPCO 2011, NewYork, NY, USA, June 15-17, 2011. Proceedings 15.Springer, 2011, pp. 104–116.
[19]I.I. Cplex, “V12. 1: User’s manual for cplex,” InternationalBusiness Machines Corporation, vol.46, no.53, p. 157, 2009.
[20]C.Barrett, A.Stump, C.Tinelli etal., “The smt-lib standard: Version2.0,” in Proceedings of the 8th international workshop onsatisfiability modulo theories (Edinburgh, UK), vol.13, 2010, p.14.
[21]L.DeMoura and N.Bjørner, “Z3: An efficient smt solver,” inInternational conference on Tools and Algorithms for the Constructionand Analysis of Systems.Springer,2008, pp. 337–340.
[22]H.Barbosa, C.Barrett, M.Brain, G.Kremer, H.Lachnitt, M.Mann, A.Mohamed,M.Mohamed, A.Niemetz, A.Nötzli etal., “cvc5: A versatile andindustrial-strength smt solver,” in International Conference on Toolsand Algorithms for the Construction and Analysis of Systems.Springer, 2022, pp. 415–442.

Appendix

V-A Transforming VIPR certificates to SMT instances

In this subsection, we provide more details with respect to the transformation of each section of the VIPR certificate (VAR, INT, CON, RTP, SOL, OBJ, and DER). The VAR and INT sections specify the type (real or integer) of variables in the original MILP problem. The type of each integer is encoded as a boolean variable with fixed value, using a declare-fun statement and an assert statement. Let’s take a look at an example of the VAR and INT sections in a VIPR certificate.

	VAR 2
	x y
	INT 1
	1

The VAR section shows that the original MILP problem has two variables, $x$ and $y$ , and our checker will index them starting from $0$ . Thus $x$ will be interpreted as $x_{0}$ and $y$ as $x_{1}$ . The INT section shows that only the variable with index $1$ is an integer variable. Thus $x_{1}$ is an integer variable and $x_{0}$ is a real variable. This information is encoded as:

	(declare-fun is $\_$ intx0 () Bool)
	(assert (not is $\_$ intx0))
	(declare-fun is $\_$ intx1 () Bool)
	$\displaystyle\texttt{(assert is$\_$intx1)}.$

where is $\_$ intx0 is a boolean variable representing whether $x_{0}$ is an integer variable or not. Notice that VIPR does not distinguish boolean variables from integer variables or bound constraints from general constraints.

The OBJ section specifies the coefficients of variables in the objective function. Each coefficient is encoded as a real variable in SMT2 format using a declare-fun statement and an assert statement. Let’s take a look at an example of the OBJ section in a VIPR certificate:

	OBJ min
	$\displaystyle\texttt{1 0 2}.$

The first number of the second line, $1$ , means there is only one variable in the objective function with a non-zero coefficient. The next number, $0$ , is the index of this variable. The next number, $2$ , is the coefficient of this variable. Thus the original MILP problem is a minimization problem and its objective function is $2x_{0}$ . In SMT2 format, this information is encoded as:

	(declare-fun obj0 () Real)
	$\displaystyle\texttt{(assert (= obj0 2.0))}.$

We use set structures in C++ to store the indecees of variables with non-zero coefficients in the objective function.

The RTP section specifies the result of the MILP solver. It either states the system is infeasible, or it gives the upper and lower bounds of the objective function. These information will be stored during the transformation for later use and will not be encoded into SMT2 format directly.

The CON section specifies the constraints in the original MILP problem (including bounds of variables). Here is an example line in the CON constraint:

\texttt{CX G 1 2 0 2 1 3}.

The first term, CX, is the name of the constraint. Constraints (including original constraints and inferenced constraints) in a VIPR certificate will be given index starting from $0$ in the transformation. If this CX is the first line of CON section, then it will be referred to as $c_{0}$ , meaning the first constraint, and the name CX will be disregarded. The next term, $G$ , means $c_{0}$ is a $>=$ constraint. In SMT2 format this is encoded as:

	(declare-fun cs0 () Real)
	(assert (= cs0 1.0))

where $cs0$ specifies the type of the constraint with index $0$ . If it is a $>=$ constraint, $cs0$ is assigned value $1.0$ . If it is a $<=$ constraint, $cs0$ is assigned value $-1.0$ . If it is an $=$ constraint, $cs0$ is assigned value $0.0$ . This information will be used later to check the validity of inferenced constraints as linear combinations of other valid constraints.

The next term, $1$ , is the right hand side value of this constraint. In SMT2 format, this is encoded as:

	(declare-fun crhs0 () Real)
	$\displaystyle\texttt{(assert (= crhs0 1.0))}.$

The next term, $2$ , means that there are two variables in this constraint with non-zero coefficients. The last four terms mean that $x_{0}$ has coefficient $2$ and $x_{1}$ has coefficient $3$ . In SMT2 format, this is encoded as

	(declare-fun c0x0 () Real)
	(assert (= c0x0 2.0))
	(declare-fun c0x1 () Real)
	$\displaystyle\texttt{(assert (= c0x1 3.0))}.$

Thus constraint $c1$ corresponds to inequality $2x_{0}+3x_{1}\geq 1$ .

So far, we have outlined how the information of the original MILP problem is encoded into SMT2 format by our checker. The last two sections, SOL and DER, contain crucial information for the validity of a VIPR certificate. Together they verify the MILP solver reported result in the RTP section. We will discuss more details of this transformation in the next subsection.

V-B Formal Proof for the Validity of VIPR Transformation

Here is the formal proof of Theorem1. In later discussion, suppose the MILP problem corresponding to the VIPR certificate contains $n$ variables: $x_{1},\ldots,x_{n}$ .

Definition 7 (Variable Type).

For each $i\in[n]$ , define the type value of $x_{i}$ , denoted by $I_{i}$ , as following boolean variable:

I_{i}=\begin{cases}true\text{, if $x_{i}$ is an integer variable}\\false\text{, if $x_{i}$ is a real varialbe}\end{cases}.

This boolean variable are declared and assigned value at the very beginning of the transformed SMT2 file.

Definition 8 (Problem Type).

The type of the corresponding MILP problem in a VIPR certificate, denoted by $P$ , is defined as the following boolean variable:

Definition 9 (Result Type).

The type of results in a VIPR certificate, denoted by $F$ , is defined as the following boolean variable:

F:=\begin{cases}false\text{, if RTP section begins with ``RTP infeas"}\\true\text{, if OBJ section begins with ``RTP lb ub"}\\\text{$\,\,\,$ where $lb,ub$ are numbers}\end{cases}.

When $F=true$ , i.e. RTP section begins with “RTP lb ub”, we use real variables $L:=lb$ and $U:=ub$ to represent the lower and upper bound of the optimum value, correspondingly. These two variables are declared and assigned value at the very beginning of the transformed SMT2 file. If $F=false$ , then we do not assign value to $L$ and $U$ as they will be meaningless.

Definition 10 (Constraint).

Suppose the MILP problem has $n$ variables. A constraint, $C$ , in a VIPR certificate is a relationship in one of three forms: $(C_{l})^{t}x\leq C_{r}$ , $(C_{l})^{t}x\geq C_{r}$ , or $(C_{l})^{t}x=C_{r}$ , where $C_{r}\in\mathbb{R}$ , $x$ is the $n$ -dimension vector representing the $n$ variables in the MILP problem, and $C_{l}\in\mathbb{R}^{n}$ representing the coefficients of variables. Define the sign of $C$ , denoted by $C_{s}$ , as

C_{s}=\begin{cases}-1,\text{ if $C$ in the form $(C_{l})^{t}x\leq C_{r}$};\\0,\text{ if $C$ in the form $(C_{l})^{t}x=C_{r}$};\\1,\text{ if $C$ in the form $(C_{l})^{t}x\geq C_{r}$}.\end{cases}

Indices of constraints are shown as superscript.

Definition 11 (Bound Constraint).

Define bound constraint, denoted by $C^{d}$ (remember $d$ is the index of this constraint and $C^{d}$ contains three parts: $C^{d}_{l}\in\mathbb{R}^{n},C^{d}_{r}\in\mathbb{R}$ , and $C^{d}_{s}\in\{-1,0,1\}$ ), as following:

If OBJ section is of the form

	OBJ min
	$m$ $n_{1}$ $a_{1}$ $n_{2}$ $a_{2}$ $\ldots$ $n_{m}$ $a_{m}$

then

(a)
$C^{d}_{s}=1$
(b)
$C^{d}_{r}=L$
(c)
for each $i\in[m]$ , $C^{d}_{l,n_{i}}=a_{n_{i}}$
(d)
for each $j\in[n]\backslash\{n_{j}\}_{j\in[m]}$ , $C^{d}_{l,j}=0$ ;

If OBJ section is of the form

	OBJ max
	$m$ $n_{1}$ $a_{1}$ $n_{2}$ $a_{2}$ $\ldots$ $n_{m}$ $a_{m}$

then

(a)
$C^{d}_{s}=-1$
(b)
$C^{d}_{r}=U$
(c)
for each $i\in[m]$ , $C^{d}_{l,n_{i}}=a_{n_{i}}$
(d)
for each $j\in[n]\backslash\{n_{j}\}_{j\in[m]}$ , $C^{d}_{l,j}=0$ .

Let the second line of the OBJ section be of the form

\texttt{$m$ $n_{1}$ $a_{1}$ $n_{2}$ $a_{2}$ $\ldots$ $n_{m}$ $a_{m}$},

then the optimum function of the corresponding MILP problem is $f^{o}(x):=\sum_{i\in[m]}a_{i}x_{n_{i}}$ , where $x$ is the vector of variables in the MILP problem. Define $S^{o}:=\{n_{i}\}_{i\in[m]}$ , representing the set of indices of variables in the optimum function with possibly non-zero coefficients.

Definition 12 (Solution Line).

Let the $p$ th line in the SOL section be in the form

\texttt{$m$ $n_{1}$ $a_{1}$ $\ldots$ $n_{m}$ $a_{m}$}.

Define $S^{p}:=\{n_{j}\}_{j\in[m]}$ , representing the set of indices of variables with possibly non-zero assignments in this solution. Specifically, this line represents a vector $v_{p}=(x_{1},x_{2},\ldots,x_{n})$ such that $\forall j\in[m]$ , $x_{n_{j}}:=a_{j}$ and $\forall i\in[n]\backslash S^{p}$ , $x_{i}=0$ . This line is valid, if it satisfies each constraint in the CON section. If this line is valid, then the optimum function with this assignment gives an upper bound (in a minimization problem) or a lower bound (in a maximization problem) of $f^{o}(v_{j})$ for the optimum value.

Lemma 3 (Solution Line Valid).

A line in the SOL section in the form

name

m

n_{1}

a_{1}

\ldots

n_{m}

a_{m}

is valid, if and only if the transformed SMT2 clause is satisfiable.

Proof.

Suppose there are $k$ constraints in the CON section. Remember that these constraints are automatically indexed from $0$ . Hence, the validity of this line can be encoded with the following logic:

1.
$\wedge_{i\in[k]}((C^{i-1}_{s}\neq 1)\vee(\sum_{j\in[m]}C^{i-1}_{l,n_{j}}a_{j}%\geq C^{i-1}_{r}))$
2.
$\wedge_{i\in[k]}((C^{i-1}_{s}\neq 0)\vee(\sum_{j\in[m]}C^{i-1}_{l,n_{j}}a_{j}=%C^{i-1}_{r}))$
3.
$\wedge_{i\in[k]}((C^{i-1}_{s}\neq-1)\vee(\sum_{j\in[m]}C^{i-1}_{l,n_{j}}a_{j}%\leq C^{i-1}_{r}))$

∎

Definition 13 (SOL valid).

The SOL section begins with the line

SOL

m

followed by $m$ lines of solutions. The SOL section is valid, if

1.
RTP section states the MILP problem is infeasible and SOL section contains no solution;
2.
or, RTP section gives the upper/lower bounds of the MILP problem, and
1. (a)
  Each line of the SOL section is valid;
2. (b)
  If the MILP is a maximization problem, then at least one line of the SOL section proves the lower bound of the optimum value stated in the RTP section, i.e. $\exists j\in[m]$ s.t. $f^{o}(v_{j})\geq L$ .
3. (c)
  If the MILP is a minimization problem, then at least one line of the SOL section proves the upper bound of the optimum value stated in the RTP section, i.e. $\exists j\in[m]$ s.t. $f^{o}(v_{j})\leq U$ .

Lemma 4 (SOL Valid).

The SOL section is valid, if and only if the transcribed SMT formula is satisfiable.

Proof.

The properties in Definition13 can be encoded with the following logic:

1.
$F\vee(m=0)$
2.
1. (a)
  Encoded with Lemma3;
2. (b)
  If $!P$ , then $\vee_{p\in[m]}(\sum_{n\in S^{p}\cap S^{o}}\geq L)$ ,
3. (c)
  else $\vee_{p\in[m]}(\sum_{n\in S^{p}\cap S^{o}}\leq U)$ .

∎

Definition 14 (Reasoning).

The part insided the $\{\}$ of a line in the DER section is called the reasoning of that line. VIPR allows four ways to derive a new constraint in the DER section, represented by four formats of reasoning of a line in the DER section: $\{asm\},\{lin\ldots\},\{rnd\ldots\},\{uns\text{ $i_{1}$ $l_{1}$ $i_{2}$ $l_{2}%$}\}$ .

Definition 15 (Assumption).

A constraint in the DER section with reasoning of the form

\{\texttt{asm}\}

is called an assumption. Assumptions do not need a reason to be true; as the word inplied, we simply “assumes” an assumption to be true when we need to do so.

Definition 16 (Set of Assumptions).

Let $C^{x}$ be a constraint in the DER or CON section. Its set of assumptions, denoted by $S^{x}$ , is a set $\{n_{1},n_{2},\ldots,n_{m}\}$ where for each $i\in[m]$ , $C^{n_{i}}$ is an assumption.

This set is implicitly inherited from constraints to contraints. In general, VIPR certificate carries the information that if we assumes all the assumptions indexed with $S^{x}$ are true, then constraints in the CON section imply the current constraint:

1.
If $C^{x}$ is an assumtion, define $S^{x}:=\{x\}$ .
2.
If $C^{x}$ is a constraint in the CON section, define $S^{x}:=\varnothing$ .
3.
If $C^{x}$ is a constraint in the DER section and is not an assumption, please refer to Definition20, Definition22, and Definition23 for details of $S^{x}$ .

Let $S$ be the set of indices of all assumptions in the DER section. Let $C^{x}$ be a constraint in the DER or CON section. For each $i\in S$ , we use a boolean variable $B_{i}^{x}$ to identify whether $i\in C^{x}$ . Thus,

1.
If $C^{x}$ is an assumtion, then
1. (a)
  $B_{x}^{x}=true$ ;
2. (b)
  $\wedge_{i\in S^{x},i\neq x}(B_{i}^{x}=false)$ .
2.
If $C^{x}$ is a constraint in the CON section, then $\wedge_{i\in S^{x}}(B_{i}^{x}=false).$
3.
If $C^{x}$ is a constraint in the DER section and is not an assumption, please refer to Definition20, Definition22, and Definition23 for specification of $B_{i}^{x}$ ’s.

Definition 17 (Disjunction Logic).

Let $C^{a}$ and $C^{b}$ be two assumptions in the DER section. We say that $C^{a}$ and $C^{b}$ form a disjunction logic, if they satisfy the following properties:

1.
$C^{a}_{l}=C^{b}_{l}$ ;
2.
For each $i\in[n]$ such that $x_{i}$ is an integer variable, $C^{a}_{l,i}$ is an integer;
3.
For each $i\in[n]$ such that $x_{i}$ is a real variable, $C^{a}_{l,i}=0$ ;
4.
Both $C^{a}_{r}$ and $C^{b}_{r}$ are integers;
5.
One of $C^{a}_{s},C^{b}_{s}$ equals $-1$ , while the other equals $1$ ;
6.
If $C^{a}_{s}=1$ and $C^{b}_{s}=-1$ , then $C^{a}_{r}=C^{b}_{r}+1$ ; If $C^{a}_{s}=-1$ and $C^{b}_{s}=1$ , then $C^{a}_{r}=C^{b}_{r}-1$ .

Let $x$ denote the $n$ -dimension vector of variables. These properties guarantee that $C^{a}$ and $C^{b}$ are in the form

C_{l}x\leq\beta\text{ and }C_{l}x\geq\beta+1,

where $C_{l}=C^{x}_{l}=C^{y}_{l}$ and $\beta$ is an integer. Since property 1.,2.,3. guarantee that $C_{l}x$ is an integer, mathematically speaking one of $C^{x}$ and $C^{y}$ has to be true.

Lemma 5.

Let $C^{a}$ and $C^{b}$ be two constraints in a VIPR certificate. By Definition17, that $C^{a}$ and $C^{b}$ form a disjunction logic, can be encoded with the following logic:

1.
$\wedge_{i=1}^{n}(C^{a}_{l,i}=C^{b}_{l,i})$
2.
$\wedge_{i=1}^{n}(!I_{i}\vee(C^{a}_{l,i}\text{ is integer}))$
3.
$\wedge_{i=1}^{n}(I_{i}\vee(C^{a}_{l,i}=0))$
4.
$(C_{r}^{a}=\lceil C_{r}^{a}\rceil)\wedge(C_{r}^{b}=\lceil C_{r}^{b}\rceil)$ , with Lemma8
5.
$(C_{s}^{a}\neq 0)\wedge(C_{s}^{a}+C_{s}^{b}=0)$
6.
If $C_{s}^{a}=1$ , then $C_{r}^{a}=C_{r}^{b}+1$ , else $C_{r}^{a}=C_{r}^{b}-1$

where the last clause is encoded with the “ite” gate in SMT2 format.

Definition 18 (Domination).

Let $C^{1}$ and $C^{2}$ be two constraints in a VIPR certificate. We say that $C^{1}$ dominates $C^{2}$ ( $C^{1}$ implies $C^{2}$ in the following specified forms), if

1.
$C^{1}_{l}=0$ , and
1. (a)
  $C_{s}^{1}=-1$ and $C_{b}^{1}<0$ (so $C^{1}:0\leq C_{b}^{1}$ is an absurdity and implies everything), or
2. (b)
  $C_{s}^{1}=0$ and $C_{b}^{1}\neq 0$ (so $C^{1}:0=C_{b}^{1}$ is an absurdity and implies everything), or
3. (c)
  $C_{s}^{1}=1$ and $C_{b}^{1}>0$ (so $C^{1}:0\geq C_{b}^{1}$ is an absurdity and inplies everything);
2.
or, $C_{l}^{1}=C_{l}^{2}$ (so LHS of $C^{1}$ and $C^{2}$ are the same) and
1. (a)
  $C_{s}^{1}\leq 0$ , $C_{s}^{2}=-1$ , and $C_{r}^{1}\leq C_{r}^{2}$ (so each of $C_{l}^{1}x\leq C_{r}^{1}$ and $C_{l}^{1}x=C_{r}^{1}$ implies $C_{l}^{1}x\leq C_{r}^{2}$ ), or
2. (b)
  $C_{s}^{1}=0$ , $C_{s}^{2}=0$ , and $C_{r}^{1}=C_{r}^{2}$ (so $C^{1}$ and $C^{2}$ are the same), or
3. (c)
  $C_{s}^{1}\geq 0$ , $C_{s}^{2}=1$ , and $C_{r}^{1}\geq C_{r}^{2}$ (so each of $C_{l}^{1}x\geq C_{r}^{1}$ and $C_{l}^{1}x=C_{r}^{1}$ implies $C_{l}^{1}x\geq C_{r}^{2}$ )

Lemma 6.

Let $C^{1}$ and $C^{2}$ be two constraints in a VIPR certificate. By Definition18, $C^{1}$ dominates $C^{2}$ if the following clause holds:

1.
$(C_{l}^{1}=0\wedge$
1. (a)
  $(C_{s}^{1}=-1\Rightarrow C_{b}^{1}<0)\wedge$
2. (b)
  $(C_{s}^{1}=0\Rightarrow C_{b}^{1}\neq 0)\wedge$
3. (c)
  $(C_{s}^{1}=1\Rightarrow C_{b}^{1}>0))\vee$
2.
$(C_{l}^{1}=C_{l}^{2}\wedge$
1. (a)
  $(C_{s}^{2}=-1\Rightarrow(C_{s}^{1}\leq 0\wedge C_{r}^{1}\leq C_{r}^{2}))\wedge$
2. (b)
  $(C_{s}^{2}=0\Rightarrow(C_{s}^{1}=0\wedge C_{r}^{1}=C_{r}^{2}))\wedge$
3. (c)
  $(C_{s}^{2}=1\Rightarrow(C_{s}^{1}\geq 0\wedge C_{r}^{1}\geq C_{r}^{2})))$

This encoding is based on the assumption that each sign value ( $C_{s}^{1}$ and $C_{s}^{2}$ ) can be only one of $-1,0,$ and $1$ . In plain syntax, $C_{l}^{1}=0$ is encoded as

(and (=

C_{l,1}

0

) (=

C_{l,2}

0

) (=

C_{l,3}

0

)

\ldots

C_{l,n}

0

)).

Definition 19 (DER Line).

A line in the DER section with $\{lin\ldots\}$ as the reasoning part has the form

C^{x}

lin

\{

m

a_{1}

n_{1}

a_{2}

n_{2}

\ldots

a_{m}

n_{m}

\}

where $x$ denote the index of the current constraint and each $n_{i}$ is the index of a previously specified constraint. Constraints in the VIPR certificate are automatically indexed from $0$ by the sequence they appear in the file. Thus, if $y<x$ , then $C^{y}$ is specified before $x$ . This notation helps prevent loop proof. Here, we use $C^{x}$ to denote the information of the current constraint, consisting of the type of constraint, the right hand side of the constraint, and the coefficients of variables in the left hand side, from which we can declare $C^{x}_{s},C^{x}_{r}$ , and $C^{x}_{l,i}$ for each $i\in[n]$ .

Reasoning in this form states that $C^{x}$ is implied by a linear combination of previous constraints. Specifically, it stated that $\sum_{k=1}^{m}a_{k}C^{n_{k}}$ forms a constraint which dominates $C^{x}$ .

Definition 20 (Lin Valid).

A line in the DER section with reasoning of the form

C^{x}

\{

lin

m

a_{1}

n_{1}

a_{2}

n_{2}

\ldots

a_{m}

n_{m}

\}

is valid, if

1.
Each of $C^{n_{1}},C^{n_{2}},\ldots,C^{n_{m}}$ is specified before $C^{x}$ ;
2.
The linear combination of constraints described in the reasoning, i.e. $\sum_{k=1}^{m}a_{k}C^{n_{k}}$ , forms a constraint;
3.
The constraint formed by this linear combination dominates $C^{x}$ .

With these properties, we can conclude that $C^{x}$ is implied by previous constraints $C^{n_{1}},C^{n_{2}},\ldots,C^{n_{m}}$ . Hence $C^{x}$ inherits all the assumptions used by $C^{n_{1}},C^{n_{2}},\ldots,C^{n_{m}}$ :

S^{x}:=\cup_{i\in[m]}S^{n_{i}}.

In SMT logic, this is characterized by

\wedge_{i\in S}(B_{i}^{x}=\vee_{j\in[m]}B_{i}^{n_{j}}).

Lemma 7 (Lin Valid).

A line in the DER section with reasoning of the form

C^{x}

\{

lin

m

a_{1}

n_{1}

a_{2}

n_{2}

\ldots

a_{m}

n_{m}

\}

is valid if and only if the transcribed SMT formula is satisfiable.

Proof.

The three properties in Definition20 can be encoded with SMT2 clauses in the following logic:

	$\displaystyle x$	$\displaystyle>n_{1}$
	$\displaystyle x$	$\displaystyle>n_{2}$
		$\displaystyle\ldots$
	$\displaystyle x$	$\displaystyle>n_{m}$

In plain syntax, $x>n_{i}$ is encoded as

\texttt{(assert ($<$ $n_{i}$ $x$))}.

Note that,

(a)
the addition of equalities gives an equality;
(b)
the addition of equalities and “less or equal to” inequalities gives a “less or equal to” inequality;
(c)
the addition of equalities and “greater or equal to” inequalities gives a “greater or equal to” inequality.

Recall we use sign value $(-1,0,1)$ to represent the type of constraints $(\leq,=,\geq)$ . Thus, for each $i\in[m]$ ,

(a)
$a_{i}C^{n_{i}}$ is an equality if $a_{i}C^{n_{i}}_{s}=0$ ;
(b)
$a_{i}C^{n_{i}}$ is an “less or equal to” inequality if $a_{i}C^{n_{i}}_{s}<0$ ;
(c)
$a_{i}C^{n_{i}}$ is an “greater or equal to” inequality if $a_{i}C^{n_{i}}_{s}>0$ .

Hence, we can use three bool variables $cleqx,ceqx,cgeqx$ to represent whether the linear combination in the reasoning gives a $\leq,=,\geq$ relation, correspondingly:

	$\displaystyle cleqx$	$\displaystyle=\vee_{i=1}^{m}(a_{i}C^{n_{i}}_{s}\leq 0)$
	$\displaystyle ceqx$	$\displaystyle=\vee_{i=1}^{m}(a_{i}C^{n_{i}}_{s}=0)$
	$\displaystyle cgeqx$	$\displaystyle=\vee_{i=1}^{m}(a_{i}C^{n_{i}}_{s}\geq 0).$

Notice that equality implies both “less or equal to” and “greater or equal to”, and in Definition18, we can see that any relations implied by “less or equal to” or “greater or equal to” can be implied by equality. Hence, if $ceqx=true$ , we assume the linear combination in the reasoning forms an equality. Otherwise, we assume it forms an “less or equal to” inequality if $cleqx$ is true, and we assume it forms an “greater or equal to” inequality if $cgeqx$ is true (notice that when $ceqx=false$ , then at most one of $cleqx$ and $cgeqx$ can be true. If $ceqx=cgeqx=cleqx=false$ , then the linear combination in the reasoning does not form a valid relation. Denote the constraint formed by the linear combination in the reasoning as $C^{xr}$ . Then, what we described can be encoded as

	if	$\displaystyle ceqx=true,\text{ then }C^{xr}_{s}=0$
	else if	$\displaystyle cleqx=true,\text{ then }C^{xr}_{s}=-1$
	else if	$\displaystyle cgeqx=true,\text{ then }C^{xr}_{s}=1$
	else	$\displaystyle alwaysfalse=true$

where $alwaysfalse$ is a bool variable that has been assigned $false$ in the very beginning. Hence, if $C^{xr}_{s}$ cannot be assigned $-1,0,$ or $1$ , i.e. the linear combination in the reasoning does not form a valid relation, then we force the transcribed SMT formula to be unsatisfiable.

In plain syntax, this is encoded with the ite (if then else) gate:

	(assert (ite ceqx (= $C^{xr}_{s}$ 0.0)
	(ite cleqx (= $C^{xr}_{s}$ -1.0)
	(ite cgeqx (= $C^{xr}_{s}$ 1.0)
	$\displaystyle\texttt{alwaysfalse))))}.$

Clearly, for each $k\in[n]$ , $C^{xr}_{l,k}=\sum_{i=1}^{m}a_{i}C^{n_{i}}_{l,k}$ . In plain syntax, this is encoded as

	(assert (= $C^{xr}_{l,1}$ (+ (* $a_{1}$ $C^{n_{1}}_{l,1}$ ) …(* $a_{m}$ $C^{n_{m}}_{l,1}$ ))))
	$\displaystyle\ldots$
	$\displaystyle\small{\texttt{(assert (= $C^{xr}_{l,n}$ (+ (* $a_{1}$ $C^{n_{1}}%_{l,n}$) \ldots(* $a_{m}$ $C^{n_{m}}_{l,n}$))))}}.$

Similarly, $C^{xr}_{r}=\sum_{i=1}^{m}a_{i}C^{n_{i}}_{r}$ , which is encoded as

\small{\texttt{(assert (= $C^{xr}_{r}$ (+ (* $a_{1}$ $C^{n_{1}}_{r}$) \ldots(*% $a_{m}$ $C^{n_{m}}_{r}$))))}}.

In 2. we have computed $C^{xr}_{s}$ , so $C^{xr}$ is determined and we can use the schema in Lemma6 to encode property 3.

∎

Lemma 8 (Rounding Number).

Let $X$ be a real constant. Then, we can express $\lceil X\rceil$ and $\lfloor X\rfloor$ by real constant $ceilX$ and $floorX$ in SMT2 logic. In particular, we will first encode $\lceil X\rceil$ and $\lfloor X\rfloor$ into integer variables $rceilX$ and $rfloorX$ , and then force $ceilX=rceilX$ and $floorX=rfloorX$ .

To compute $ceilX$ , the logic is as following :

1.
Declare $rceilX$ as int variable;
2.
$(rceilX\geq X)\wedge((rceilX-1)<X)$ ;
3.
Declare $ceilX$ as real variable;
4.
$ceilX=rceilX$ .

In plain syntax, this is encoded as:

	(declare-fun rceilX () Int)
	(assert (and ( $\geq$ (to_real rceilX) X)
	( $<$ (to_real (- rceilX1)) x)))
	(declare-fun ceilX () Real)
	$\displaystyle\texttt{(assert (= ceilX (to\_real rceilX)) }.$

Similarly, we can compute $floorX$ with the following logic:

1.
Declare $rfloorX$ as int variable;
2.
$(rceilX\leq X)\wedge((rceilX+1)>X)$ ;
3.
Declare $floorX$ as real variable;
4.
$floorX=rfloorX$ .

Definition 21 (Gomory Cut).

Let $C$ be a constraint with $n$ variables. We say $C$ can be rounded, if

1.
For each $i\in[n]$ such that $x_{i}$ is an integer variable, $C_{l,i}$ is an integer;
2.
For each $i\in[n]$ such that $x_{i}$ is a real variable, $C_{l,i}=0$ ;
3.
$C_{s}\neq 0$ . (Nothing should be done to an equality; we can only do rounding operation for inequalities.)
Specifically, $C$ can be rounded to the constraint $C^{r}$ in the following way:
4.
When $C_{s}=-1$ :
1. (a)
  $C^{r}_{l}:=C_{l}$ ;
2. (b)
  $C^{r}_{s}:=C_{s}$ ;
3. (c)
  $C^{r}_{r}:=\lfloor C_{r}\rfloor$ .
5.
When $C_{s}=1$ :
1. (a)
  $C^{r}_{l}:=C_{l}$ ;
2. (b)
  $C^{r}_{s}:=C_{s}$ ;
3. (c)
  $C^{r}_{r}:=\lceil C_{r}\rceil$ .

Lemma 9 (Rounding Operation).

Let $C$ be a constraint with $n$ variables. That $C$ can be rounded to $C^{r}$ , by definition, can be encoded with the following logic:

1.
$\wedge_{i=1}^{n}(!I_{i}\vee(C_{l,i}\text{ is integer}))$
2.
$\wedge_{i=1}^{n}(I_{i}\vee(C_{l,i}=0))$
3.
$(C_{s}\neq 0)\wedge(C^{r}_{l}=C_{l})\wedge(C^{r}_{s}=C_{s})$
4.
If $C_{s}=-1$ , then $(C^{r}_{r}=\lfloor C_{r}\rfloor)$ , else $(C^{r}_{r}=\lceil C_{r}\rceil)$ .

Specifically, in 1., the type of each variable $x_{i}$ can be represented by a bool variable, assigned value when we declare $x_{i}$ in the SMT2 file. In 4., the rounding of $C_{r}$ is encoded with Lemma8.

Definition 22 (Rnd Valid).

A line in the DER section with reasoning of the form

C^{x}

\{

rnd

m

a_{1}

n_{1}

a_{2}

n_{2}

\ldots

a_{m}

n_{m}

\}

is valid, if

1.
Each of $C^{n_{1}},C^{n_{2}},\ldots,C^{n_{m}}$ is specified before $C^{x}$ ;
2.
The linear combination of constraints described in the reasoning, i.e. $\sum_{k=1}^{m}a_{k}C^{n_{k}}$ , forms a constraint;
3.
The constraint formed by this linear combination can be rounded by Lemma9 to another constraint, denoted by $C^{xr}$ ;
4.
The constraint $C^{xr}$ dominates $C^{x}$ .

S^{x}:=\cup_{i\in[m]}S^{n_{i}}.

In SMT logic, this is characterized by

\wedge_{i\in S}(B_{i}^{x}=\vee_{j\in[m]}B_{i}^{n_{j}}).

Lemma 10 (Rnd Valid).

A line in the DER section with reasoning of the form

C^{x}

\{

rnd

m

a_{1}

n_{1}

a_{2}

n_{2}

\ldots

a_{m}

n_{m}

\}

is valid if and only if the transcribed SMT model is satisfiable.

Proof.

We can encode each of the four properties in Definition22 with SMT logic. Property 3) involves encoding $C^{xr}$ , which is characterized in Lemma9. Property 1), 2), and 4) can be encoded exactly the same way as the three properties in Lemma7.∎

Definition 23 (Uns Valid).

A line in the DER section with reasoning of the form

C^{x}

\{

uns

i_{1}

l_{1}

i_{2}

l_{2}

\}

is valid, if

1.
Each of $C^{i_{1}},C^{l_{1}},C^{i_{2}},C^{l_{2}}$ is specified before $C^{x}$ ;
2.
Each of $C^{i_{1}}$ and $C^{i_{2}}$ dominates $C^{x}$ ;
3.
$C^{l_{1}}$ is an assumption used by $C^{i_{1}}$ and $C^{l_{2}}$ is an assumption used by $C^{i_{2}}$ (or formally, $l_{1}\in S^{i_{1}}$ and $l_{2}\in S^{i_{2}}$ );
4.
$C^{l_{1}}$ and $C^{l_{2}}$ form a disjunction logic;

Recall that by Definition16, if we assume all the assumptions indexed with $S^{i_{1}}$ are true, then CON section (which contains original constraints in the MILP problem) implies $C^{i_{1}}$ . Similarly, if we assume all the assumptions indexed with $S^{i_{2}}$ are true, then CON section implies $C^{i_{2}}$ .

Since both $C^{i_{1}}$ and $C^{i_{2}}$ imply $C^{x}$ , if we assume all the assumptions indexed with $S^{i_{1}}$ , or if we assume all the assumptions indexed with $S^{i_{2}}$ , then CON section implies $C^{x}$ . By 3) and 4), if we assume all the assumptions indexed with $(S^{i_{1}}\cup S^{i_{2}})\backslash\{l_{1},l_{2}\}$ , then CON section implies $C^{x}$ . This is because one of $l_{1}$ and $l_{2}$ has to be true, so if we assume all the assumptions indexed with

S^{x}:=(S^{i_{1}}\cup S^{i_{2}})\backslash\{l_{1},l_{2}\},

then we are actually assuming either all the assumptions indexed with $S^{i_{1}}$ or all the assumptions indexed with $S^{i_{2}}$ .

In SMT logic, this is characterized by

\wedge_{j\in S}(B_{j}^{x}=(B_{j}^{i_{1}}\vee B_{j}^{i_{2}})\wedge(!B_{j}^{l_{1%}})\wedge(!B_{j}^{l_{2}})).

Lemma 11 (Uns Valid).

A line in the DER section with reasoning of the form

C^{x}

\{

uns

i_{1}

l_{1}

i_{2}

l_{2}

\}

is valid if and only if the transcribed SMT model is satisfiable.

Proof.

The four properties in Definition23 can be encoded with SMT2 clauses in the following logic:

	$\displaystyle x$	$\displaystyle>i_{1}$
	$\displaystyle x$	$\displaystyle>i_{2}$
	$\displaystyle x$	$\displaystyle>l_{1}$
	$\displaystyle x$	$\displaystyle>l_{2}$

2.
Encoded by Lemma6;

B_{l_{1}}^{i_{1}}\wedge B_{l_{2}}^{i_{2}}

4.
Encoded by Lemma5.

∎

Definition 24 (DER Valid).

Let the last line in the DER section be of the form

\texttt{$C^{x}$ $\{\ldots\}$}.

The DER section is valid, if

1.
Each line in the DER section is valid;
2.
The set of assumptions of $C^{x}$ is empty, i.e. $S^{x}=\varnothing$ ; (This ensures $C^{x}$ can be implied from the CON section without making any assumptions.)
3.
1. (a)
  If $F$ is false, then $C^{x}$ dominates $1\leq 0$ ; (Notice that $1\leq 0$ is a mathematical absurdity, so this implies $C^{x}$ is also a mathematical absurdity, i.e. we reach a contradiction from constraints in the CON section.)
2. (b)
  If $F$ is true, then $C^{x}$ dominates $C^{d}$ . (So the lower bound of a minimization problem, or the upperbound of a maximization problem, is proved.)

Lemma 12 (DER Valid).

The DER section is valid, if and only if the transcribed SMT model is satisfiable.

Proof.

The three properties in Definition24 can be encoded with SMT2 clauses in the following logic:

1.
Encoded with Lemma7, Lemma10, and Lemma11;
2.
$\wedge_{i\in S}(!B_{i}^{x})$ ;
3.
Encoded with Lemma6 and the ite (if-then-else) gate.

∎

Theorem 2 (Main).

A VIPR certificate is valid, if and only if the transcribed SMT model is satisfiable.

Proof.

Theorem2 follows from Lemma4 and Lemma12.∎

V-C Transforming MILP instances to SMT instances

For suitable applications in the MILP domain where additional safeguards are warranted, tranforming MILP instances to SMT instances may be advantageous. However, to the best of our knowledge, we are not aware of any such general translation tools that are publicly available.

Two common file formats for MILP problems are the LP file format, which is human-readable and analogous to the algebraic form of linear constraints, and the MPS file format, which is more machine-friendly with higher precision for constraint coefficients. In MPS format, constraints are specified in a matrix, where each column corresponds to a variable and each row corresponds to a constraint. For each variable, its coefficient at each row is specified, otherwise the coefficient is assumed to be zero. In our implementation of the the transformation, we input MILP instances in MPS format and output equivalent SMT instances in SMT2 format.

At a high level, our transformation from MPS format to SMT2 format is straightforward: we use declare-fun statements to declare variables and assert statements to capture constraints or bounds specified in the original MPS file. Although it is likely that further optimizations could improve the performance of our implementation, our simple transformation provides a useful baseline for comparison. It enables us to experimentally examine the advantages of checking the correctness of a VIPR certificate for a MILP instance via an SMT solver versus directly solving the transformed MILP instances via an SMT solver.

MPS files encode most instance information in four sections: ROWS, RHS, COLUMNS, and BOUNDS. The ROWS section specifies the type of each constraint ( $>=$ , $<=$ , or $=$ ). The RHS section specifies the right hand side value of each constraint, which is assumed to be a constant. The COLUMNS section specifies for each variable its corresponding coefficient in each constraint. The BOUNDS section specifies the upper and lower bounds of each variables.

Here is the logic of transformation from these four general sections to SMT formulas. First, each variable specified in the COLUMNS section will be encoded as a declare-fun statement. Furthermore, sections ROWS, RHS and COLUMNS encode information on each constraint in the corresponding MILP problem, and each such constraint is transformed into an assert statement. Finally, sections COLUMNS and BOUNDS encode lower and upper bounds for each variable, and each such bound is transformed into an assert statement.⁴⁴4Our implementation can also handle non-standard statements in MPS format, such as the RANGE section and the INDICATOR section.

V-D Block Size and Parallelization in Sequential Transformation

In SectionIV, we presented the aggregated statistics of Strategy 2 and 3 (VIPR checking with sequential transformation, with and without parallelization) when the block size (largest number of VIPR lines encoded in each SMT instance) is $50$ ( $B=50$ ). In addition, we tested Strategy 2 and 3 with other block sizes ( $B=12,25,50,100$ ). We run experiments in $3$ Intel Xeon Gold 6226R running at $2.90$ GHz, each with $32$ CPUs available (and each CPU supports $2$ hyperthreads).

For the sake of explanation, define the set of all tests as $S$ , containing all the $55$ benchmarks as explained in SectionIV. We define the tests that run for more than $1$ minute in the non-parallel sequential version,with block size $B=50$ as $S_{1min}$ ; the ones that run for more than $1$ hour as $S_{1h}$ ; and the ones that run for more than $6$ hours as $S_{6h}$ . Compared to the non-parallel sequential approach with $B=50$ , the parallel sequential approach with $B=50$ is:

1.
$9.92$ times faster (stdev = $6.78$ ) for tests in $S$ ;
2.
$12.34$ times faster (stdev = $5.82$ ) for tests in $S_{1min}$ ;
3.
$15.95$ times faster (stdev = $4.61$ ) for tests in $S_{1h}$ ;
4.
$16.85$ times faster (stdev = $3.82$ ) for tests in $S_{6h}$ .

Maintaining the baseline comparison (non-parallel sequential with $B=50$ ), as we vary block sizes with $B\in\{12,25,50,100\}$ in the parallel approach,its fastest choice of $B$ is:

1.
$11.53$ times faster (stdev = $6.75$ ) for tests in $S$ ;
2.
$14.17$ times faster (stdev = $5.29$ ) for tests in $S_{1min}$ ;
3.
$16.93$ times faster (stdev = $3.87$ ) for tests in $S_{1h}$ ;
4.
$17.48$ times faster (stdev = $3.18$ ) for tests in $S_{6h}$ .

For larger problems (those in $S_{1h}\cup S_{6h}$ ), in all cases $B\in\{50,100\}$ represents the best block size choice.We also note diminishing returns in increasing the block size: in only $16\%$ of the larger problems, moving from $B=50$ to $B=100$ makes the speedup more than $10\%$ faster.