Computer-Aided Proof of Erdős Discrepancy Properties

Background

In 1930s Paul Erdős conjectured that for any positive integer $C$ in any infinite $\pm 1$ sequence $(x_n)$ there exists a subsequence $x_d, x_{2d}, x_{3d},\dots, x_{kd}$, for some positive integers $k$ and $d$, such that $\mid \sum_{i=1}^k x_{i\cdot d} \mid >C$. The conjecture has been referred to  as one of the major open problems in combinatorial number theory and discrepancy theory. For the particular case of $C=1$ a human proof of the conjecture exists; for $C=2$ a bespoke computer program had generated sequences of length $1124$ of discrepancy $2$, but the status of the conjecture remained open even for such a small bound. We show that by encoding the problem into Boolean satisfiability and applying the state of the art SAT solvers, one can obtain a discrepancy $2$ sequence of length $1160$ and a proof of the Erdős discrepancy conjecture for $C=2$, claiming that no discrepancy 2 sequence of length $1161$, or more, exists. In the similar way, we obtain a precise bound of $127\,645$ on the maximal lengths of both multiplicative and completely multiplicative sequences of discrepancy $3$.

For further details see the paper

CNF generator

All SAT instances used in our experiments have been automatically generated by a C program that can be downloaded here.

Usage: ./a.out [-m] [-c] [-X num] [-noX num] discrepancy length
-X n sets n's x to be +1
-noX n sets n's x to be -1
-o just the sequence with difference one is required to be cbounded

The output is in Donald Knuth's SAT format. To convert to DIMACS use, for example, the following python script

Running the program

The SAT generator is a short C program. We give brief instructions on how to use if under a Linux system.

• Save the program as edp-sinz.c
• Compile the program
gcc -lm edp-sinz.c -o edp-sinz
• Run the program, e.g.
./edp-sinz 2 1160 | ./STD.py -n 1160 > output.cnf
• Run your favourite SAT solver on output.cnf
• Interpreting the results: if the formula is satisfiable, the assignment to X1,.., Xl, where l is the length of a sequence, encodes the sequence of the requested discrepancy. X1,..,Xl are first in the satisfying assignment if STD.py is used with -n l option. If the formula is unsatisfiable, no sequence of the given length and discrepancy exists.

Results

Satisfiable cases

The following results have been obtained with the Plingeling SAT solver version aqw.

Discrepancy 2

• Input files encoding sequences of length 1160 and
• Generated by
./edp-sinz -X 60 2 1160 | ./STD.py -n 1160 > output.cnf

Unsatisfiable cases

• The encoding of discrepancy 2 sequences of of length 1161 is generated by
./edp-sinz -X 60 2 1161 | ./STD.py -n 1161 > output.cnf
• The encoding of discrepancy 3 multiplicative sequences of length 127646  is generated by
./edp-sinz -m 3 127646 | ./STD.py -n 127646 > output.cnf
• The encoding of discrepancy 3 completely multiplicative sequences of length 127646  is generated by
./edp-sinz -c 3 127646 | ./STD.py -n 127646 > output.cnf
• The encoding of 3-bounded completely multiplicative sequences of length 127646  is generated by
./edp-sinz -o -c 3 127646 | ./STD.py -n 127646 > output.cnf
Although SAT solvers can establish the unsatisfiability of the EDP encodings for all the cases above, this margin our web-server quota is too small to contain the DRUP certificates. We describe here the steps we followed in our experiments. We used the Glucose SAT solver version 3.0 for generating the certificate and the drup-trim tool for verifying it.
• glucose -var-decay=0.995 -certified task_d2_l1161.cnf -certified-output=<path to storage>/cert_d2_l1161.txt
• drup-trim task_d2_l1161.cnf <path to storage>/cert_d2_l1161.txt

Discrepancy checkers

In order to check independently the discrepancy of generated sequences, one can also use the Python script, a variation of the verifying script taken from the Polymath page and tailored to read outputs of a SAT solver.