Name
Abstract | ||
|---|---|---|
In 1930s Paul Erd¿s conjectured that for any positive integer C in any infinite ¿1 sequence ( x n ) there exists a subsequence x d , x 2 d , x 3 d , ¿ , x k d , for some positive integers k and d, such that | ¿ i = 1 k x i ¿ 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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1016/j.artint.2015.03.004 | Artif. Intell. |
Keywords | DocType | Volume |
computer-aided proof,erdos discrepancy problem,propositional satisfiability | Journal | 224 |
Issue | ISSN | Citations |
C | 0004-3702 | 10 |
PageRank | References | Authors |
0.57 | 18 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Boris Konev | 1 | 569 | 42.08 |
| Alexei Lisitsa | 2 | 272 | 45.94 |