Top

Journal of Automated Reasoning

Published in:

27-10-2018

Formally Verifying the Solution to the Boolean Pythagorean Triples Problem

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

Published in: Journal of Automated Reasoning | Issue 3/2019

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

previous article Classification of Finite Fields with Applications

next article Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

This would require both the SAT solver and the checker to be flawed in a similar way, which is unlikely given that they were developed independently.

The constants

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9490-4/MediaObjects/10817_2018_9490_Figae_HTML.gif

and

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9490-4/MediaObjects/10817_2018_9490_Figaf_HTML.gif

, inhabiting the type

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9490-4/MediaObjects/10817_2018_9490_Figag_HTML.gif

, are distinguished in Coq from the singleton type

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9490-4/MediaObjects/10817_2018_9490_Figah_HTML.gif

and the empty type

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9490-4/MediaObjects/10817_2018_9490_Figai_HTML.gif

, which are logical propositions inhabiting the sort

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9490-4/MediaObjects/10817_2018_9490_Figaj_HTML.gif

Expressing this property as a predicate, rather than as a record type, simplifies our development.

This simple argument was communicated informally by Marijn Heule. To the best of our knowledge, it has not been published elsewhere.

This value was originally chosen because 2520 is the number that occurs most often in the triples after simplification, hence the potential for simplification was highest.

This is a sanity check, but it is nice that we can perform it using certified code.

Practical measurements show that these depths are at most approximately 150, for CNFs containing just under 15,000 clauses. Although this is much higher than for a perfectly balanced tree, it suffices for practical purposes, and allows us to avoid formalizing a balancing algorithm. See [8] for a similar discussion.

Declaring a function of type

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9490-4/MediaObjects/10817_2018_9490_Figiu_HTML.gif

as a coercion means that Coq applies it automatically whenever it expects a term of type

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9490-4/MediaObjects/10817_2018_9490_Figiv_HTML.gif

and one of type

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9490-4/MediaObjects/10817_2018_9490_Figiw_HTML.gif

is given. In order to guarantee termination, no composition of coercions may map a type to itself.

In principle, this approach could break soundness of extraction; we are using the fact that these constructs behave as identities. Targeting a lazy language like Haskell would not require this workaround; however, our experiments showed that using OCaml instead of Haskell reduced computation times to around one-fourth.

The modified version of drat-trim from [9] is slightly slower than the original, due to the need to generate more detailed proofs.

Anand, A., Appel, A.W., Morrisett, G., Paraskevopoulou, Z., Pollack, R., Bélanger, O.S., Sozeau, M., Weaver, M.: CertiCoq: a verified compiler for Coq. In: CoqPL Workshop (2017)

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)CrossRefMATH

Blanqui, F., Koprowski, A.: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21, 827–859 (2011)MathSciNetCrossRefMATH

Cook, S.A.: The complexity of theorem-proving procedures. In: Harrison, M.A., Banerji, R.B., Ullman, J.D. (eds.) STOC, pp. 151–158. ACM, New York (1971)

Cooper, J., Overstreet, R.: Coloring so that no pythagorean triple is monochromatic. CoRR arXiv:1505.02222 (2015)

Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2/3), 95–120 (1988)MathSciNetCrossRefMATH

Cruz-Filipe, L., Heule, M.J.H., Jr., W.A.H., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura [14], pp. 220–236

Cruz-Filipe, L., Larsen, K.S., Schneider-Kamp, P.: Formally proving size optimality of sorting networks. J. Autom. Reason. 59(4), 425–454 (2017)MathSciNetCrossRefMATH

Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: TACAS, LNCS, vol. 10205. Springer (2017)

10.

Cruz-Filipe, L., Schneider-Kamp, P.: Formally verifying the Boolean pythagorean triples conjecture. In: Eiter and Sands [15], pp. 509–522

11.

Cruz-Filipe, L., Wiedijk, F.: Hierarchical reflection. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs, LNCS, vol. 3223, pp. 66–81. Springer, Heidelberg (2004)

12.

Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-strength certified SAT solving through verified SAT proof checking. In: ICTAC, LNCS, vol. 6255, pp. 260–274. Springer (2010)

13.

Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5, 394–397 (1962)MathSciNetCrossRefMATH

14.

de Moura, L. (ed.): Automated Deduction—CADE 26—26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings, LNCS, vol. 10395. Springer (2017)

15.

Eiter, T., Sands, D. (eds.): LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 7–12th May 2017, EPiC Series, vol. 46. EasyChair (2017)

16.

Fouilhé, A., Monniaux, D., Périn, M.: Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Logozzo, F., Fähndrich, M. (eds.) SAS, LNCS, vol. 7935, pp. 345–365. Springer, Heidelberg (2013)

17.

Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE, pp. 10,886–10,891 (2003)

18.

Heule, M., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT, LNCS, vol. 9710, pp. 228–245. Springer, Heidelberg (2016)

19.

Heule, M., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC, LNCS, vol. 7261, pp. 50–65. Springer, Heidelberg (2012)

20.

Järvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS, LNCS, vol. 6015, pp. 129–144. Springer, Heidelberg (2010)

21.

Konev, B., Lisitsa, A.: Computer-aided proof of erdős discrepancy properties. Artif. Intell. 224, 103–118 (2015)CrossRefMATH

22.

Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de Moura [14], pp. 237–254

23.

Landman, B.M., Robertson, A.: Ramsey Theory on the Integers. The Student Mathematical Library, vol. 24. AMS (2004)

24.

Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef

25.

Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds.) CiE 2008, LNCS, vol. 5028, pp. 359–369. Springer, Heidelberg (2008)

26.

Mijnders, S., de Wilde, B., Heule, M.: Symbiosis of search and heuristics for random 3-SAT. In: Mitchell, D.G., Ternovska, E. (eds.) Proceedings of LaSh 2010 (2010)

27.

Philipp, T., Rebola-Pardo, A.: Towards a semantics of unsatisfiability proofs with inprocessing. In: Eiter and Sands [15], pp. 65–84

28.

Rebola-Pardo, A., Biere, A.: Two flavours of DRAT. In: Pragmatics of SAT 2018 (2018)

29.

Silva, J.P.M., Sakallah, K.A.: Conflict analysis in search algorithms for satisfiability. In: ICTAI, pp. 467–469. IEEE Computer Society (1996)

30.

Sternagel, C., Thiemann, R.: The certification problem format. In: C. Benzmüller, B.W. Paleo (eds.) UITP, EPTCS, vol. 167, pp. 61–72 (2014)

31.

Wetzler, N.D., Heule, M.J., Hunt Jr., W.A.: Mechanical verification of SAT refutations with extended resolution. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP, LNCS, vol. 7998, pp. 229–244. Springer, Heidelberg (2013)

32.

Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS, vol. 3600. Springer (2006)

Title: Formally Verifying the Solution to the Boolean Pythagorean Triples Problem
Authors: Luís Cruz-Filipe
Joao Marques-Silva
Peter Schneider-Kamp
Publication date: 27-10-2018
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 3/2019
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-9490-4

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 3/2019

Mechanized Metatheory Revisited

An Isabelle/HOL Formalisation of Green’s Theorem

Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF

Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation

A PSpace Algorithm for Acyclic Epistemic DL

Formalization of Geometric Algebra in HOL Light

Premium Partner