Computer-aided proof of Erdős discrepancy properties

DOI10.1016/J.ARTINT.2015.03.004zbMATH Open1344.68205arXiv1405.3097OpenAlexW2090857454MaRDI QIDQ892235FDOQ892235

B. Konev, Alexej P. Lisitsa

Publication date: 18 November 2015

Published in: Artificial Intelligence (Search for Journal in Brave)

Abstract: In 1930s Paul Erdos conjectured that for any positive integer $C$ in any infinite $pm1$ 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 $midsu{m}_{i=1}^k{x}_{icdotd}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 ErdH{o}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$.

Full work available at URL: https://arxiv.org/abs/1405.3097

Recommendations

• A SAT attack on the Erdős discrepancy conjecture
• On the Erdős discrepancy problem
• Counting sequences with small discrepancies
• Tao's resolution of the Erdős discrepancy problem
• Computer solution to the 17-point Erdős-Szekeres problem

zbMATH Keywords

propositional satisfiabilityBoolean satisfiabilitycomputer-aided proofErdős discrepancy problem

Mathematics Subject Classification ID

Irregularities of distribution, discrepancy (11K38) Arithmetic combinatorics; higher degree uniformity (11B30)

Cites Work

• Theory and Applications of Satisfiability Testing
• A proof of the Kepler conjecture
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A panorama of discrepancy theory
• Title not available (Why is that?)
• Geometric discrepancy. An illustrated guide
• The four-colour theorem
• Every planar map is four colorable
• Solution of the Robbins problem
• Title not available (Why is that?)
• Principles and Practice of Constraint Programming – CP 2004
• Some unsolved problems
• Transmitting in the \(n\)-dimensional cube
• Title not available (Why is that?)
• Symmetry in Gardens of Eden
• On Highly Composite and Similar Numbers
• A Machine-Checked Proof of the Odd Order Theorem
• The Non-Existence of Finite Projective Planes of Order 10
• A SAT Attack on the Erdős Discrepancy Conjecture
• Title not available (Why is that?)
• Remark concerning integer sequences
• A concise introduction to mathematical logic
• A revision of the proof of the Kepler conjecture
• Automated theorem provers: a practical tool for the working mathematician?
• Symmetry definitions for constraint satisfaction problems
• Title not available (Why is that?)
• Completely multiplicative functions taking values in ${-1,1}$
• Title not available (Why is that?)
• Discrepancy in arithmetic progressions
• On the hereditary discrepancy of homogeneous arithmetic progressions
• Roth’s Orthogonal Function Method in Discrepancy Theory and Some New Connections
• On the Erdős Discrepancy Problem
• Optimal private halfspace counting via discrepancy
• Erdős and Arithmetic Progressions
• Theory and Applications of Satisfiability Testing
• Note on irregularities of distribution

Cited In (17)

• Formally verifying the solution to the Boolean Pythagorean triples problem
• Title not available (Why is that?)
• Decomposing SAT Instances with Pseudo Backbones
• Simulating strong practical proof systems with extended resolution
• Computer-aided constructions of commafree codes
• The Erdös discrepancy problem
• Functional Encryption for Inner Product with Full Function Privacy
• Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
• On computer-assisted proofs in ordinal number theory
• The resolution of Keller's conjecture
• The resolution of Keller's conjecture
• Non-clausal redundancy properties
• Covered clauses are not propagation redundant
• Optimal-depth sorting networks
• A nonexistence certificate for projective planes of order ten with weight 15 codewords
• Strong extension-free proof systems
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML

Uses Software

• MiniSat
• Plingeling
• Glucose
• Treengeling
• kepler98
• Lingeling

This page was built for publication: Computer-aided proof of Erdős discrepancy properties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q892235)