We show that 11-channel sorting networks have at least 35 comparators and that 12-channel sorting networks have at least 39 comparators. This positively settles the optimality of the corresponding sorting networks given in The Art of Computer Programming vol. 3 and closes the two smallest open instances of the Bose-Nelson sorting problem. We obtain these bounds by generalizing a result of Van Voorhis from sorting networks to a more general class of comparator networks. From this we derive a dynamic programming algorithm that computes the optimal size for a sorting network with a given number of channels. From an execution of this algorithm we construct a certificate containing a derivation of the corresponding lower size bound, which we check using a program formally verified using the Isabelle/HOL proof assistant.
翻译:我们显示,11个频道分类网络至少有35个比较者,12个频道分类网络至少有39个比较者。这积极解决了《计算机编程艺术》第3卷中给出的相应分类网络的最佳性,并关闭了Bose-Nelson分类问题中两个最小的开放实例。我们通过将Van Voorhis的分类网络结果推广到一个比较者网络的更一般的类别来获得这些界限。我们从中得出一个动态的编程算法,该算法用一定数量的频道来计算一个分类网络的最佳大小。我们通过执行这一算法,建立了一个包含相应较小尺寸约束的衍生物的证书,我们用Isabel/HOL验证助理正式核实的程序检查。