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

DOI10.1007/978-3-319-40970-2_15MaRDI QIDQ2818017zbMATH OpenOpenAlexWikidataFDO

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)

Full work available at URL https://arxiv.org/abs/1605.00723, https://cronfa.swan.ac.uk/Record/cronfa28694/Download/0028694-06062016010529.pdf

Mathematics Subject Classification ID

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

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.

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

Cites work

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

Cited in

(53)

• 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
• Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
• Inductive logic programming at 30
• Propositional proof skeletons
• 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
• Ramsey properties of nonlinear Diophantine equations
• Foundations for the Working Mathematician, and for Their Computer
• How to get more out of your oracles
• Finding Effective SAT Partitionings Via Black-Box Optimization
• 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
• Without loss of satisfaction
• 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
• A flexible proof format for SAT solver-elaborator communication
• scientific article; zbMATH DE number 7566059 (Why is no real title available?)
• A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture
• On propositional coding techniques for the distinguishability of objects in finite sets
• DRAT proofs for XOR reasoning
• Unsatisfiability proofs for distributed clause-sharing SAT solvers
• The resolution of Keller's conjecture
• The resolution of Keller's conjecture
• Some nonlinear Rado numbers
• Non-clausal redundancy properties
• Optimal-depth sorting networks
• Covered clauses are not propagation redundant
• Truth assignments as conditional autarkies
• A nonexistence certificate for projective planes of order ten with weight 15 codewords
• Incompleteness, Undecidability and Automated Proofs
• Optimal bounds for the no-show paradox via SAT solving
• Strong extension-free proof systems
• Automated mathematical discovery and verification: minimizing pentagons in the plane
• 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
• Applying computer algebra systems with SAT solvers to the Williamson conjecture
• Additive averages of multiplicative correlation sequences and applications
• Finding the hardest formulas for resolution
• Maker-breaker Rado games for equations with radicals
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML

Describes a project that uses

Uses Software

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

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)