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

Originalsprog | Engelsk |
---|---|

Tidsskrift | Journal of Automated Reasoning |

Vol/bind | 63 |

Udgave nummer | 3 |

Sider (fra-til) | 695-722 |

Antal sider | 28 |

ISSN | 0168-7433 |

DOI | |

Status | Udgivet - okt. 2019 |

### Fingeraftryk

### Citer dette

*Journal of Automated Reasoning*,

*63*(3), 695-722. https://doi.org/10.1007/s10817-018-9490-4

}

*Journal of Automated Reasoning*, bind 63, nr. 3, s. 695-722. https://doi.org/10.1007/s10817-018-9490-4

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

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › peer 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 -