Konev, Boris ORCID: 0000-0002-6507-0494 and Lisitsa, Alexei
(2015)
Computer-aided proof of Erdős discrepancy properties.
Artificial Intelligence, 224.
pp. 103-118.
Text
journal.pdf - Unspecified Download (354kB) |
Abstract
In 1930s Paul Erdős conjectured that for any positive integer C in any infinite ±1 sequence (xn) there exists a subsequence xd, x2d, x3d, ..., xkd, for some positive integers k and d, such that |∑ki=1xi·d| >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. We also demonstrate that unrestricted discrepancy 3 sequences can be longer than 130 000.
Item Type: | Article |
---|---|
Additional Information: | Revised and extended journal version of arXiv:1402.2184, http://arxiv.org/abs/1402.2184 |
Uncontrolled Keywords: | Erdős discrepancy problem, Computer-aided proof, Propositional satisfiability |
Subjects: | ?? QA75 ?? |
Depositing User: | Symplectic Admin |
Date Deposited: | 31 Mar 2016 10:09 |
Last Modified: | 15 Dec 2022 13:37 |
DOI: | 10.1016/j.artint.2015.03.004 |
Related URLs: | |
URI: | https://livrepository.liverpool.ac.uk/id/eprint/2022487 |