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 occur either 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.

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.