Formally Verifying the Solution to the Boolean Pythagorean Triples Problem

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

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

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.

OriginalsprogEngelsk
TidsskriftJournal of Automated Reasoning
Vol/bind63
Udgave nummer3
Sider (fra-til)695-722
Antal sider28
ISSN0168-7433
DOI
StatusUdgivet - okt. 2019

Fingeraftryk

Coloring
Acoustic waves
Color

Citer dette

@article{65480451893c46ab82001c64b1fc711c,
title = "Formally Verifying the Solution to the Boolean Pythagorean Triples Problem",
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.",
keywords = "Interactive theorem proving, Large-scale proofs, SAT solving",
author = "Lu{\'i}s Cruz-Filipe and Joao Marques-Silva and Peter Schneider-Kamp",
year = "2019",
month = "10",
doi = "10.1007/s10817-018-9490-4",
language = "English",
volume = "63",
pages = "695--722",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer",
number = "3",

}

Formally Verifying the Solution to the Boolean Pythagorean Triples Problem. / Cruz-Filipe, Luís; Marques-Silva, Joao; Schneider-Kamp, Peter.

I: Journal of Automated Reasoning, Bind 63, Nr. 3, 10.2019, s. 695-722.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Formally Verifying the Solution to the Boolean Pythagorean Triples Problem

AU - Cruz-Filipe, Luís

AU - Marques-Silva, Joao

AU - Schneider-Kamp, Peter

PY - 2019/10

Y1 - 2019/10

N2 - 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.

AB - 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.

KW - Interactive theorem proving

KW - Large-scale proofs

KW - SAT solving

U2 - 10.1007/s10817-018-9490-4

DO - 10.1007/s10817-018-9490-4

M3 - Journal article

VL - 63

SP - 695

EP - 722

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 3

ER -