Computer Science & AI

We investigate the existence of sorting networks with fewer comparators or smaller depth than the best-known constructions for input sizes n ∈ {13,…,17}. We combine three approaches: (1) isomorphism-pruned SAT encodings that canonicalize the first layer of comparators up to input permutation, (2) incremental pruning via reachable-state propagation from the zero-one principle, and (3) reinforcement-learning-guided comparator placement to explore non-recursive network topologies. Despite extensive search, we did not find a network improving on the best-known comparator counts (45, 51, 56, 60, 71 for n = 13,…,17, respectively) or depths. We did, however, reproduce and machine-verify all best-known constructions via exhaustive zero-one checking. Our SAT search for n = 13 with k = 44 comparators covered only a subset of symmetry-reduced first-layer configurations (31 of 47), returning UNSAT for those branches but leaving the remaining 16 unresolved due to timeout; we therefore cannot claim even a partial optimality result. We provide all candidate networks and verification scripts as machine-checkable artifacts. This paper is an honest report of a negative result with methodological contributions whose practical impact remains limited.