Optimal-depth sorting networks
作者：
Highlights：
• 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.
摘要
•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.
论文关键词：Sorting networks,SAT solving,Symmetry breaking
论文评审过程：Received 6 February 2015, Revised 20 August 2016, Accepted 22 September 2016, Available online 11 October 2016, Version of Record 14 November 2016.
论文官网地址：https://doi.org/10.1016/j.jcss.2016.09.004
