Computer-aided proof of Erdos discrepancy properties
Computer-aided proof of Erdos discrepancy properties
复制标题
DOI：
10.1016/j.artint.2015.03.004
复制
发表时间：
2015-07-01
影响因子：
14.4
通讯作者：
Lisitsa, Alexei
中科院分区：
文献类型：
--
作者：
Konev, Boris;Lisitsa, Alexei
在20世纪30年代，Paul Erdos证明了对于任意正整数C，在任意无穷1序列（4）中，存在子序列x（d），x（2d），x（3d），. x（kd），对于某些正整数k和d，使得竖线Sigma（k）（i=1）x（i.d）竖线> C.该猜想已被称为组合数论和差异理论中的主要开放问题之一。对于C = 1的特殊情况，存在猜想的人类证明;对于C = 2，定制的计算机程序生成了长度为1124的差异为2的序列，但即使对于如此小的界限，猜想的状态仍然是开放的。我们表明，通过编码的问题到布尔可满足性和应用最先进的SAT求解器，可以获得长度为1160的差异2序列和C = 2的Erdos差异猜想的证明，声称没有差异2序列的长度为1161，或更多，存在。以类似的方式，我们得到了一个精确的界限127 645的最大长度的乘法和完全乘法序列的差异3。我们还证明了不受限制的差异3序列可以长于130 000。(C)2015 Elsevier B. V.版权所有。
In 1930s Paul Erdos conjectured that for any positive integer C in any infinite 1 sequence (4) there exists a subsequence x(d), x(2d), x(3d), ... x(kd), for some positive integers k and d, such that vertical bar Sigma(k)(i=1) x(i.d)vertical bar > 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 Erdos 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. (C) 2015 Elsevier B.V. All rights reserved.