[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Formally Verifying the Solution to the Boolean Pythagorean Triples Problem

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

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

  2. The constants and , inhabiting the type , are distinguished in Coq from the singleton type and the empty type , which are logical propositions inhabiting the sort .

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

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

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

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

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

  8. Declaring a function of type as a coercion means that Coq applies it automatically whenever it expects a term of type and one of type is given. In order to guarantee termination, no composition of coercions may map a type to itself.

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

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

References

  1. 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)

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

    Book  MATH  Google Scholar 

  3. 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)

    Article  MathSciNet  MATH  Google Scholar 

  4. 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)

    Google Scholar 

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

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

    Article  MathSciNet  MATH  Google Scholar 

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

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

    Article  MathSciNet  MATH  Google Scholar 

  9. 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)

    Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

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

    Article  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

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

Download references

Acknowledgements

The authors would like to thank Marijn Heule for providing some valuable insights, namely regarding the mathematical interpretation of the simplification procedure used in [18]. This work was partially supported by the Danish Council for Independent Research, Natural Sciences, Grant DFF-1323-00247.

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, University of Southern Denmark, Campusvej 55, 5230, Odense M, Denmark

    Luís Cruz-Filipe & Peter Schneider-Kamp

  2. LaSIGE, Faculty of Science, University of Lisbon, Lisbon, Portugal

    Joao Marques-Silva

Authors
  1. Luís Cruz-Filipe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joao Marques-Silva
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter Schneider-Kamp
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Luís Cruz-Filipe.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Cruz-Filipe, L., Marques-Silva, J. & Schneider-Kamp, P. Formally Verifying the Solution to the Boolean Pythagorean Triples Problem. J Autom Reasoning 63, 695–722 (2019). https://doi.org/10.1007/s10817-018-9490-4

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-018-9490-4

Keywords

Mathematics Subject Classification

Search

Navigation