Formally Proving the Boolean Triples Conjecture

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

31 Downloads (Pure)

Abstract

In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered. In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular n implies that there does not exist a solution to the problem. We then formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability and the logical argument underlying cube-and-conquer, obtaining a verified proof of Heule et al.’s solution.
Original languageEnglish
Title of host publicationProceedings of LPAR-21 : 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
EditorsThomas Eiter, David Sands
PublisherEasyChair Publications
Publication date2017
Pages509-522
DOIs
Publication statusPublished - 2017
Event21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Maun, Botswana
Duration: 7 May 201712 May 2017
Conference number: 21

Conference

Conference21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Number21
CountryBotswana
CityMaun
Period07/05/201712/05/2017
SeriesEPiC Series in Computing
Volume46
ISSN2398-7340

Fingerprint

Pythagorean
Natural numbers
Coloring
Encoding
Logic
Simplification
Formalization

Cite this

Cruz-Filipe, L., & Schneider-Kamp, P. (2017). Formally Proving the Boolean Triples Conjecture. In T. Eiter, & D. Sands (Eds.), Proceedings of LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 509-522). EasyChair Publications. EPiC Series in Computing, Vol.. 46 https://doi.org/10.29007/jvdj
Cruz-Filipe, Luis ; Schneider-Kamp, Peter. / Formally Proving the Boolean Triples Conjecture. Proceedings of LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. editor / Thomas Eiter ; David Sands. EasyChair Publications, 2017. pp. 509-522 (EPiC Series in Computing, Vol. 46).
@inproceedings{e51a8ddd9752469b8270a08eb90cc8dc,
title = "Formally Proving the Boolean Triples Conjecture",
abstract = "In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered. In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular n implies that there does not exist a solution to the problem. We then formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability and the logical argument underlying cube-and-conquer, obtaining a verified proof of Heule et al.’s solution.",
author = "Luis Cruz-Filipe and Peter Schneider-Kamp",
year = "2017",
doi = "10.29007/jvdj",
language = "English",
pages = "509--522",
editor = "Thomas Eiter and David Sands",
booktitle = "Proceedings of LPAR-21",
publisher = "EasyChair Publications",

}

Cruz-Filipe, L & Schneider-Kamp, P 2017, Formally Proving the Boolean Triples Conjecture. in T Eiter & D Sands (eds), Proceedings of LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EasyChair Publications, EPiC Series in Computing, vol. 46, pp. 509-522, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 07/05/2017. https://doi.org/10.29007/jvdj

Formally Proving the Boolean Triples Conjecture. / Cruz-Filipe, Luis; Schneider-Kamp, Peter.

Proceedings of LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. ed. / Thomas Eiter; David Sands. EasyChair Publications, 2017. p. 509-522.

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

TY - GEN

T1 - Formally Proving the Boolean Triples Conjecture

AU - Cruz-Filipe, Luis

AU - Schneider-Kamp, Peter

PY - 2017

Y1 - 2017

N2 - In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered. In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular n implies that there does not exist a solution to the problem. We then formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability and the logical argument underlying cube-and-conquer, obtaining a verified proof of Heule et al.’s solution.

AB - In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered. In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular n implies that there does not exist a solution to the problem. We then formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability and the logical argument underlying cube-and-conquer, obtaining a verified proof of Heule et al.’s solution.

U2 - 10.29007/jvdj

DO - 10.29007/jvdj

M3 - Article in proceedings

SP - 509

EP - 522

BT - Proceedings of LPAR-21

A2 - Eiter, Thomas

A2 - Sands, David

PB - EasyChair Publications

ER -

Cruz-Filipe L, Schneider-Kamp P. Formally Proving the Boolean Triples Conjecture. In Eiter T, Sands D, editors, Proceedings of LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EasyChair Publications. 2017. p. 509-522. (EPiC Series in Computing, Vol. 46). https://doi.org/10.29007/jvdj