Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker

TL;DR

This paper formalizes the theory of size-optimal sorting networks and develops a certified checker that verifies proofs of optimality for networks with up to 8 inputs, leveraging an untrusted oracle for efficiency.

Contribution

It introduces a formalized framework for size-optimal sorting networks and provides a certified proof checker capable of handling large proof searches efficiently.

Findings

Successfully verifies proofs of optimality for up to 8-input sorting networks.

Utilizes an untrusted oracle to efficiently handle over 1.6 million NP-complete subproblems.

Demonstrates the practicality of formalized proof verification in complex combinatorial problems.

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.