论文标题
11和12个频道的Bose-Nelson排序问题的答案
An Answer to the Bose-Nelson Sorting Problem for 11 and 12 Channels
论文作者
论文摘要
我们表明,11通道排序网络至少具有35个比较器,而12个通道排序网络至少具有39个比较器。这积极地解决了计算机编程卷中给出的相应排序网络的最佳性。 3并关闭了Bose-Nelson分类问题的两个最小的开放实例。我们通过概括从分类网络到更一般的比较器网络类别的结果来获得这些界限。由此,我们得出了一种动态编程算法,该算法计算具有给定数量的通道数的分类网络的最佳大小。从该算法的执行中,我们构建了一个包含相应尺寸绑定的派生的证书,我们使用使用Isabelle/Hol Proof Assistant正式验证的程序检查该证书。
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.