We prove depth optimality of sorting networks from “The Art of Computer Programming”.

Sorting networks posses symmetry that can be used to generate a few representatives.

These representatives can be efficiently encoded using regular expressions.

We construct SAT formulas whose unsatisfiability is sufficient to show optimality.

Resulting algorithm is orders of magnitude faster than prior work on small instances.