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
most of the benchmarks will use small integers to avoid integer overflows as much as possible
any solver (subject or not to integer overflow) is welcome. You are not required to modify your solver to use big integers !
to gather information about the integers internally used by each solver so as to explain possible failures

The registration form asks you two questions. The first one is about the size of integers used inside your solver. This gives an idea of the integer overflow problem during the input of the formula. The second question asks you if your solver may overflow an integer when it handles multiple constraints even when each constraint individually wouldn't do harm. This is indeed another way to ask you if your implementation may face an integer overflow during the resolution of the formula.