About integer overflow problems
One problem that may occur when solving a linear pseudo-Boolean formula
is integer overflow. Usually, programs use integers of size
corresponding to the processor registers. On the usual 32 bits
platforms, this means that the biggest positive integer is only
2,147,483,647 when using the int type (C/C++/Java). This limit is
fairly easy to reach. Using 64 bits integers gives a more comfortable
limit but doesn't really solve the problem.
Notice that it's fairly easy and natural to get constraints with
big integers. For example, if you need to encode that A=B+C where A,B,C
are integers, you may just want to write that the sum over i of 2i.Ai
is equal to the sum over i of 2i.Bi plus the sum
over i of 2i.Ci. As soon as the size of A,B,C
equals the size of the integers used by the solver, we get an integer
overflow problem. Another natural example is the encoding of the
factorization of an integer.
As far as pseudo-Boolean solver are concerned, integer overflow can
during the input of the formula or during the resolution of the formula
and will have different effect on the solver capabilities:
Such integer overflows are a concern for the evaluation because we
expect to get some wrong answer from time to time on a few benchmarks.
On the other hand, integer overflows are easy to fix and are related to
the implementation and not to the algorithm used by the solver. One
just has to use a multiple precision integer library to get rid of the
problem. Of course, computations will be a little bit slower with this
kind of library but this is the price to pay for correctness.
- during the input of the formula
If a solver doesn't use big enough integers, it will fail to read some
input file with large integers. This is a minor problem provided that
this failure is either detected of at least documented in the solver
- during the resolution of the formula
This problem is more serious because it will break the correctness of
the prover in ways that will be subtle to identify. Suppose that each
constraint in the formula contains only small numbers (i.e. such that
their sum fits into an integer). If the solver computes new constraints
or simply new weights, it may from time to time overflow the limit of
the integer it uses internally and give a wrong answer.
Some example of multiple precision libraries:
Our policy for this evaluation is
Any solver (subject or not to
integer overflow) is welcome. You are not required to modify your
solver to use big integers ! You are just required to register in the
right category of benchmarks.
- to specify a format which doesn't hide this problem by specifying
that integers may be of arbitrary size
- to classify benchmarks
according to the size of the coefficients they contain (small or big
- to ask submitters to register their solver in the category of
benchmarks which it is able to solve