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 2

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:

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

- 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:

**G**NU**M**ultiple**P**recision Arithmetic Library for C/C++

- the
BigInteger class in Java

- 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
integers)

- to ask submitters to register their solver in the category of
benchmarks which it is able to solve