Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer

DOI10.1007/978-3-319-40970-2_15zbMATH Open1403.68226arXiv1605.00723OpenAlexW2345876752WikidataQ55969534 ScholiaQ55969534MaRDI QIDQ2818017FDOQ2818017

Authors: Marijn J. H. Heule, Oliver Kullmann, Wiktor Marek 

Publication date: 5 September 2016

Published in: Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Abstract: The boolean Pythagorean Triples problem has been a longstanding open problem in Ramsey Theory: Can the set N = $1,2,\mathrm{...}$ 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.

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

Recommendations

• Formally verifying the solution to the Boolean Pythagorean triples problem
• Formally proving the Boolean Pythagorean triples conjecture
• scientific article; zbMATH DE number 1512149
• scientific article; zbMATH DE number 4131953
• scientific article; zbMATH DE number 4185387
• A new approach to generate all Pythagorean triples
• On the algorithm for generating Pythagorean triples
• Improved Lower Bounds for Testing Triangle-freeness in Boolean Functions via Fast Matrix Multiplication
• Boolean Reducts of Relation and Cylindric Algebras and the Cube Problem
• scientific article; zbMATH DE number 4012690

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Ramsey theory (05D10)

Cites Work

• Theory and Applications of Satisfiability Testing
• Title not available (Why is that?)
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theory and Applications of Satisfiability Testing
• Inprocessing rules
• Blocked clause elimination
• On a generalization of extended resolution
• Unit Refutations and Horn Sets
• Computing the van der Waerden number \(W(3,4)=293\)
• The van der Waerden NumberW(2, 6) Is 1132
• On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
• Title not available (Why is that?)
• Verifying Refutations with Extended Resolution
• A constraint-based approach to narrow search trees for satisfiability
• Expressing symmetry breaking in DRAT proofs
• Theory and Applications of Satisfiability Testing
• Compositional propositional proofs
• Theory and Applications of Satisfiability Testing

Cited In (53)

• Without loss of satisfaction
• Automated mathematical discovery and verification: minimizing pentagons in the plane
• Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
• Formally verifying the solution to the Boolean Pythagorean triples problem
• Propositional proof skeletons
• Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
• Inductive logic programming at 30
• A proof system for graph (non)-isomorphism verification
• Square Coloring Planar Graphs with Automatic Discharging
• Say no to case analysis: automating the drudgery of case-based proofs
• Deep cooperation of CDCL and local search for SAT
• Investigating the existence of Costas Latin squares via satisfiability testing
• XOR local search for Boolean Brent equations
• New ways to multiply \(3 \times 3\)-matrices
• Online over time processing of combinatorial problems
• Optimal symmetry breaking for graph problems
• Functional encryption for inner product with full function privacy
• Foundations for the Working Mathematician, and for Their Computer
• Ramsey properties of nonlinear Diophantine equations
• Finding Effective SAT Partitionings Via Black-Box Optimization
• How to get more out of your oracles
• Computing maximum unavoidable subgraphs using SAT solvers
• Simulating strong practical proof systems with extended resolution
• Preprocessing of propagation redundant clauses
• Preprocessing of propagation redundant clauses
• Rado's criterion over squares and higher powers
• Computer-aided constructions of commafree codes
• Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
• Title not available (Why is that?)
• A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture
• A flexible proof format for SAT solver-elaborator communication
• Unsatisfiability proofs for distributed clause-sharing SAT solvers
• On propositional coding techniques for the distinguishability of objects in finite sets
• The resolution of Keller's conjecture
• The resolution of Keller's conjecture
• DRAT proofs for XOR reasoning
• Some nonlinear Rado numbers
• Non-clausal redundancy properties
• Covered clauses are not propagation redundant
• Optimal-depth sorting networks
• Truth assignments as conditional autarkies
• Incompleteness, Undecidability and Automated Proofs
• A nonexistence certificate for projective planes of order ten with weight 15 codewords
• Strong extension-free proof systems
• Optimal bounds for the no-show paradox via SAT solving
• The SAT+CAS method for combinatorial search with applications to best matrices
• Formally proving the Boolean Pythagorean triples conjecture
• Formally proving size optimality of sorting networks
• Additive averages of multiplicative correlation sequences and applications
• Maker-breaker Rado games for equations with radicals
• Finding the hardest formulas for resolution
• Applying computer algebra systems with SAT solvers to the Williamson conjecture
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML

Uses Software

• kcnfs
• MiniSat
• Plingeling
• PicoSAT
• Flyspeck
• tawSolver
• DRAT-trim
• Treengeling
• Lingeling
• DRABT

This page was built for publication: Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer

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