# 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

where -m adds
multiplicativity restrictions

-c adds complete
multiplicativity restrictions

-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

- Run the program, e.g.

- 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

- A discrepancy 2 sequence of length 1160: A graphical representation. A log file with the satisfying assignment.

#### Discrepancy 3, Completely Multiplicative

- Input files encoding a completely multiplicative sequence of length 127645 (bzipped)
- Generated by

./edp-sinz -c 3 127645 | ./STD.py -n 127645 > output.cnf - A completely multiplicative discrepancy 3 sequence of length 127645. A graphical representation (bzipped). A log file (bzipped) with the satisfying assignment.

#### 3-Bounded, Completely Multiplicative

- Input files encoding a completely multiplicative sequence of length 127645 (bzipped)
- Generated by

./edp-sinz -o -c 3 127645 | ./STD.py -n 127645 > output.cnf - A completely multiplicative 3-bounded (and hence discrepancy 3) sequence of length 127645. A graphical representation (bzipped). A log file (bzipped) with the satisfying assignment.

#### Discrepancy 3, Multiplicative

- Input files encoding a multiplicative discrepancy 3 sequence of length 127645 (bzipped)
- Generated by

./edp-sinz -m 3 127645 | ./STD.py -n 127645 > output.cnf - A multiplicative discrepancy 3 sequence of length 127645. A graphical representation (bzipped). A log file (bzipped) with the satisfying assignment.

#### Discrepancy 3, unrestricted but starting as completely multiplicative

- Input files encoding an unrestricted discrepancy 3 sequence of length 130000 whose first 127600 elements satisfy the complete multiplicativity conditions (bzipped)
- To generate, edit edp-sinz.c and replace the variable n by a specific number when calling the multiplicatitivy rule generator.
- A discrepancy 3 sequence of length 130000. A graphical representation (bzipped). A log file (bzipped) with the satisfying assignment.

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

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