PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek

arXiv:1605.00723v1cs.DMcs.LO

TL;DR

The paper asks whether the natural numbers can be divided into two parts with no monochromatic Pythagorean triple. It solves the problem with Cube-and-Conquer SAT solving and formal DRAT verification, proving avoidance possible through 7824 but impossible at 7825.

  • Problem

    The central problem is whether the natural numbers can be partitioned into two parts so that neither part contains a Pythagorean triple.

  • Method

    The paper combines look-ahead splitting with CDCL solving in Cube-and-Conquer and uses DRAT proofs to formally verify unsatisfiability.

  • Results

    7824 admits a two-part Pythagorean-triple-free partition, whereas such a partition is impossible for 7825.

  • Takeaways & Limitations

    The result establishes the boolean Pythagorean triples partition theorem and demonstrates SAT-based computation of Ramsey-theoretic numbers.

  • Takeaways & Limitations

    The unsatisfiability proof is extremely large, requiring significant compression even to store and share it.

Abstract

from arXiv · show

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.

1 Introduction

The paper applies SAT to Ramsey-theoretic configuration problems and resolves the boolean Pythagorean triples partition problem. It proves that two-partition avoidance is possible through 7824 but impossible at 7825, using SAT formulations and formal proof verification.

  • SAT represents finite-domain constraint problems and is used here to compute configurations in extremal combinatorics and Ramsey theory.
  • The paper contributes both the boolean Pythagorean triples partition theorem and methods for computing Ramsey-theoretic numbers with SAT solvers.
  • 7825 cannot be partitioned into two parts without a Pythagorean triple in at least one part.
  • The result addresses a problem for which Graham repeatedly offered a $100 prize and whose solution was not merely numerical detail from SAT.
  • The authors prove the theorem by encoding the satisfiable case n = 7824 and the unsatisfiable case n = 7825 as two SAT problems.

2 Preliminaries

This section introduces CNF formulas, assignments, satisfiability-preserving transformations, resolution, unit propagation, and RAT clauses as foundations for SAT proof checking.

  • A CNF formula is a conjunction of clauses, with literals representing Boolean variables or their negations.
  • A formula is unsatisfiable when it contains the empty clause or when no assignment satisfies all its clauses.
  • Clause addition is unsat-preserving, while clause elimination is sat-preserving; transformations can therefore preserve satisfiability or unsatisfiability in different directions.
  • Resolution and Extended Resolution: Resolution derives a clause from two clauses containing complementary literals, while extension introduces a variable defined as the conjunction of two literals.
  • Unit Propagation: Unit propagation repeatedly simplifies clauses using unit literals and derives a conflict from complementary units.
  • Asymmetric tautologies generalize resolvent additions through unit propagation and correspond to clauses derivable by input resolution.
  • RAT clauses: RAT clauses extend sat-preserving additions beyond logically implied clauses, and their validity is tested against clauses containing the pivot's negation.

3 Proofs of Unsatisfiability

The paper describes unsatisfiability proofs as sequences of satisfiability-preserving clause operations and uses DRAT to formalize SAT-solver refutations.

  • Unsatisfiability proofs end with a formula containing the empty clause after a sequence of sat-preserving transitions.
  • Figure 1 contrasts DIMACS CNF input with a DRAT refutation whose lines encode additions, deletions, and RAT-pivot requirements.
  • Clausal proof formats allow both clause additions and deletions, including additions that are not logically implied but remain sat-preserving.
  • A DRAT proof consists of clause additions and deletions, with each addition required to be a RAT clause or an empty clause justified by unit propagation.
  • DRAT refutations are correct unsatisfiability proofs, checkable in cubic time, and have power equivalent up to polynomial transformations to Extended Resolution.

4 Cube-and-Conquer Solving

Cube-and-Conquer combines look-ahead splitting with CDCL solving to partition hard SAT instances into subproblems that can be solved in parallel or incrementally.

  • Cube-and-Conquer uses a look-ahead solver to split a problem into cubes and a CDCL solver to conquer the resulting subproblems.
  • Look-ahead heuristics make global splitting decisions, whereas CDCL heuristics handle local decisions and short refutations.
  • The two C&C variants trade parallel solving of individual cubes against reuse of heuristics and learned clauses across multiple cubes.
  • The computation first split the problem into 106 cubes, then split each cube into billions of sub-cubes solved sequentially by an incremental SAT solver.

5 Solving the boolean Pythagorean Triples Problem

The framework encodes the Pythagorean Triples problem as SAT, transforms the encoding, splits it into subproblems, solves them, and validates the resulting proofs.

  • The five phases are encode, transform, split, solve, and validate.Encoding validates the SAT representation, while transformation reduces later computational costs.
  • 5 Solving the boolean Pythagorean Triples Problem: Formula F_n represents whether numbers up to n can be partitioned into two parts avoiding monochromatic Pythagorean triples.Boolean variable x_i records the part containing i, and constraints are added for each triple satisfying a^2 + b^2 = c^2.
  • Blocked clause elimination removes constraints whose variables occur only there, repeatedly applying the resulting reductions to a fixpoint.This transformation is one of the two transformations applied to the encodings.
  • Symmetry breaking fixes a frequently occurring variable, x_2520, to true because the two partition parts are interchangeable.The chosen variable was the most frequent in the formulas used during the experiments.
  • Bounded variable elimination was omitted because experiments increased solving times and it harmed specialized 3-SAT look-ahead heuristics.The transformation also changes the problem into a non-3-SAT formula.

