Formally Verifying the Solution to the Boolean Pythagorean Triples Problem

Luís Cruz-Filipe*, Joao Marques-Silva, Peter Schneider-Kamp

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

The Boolean Pythagorean Triples problem asks: does there exist a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? This problem was first solved in 2016, when Heule, Kullmann and Marek encoded a finite restriction of this problem as a propositional formula and showed its unsatisfiability. In this work we formalize their development in the theorem prover Coq. We state the Boolean Pythagorean Triples problem in Coq, define its encoding as a propositional formula and establish the relation between solutions to the problem and satisfying assignments to the formula. We verify Heule et al.’s proof by showing that the symmetry breaks they introduced to simplify the propositional formula are sound, and by implementing a correct-by-construction checker for proofs of unsatisfiability based on reverse unit propagation.

Original languageEnglish
JournalJournal of Automated Reasoning
Volume63
Issue number3
Pages (from-to)695-722
Number of pages28
ISSN0168-7433
DOIs
Publication statusPublished - Oct 2019

    Fingerprint

Keywords

  • Interactive theorem proving
  • Large-scale proofs
  • SAT solving

Cite this