Abstract
Since the proof of the four color theorem in 1976, computer-generated proofs have become a reality in mathematics and computer science. During the last decade, we have seen formal proofs using verified proof assistants being used to verify the validity of such proofs.
In this paper, we describe a formalized theory of size-optimal sorting networks. From this formalization we extract a certified checker that successfully verifies computer-generated proofs of optimality on up to 8 inputs. The checker relies on an untrusted oracle to shortcut the search for witnesses on more than 1.6 million NP-complete subproblems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The logs and the Java verifier are available at http://imada.sdu.dk/~petersk/sn/.
- 2.
Comparator (i, j) in comparator network \(C;(i,j);C'\) is redundant if \({\varvec{x}}_i<{\varvec{x}}_j\) for all \({\varvec{x}}\in \mathsf {outputs}(C)\) – in other words, (i, j) never changes its inputs.
References
Appel, K., Haken, W.: Every planar map is four colorable. Part I: discharging. Ill. J. Math. 21, 429–490 (1977)
Appel, K., Haken, W., Koch, J.: Every planar map is four colorable. Part II: reducibility. Ill. J. Math. 21, 491–567 (1977)
Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. Trans. A Roy. Soc. 363(1835), 2351–2375 (2005)
Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.): ITP 2013. LNCS, vol. 7998. Springer, Heidelberg (2013)
Claret, G., González-Huesca, L.C., Régis-Gianas, Y., Ziliani, B.: Lightweight proof by reflection using a posteriori simulation of effectful computation. In Blazy et al. [4], pp. 67–83
Codish, M., Cruz-Filipe, L., Frank, M., Schneider-Kamp, P.: Twenty-five comparators is optimal when sorting nine inputs (and twenty-nine for ten). In: ICTAI 2014, pp. 186–193. IEEE (2014)
Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: Schmidt-Schauß, M., (ed.) RTA 2011. LIPIcs, vol. 10, pp. 21–30. Schloss Dagstuhl (2011)
Cruz-Filipe, L., Schneider-Kamp, P.: Optimizing a certified proof checker for a large-scale computer-generated proof. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 55–70. Springer, Heidelberg (2015)
Floyd, R.W., Knuth, D.E.: The Bose-Nelson sorting problem. In: Srivastava, J.N. (ed.) A Survey of Combinatorial Theory, pp. 163–172. North-Holland, Amsterdam (1973)
Fouilhe, A., Monniaux, D., Périn, M.: Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 345–365. Springer, Heidelberg (2013)
Gonthier, G.: Formal proof - the four-color theorem. Not. AMS 55(11), 1382–1393 (2008)
Knuth, D.E.: The Art of Computer Programming. Sorting and Searching, vol. 3. Addison-Wesley, Reading (1973)
Konev, B., Lisitsa, A.: A SAT attack on the Erdős discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 219–226. Springer, Heidelberg (2014)
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)
Parberry, I.: A computer-assisted optimal depth lower bound for nine-input sorting networks. Math. Syst. Theor. 24(2), 101–116 (1991)
Sternagel, C., Thiemann, R.: The certification problem format. In: Benzmüller, C., Paleo, B.W. (eds.) UITP 2014. EPTCS, vol. 167, pp. 61–72 (2014)
Thiemann, R.: Formalizing bounded increase. In: Blazy et al. [4], pp. 245–260
van Voorhis, D.C.: Toward a lower bound for sorting networks. In: Miller, R.E., Thatcher, J.W. (eds.) Complexity of Computer Computations. The IBM Research Symposia Series, pp. 119–129. Plenum Press, New York (1972)
Acknowledgements
We would like to thank Femke van Raamsdonk, whose initial skepticism about our informal proof inspired this work, and Michael Codish for his support and his enthusiasm about sorting networks. The authors were supported by the Danish Council for Independent Research, Natural Sciences. Computational resources were generously provided by the Danish Center for Scientific Computing.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Cruz-Filipe, L., Schneider-Kamp, P. (2015). Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker. In: Urban, C., Zhang, X. (eds) Interactive Theorem Proving. ITP 2015. Lecture Notes in Computer Science(), vol 9236. Springer, Cham. https://doi.org/10.1007/978-3-319-22102-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-22102-1_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22101-4
Online ISBN: 978-3-319-22102-1
eBook Packages: Computer ScienceComputer Science (R0)