5.3 Split

The split phase partitions the transformed formula into many cube-defined subproblems using global look-ahead heuristics specialized for the Pythagorean Triples encoding.

  • 5.3 Split: The split phase produces a binary branching tree whose leaves represent subproblems formed by adding the path decisions as unit clauses.The corresponding cubes are conjunctions of the decisions leading to each leaf.
  • Look-ahead assigns a variable, performs unit propagation, and measures formula changes to guide splitting decisions.Expected future gains from newly produced short clauses are more important than current reductions.
  • Figure 3 pairs decision-variable branching with an inccnf cube file, where edge polarity determines literal sign and each cube ends with 0.The prefix a denotes assumptions; positive and negative numbers represent positive and negative literals.
  • The specialized heuristic refines the default C&C weighting scheme with a method adapted from random 3-SAT.This refinement was more powerful for the Pythagorean Triples encoding.

5.4 Details regarding the heuristics

The splitting heuristics estimate how strongly literals are forced through propagation, normalize these values iteratively, and use bounded parameters tailored to this problem.

  • 5.4 Details regarding the heuristics: Look-ahead heuristic values h_i(l) approximate how strongly literal l is forced true by clauses containing it through unit propagation.The initial values are h_0(x) = h_0(¯x) = 1 for every variable.
  • At each level, the average μ_i scales heuristic values, while later iterations weight literals y by h_i(¯y)/μ_i.The recurrence also uses the relative weight γ of binary clauses.
  • At every branching-tree node, the solver computes h(l) := h_4(l) for all literals occurring in the formula.The branching variable is selected using the product of the heuristic values for its two polarities.
  • The tuned parameters are α = 8, β = 550, and γ = 25, differing substantially from values reported as optimal for random 3-SAT.Here α and β bound heuristic values, while γ expresses the relative importance of binary clauses.

5.5 Solve

The solve phase applies SAT solvers to the cube-defined subproblems and emits proofs, while the validation phase checks the encoding and combines the proof components into a refutation.

  • 5.5 Solve: The solve phase takes the transformed formula and cube files as input and produces an unsatisfiability proof.Easy and hard problems use different solving approaches, with hard problems requiring partitioning into many cubes.
  • Approximately 4 CPU years were required for F7825, including 21,900 CPU hours for splitting and 13,200 CPU hours for solving.The problem was partitioned into 10^6 subproblems and therefore solved in parallel.
  • Learned clauses from one cube can be reused when solving another cube.
  • Each subproblem produces a DRAT refutation, and combining them requires extending generated lemmas with the negated cube clause ¬ϕ_i.The resulting subproblem proofs can then contribute to a proof for F7825.
  • Validation checks the SAT encoding and the transformation, cube, and tautology DRAT proofs.The proof components are merged in the order transformation proof, cube proofs, then tautology proof.

Transformation Proof

The validation framework checks cube coverage and verifies each subproblem’s unsatisfiability, but the resulting DRAT proof is too large to distribute directly.

  • 106 cube proofs were generated and validated by checking whether each cube’s negation is implied by the transformed formula.
  • Almost 200 terabytes of DRAT proofs were compressed to 14 terabytes, so the authors instead provide 68 gigabytes of compressed cube files.
  • The cube files let glucose 3.0 reproduce the DRAT proofs, while checking them requires about 16,000 CPU hours.
  • The complete search space is validated by proving that the disjunction of cubes is a tautology.

6 Results

The experiments use dedicated look-ahead heuristics to split the problem into 106 subproblems, then compare cube-and-conquer with alternative solving strategies and analyze the resulting subproblems.

  • 6.2 Cube and Conquer: 35,000 CPU hours was the estimated runtime after optimizing march cc’s heuristic, down from roughly 300,000 CPU hours.
  • 6.2 Cube and Conquer: 800 cores were used to split the transformed formula into exactly 106 subproblems, keeping most conquer runtimes below two minutes.
  • 6.2 Cube and Conquer: The selected cubes ranged from size 12 to 49, with average cube and conquer runtime peaks around sizes 24 and 26, respectively.
  • 6.2 Cube and Conquer: 78.87, 47.52, and 60.62 seconds were the average cube, conquer, and validation times for the 106 subproblems, respectively.
  • 6.2 Cube and Conquer: Cube-and-conquer clearly outperformed pure CDCL and was about twice as fast as pure look-ahead on average.
  • 6.3 Extreme Solutions: Only one of the 106 subproblems was satisfiable for n = 7824, and the corresponding formula had a backbone of 2304 variables.
  • 6.3 Extreme Solutions: A satisfying assignment for F7824 assigned 4925 of the 6492 variables occurring in the formula, indicating many solutions.

7 Conclusions

The paper reports a solved and verified result obtained with cube-and-conquer, enabled by parallel computation and dedicated look-ahead heuristics. It also emphasizes community-checkable certificates and asks whether a human-readable proof exists.

  • The problem was solved and verified using cube-and-conquer, requiring about 35,000 solving hours and 16,000 verification hours.
  • Parallelization reduced the elapsed computation to about two days on the Stampede cluster.
  • The authors argue that difficult computational results should provide certificates that the community can validate.
  • Future work targets look-ahead heuristics that operate effectively on hard combinatorial problems without manual tuning.
Loading 1605.00723v1…