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.

As far as PB solver are concerned, integer overflow can occur either during the input of the formula or during the resolution of the formula and will have different effect on the solver capabilities:

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 manual. Note 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 2ⁱ.A_i is equal to the sum over i of 2ⁱ.B_i plus the sum over i of 2ⁱ.C_i. 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.
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.

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.

Our policy for this evaluation is

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, medium and big integers)
to ask submitters to register their solver in the category of benchmarks which it is able to solve

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.