Scippy

SCIP

Solving Constraint Integer Programs

How to use the numerically exact solving mode

As a feature standing out among today's MIP solvers, SCIP offers the option to solve mixed-integer linear programs in a numerically exact solving mode, in which it uses rational, extended-precision, and safe floating-point computation in order to guarantee that results are not affected by roundoff errors from unsafe floating-point arithmetic.

Exact solving mode requires SCIP to be built with

  • GMP for rational arithmetic in ZIMPL, SoPlex, SCIP, and PaPILO,
  • Boost multiprecision library for rationals in SCIP (and PaPILO, if linked),
  • MPFR for approximating rationals with floating-point numbers in SCIP,
  • and an exact LP solver such as SoPlex.

Enabling the exact solving mode is done by setting the parameter exact/enable = TRUE or calling the API method SCIPenableExactSolving(). Note that this has to be done before reading a problem instance. Further advanced parameters for exact solving can be set in the exact submenu.

Optionally, the output of a certificate (also known as proof logging) can be enabled by specifying certificate/filename. The resulting certificate can be checked with the proof checker VIPR or a formally verified version in CakeML. Note that certificate files are incomplete if cutting plane separation is enabled (as by default). In this case, the certificate needs to be completed using the viprcomp script prior to verification.

All plugins that want to participate in exact solving mode need to be marked as safe to use when included.

For further details we refer to the release report of SCIP 10.