Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer

Abstract

The boolean Pythagorean Triples problem has been a longstanding open problem in Ramsey Theory: Can the set N = $\{1,2,...\}$ of natural numbers be divided into two parts, such that no part contains a triple $(a,b,c)$ with $a^2+b^2=c^2$ ? A prize for the solution was offered by Ronald Graham over two decades ago. We solve this problem, proving in fact the impossibility, by using the Cube-and-Conquer paradigm, a hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers. An important role is played by dedicated look-ahead heuristics, which indeed allowed to solve the problem on a cluster with 800 cores in about 2 days. Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, which is almost 200 terabytes in size. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking.

References in corpus (3)

• On the van der Waerden numbers w(2;3,t)
• Symbiosis of Search and Heuristics for Random 3-SAT
• Coloring so that no Pythagorean Triple is Monochromatic

Cited by in corpus (29)

• Efficient Certified RAT Verification
• Computer-inspired Quantum Experiments
• Efficient Certified Resolution Proof Checking
• Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture
• Parallelization Techniques for Verifying Neural Networks
• Computing Spectra -- On the Solvability Complexity Index Hierarchy and Towers of Algorithms
• SAT-based Encodings for Optimal Decision Trees with Explicit Paths
• Optimal-Depth Sorting Networks
• Design of quantum optical experiments with logic artificial intelligence
• Computing Small Unit-Distance Graphs with Chromatic Number 5
• Learning definable hypotheses on trees
• A SAT-based Resolution of Lam's Problem
• A Flexible Proof Format for SAT Solver-Elaborator Communication
• Guiding High-Performance SAT Solvers with Unsat-Core Predictions
• Verifier Theory and Unverifiability
• New ways to multiply 3 x 3-matrices
• The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices
• A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples
• SAT and Lattice Reduction for Integer Factorization
• SAT-Encodings for Treecut Width and Treedepth
• Consistent Answers of Aggregation Queries using SAT Solvers
• Too much information: why CDCL solvers need to forget learned clauses
• Partition regularity of Pythagorean pairs
• Additive averages of multiplicative correlation sequences and applications
• Complexity of Fermionic 2-SAT
• Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
• Rado Numbers and SAT Computations
• Exploiting Isomorphic Subgraphs in SAT (Long version)
• Properties and Extensions of Alternating Path Relevance - I