Sorting nine inputs requires twenty-five comparisons

DOI10.1016/j.jcss.2015.11.014zbMath1333.68087OpenAlexW2208979138MaRDI QIDQ899586

Peter Schneider-Kamp, Luís Cruz-Filipe, Michael Codish, Michael Frank

Publication date: 30 December 2015

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jcss.2015.11.014

zbMATH Keywords

symmetry breakingcomputer-assisted proofsSAT solvingsorting networks

Mathematics Subject Classification ID

Searching and sorting (68P10)

Related Items (10)

Optimizing sorting algorithms by using sorting networks ⋮ Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof ⋮ Expressing Symmetry Breaking in DRAT Proofs ⋮ Optimal-depth sorting networks ⋮ The Half Cleaner Lemma: Constructing Efficient Interconnection Networks from Sorting Networks ⋮ Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker ⋮ How to get more out of your oracles ⋮ Logic Programming with Graph Automorphism: Integratingnautywith Prolog (Tool Description) ⋮ Sorting networks: to the end and back again ⋮ Formally proving size optimality of sorting networks

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Bounds on the size of test sets for sorting and related networks
• Sorting in \(c \log n\) parallel steps
• Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
• A computer-assisted optimal depth lower bound for nine-input sorting networks
• A Sorting Problem
• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• Extraction in Coq: An Overview
• Efficient generation of the binary reflected gray code and its applications
• Boolean Equi-propagation for Concise and Efficient SAT Encodings of Combinatorial Problems
• Toward a Lower Bound for Sorting Networks
• The challenge of computer mathematics
• Optimal Sorting Networks
• An Improved Lower Bound for Sorting Networks
• Principles and Practice of Constraint Programming – CP 2003

This page was built for publication: Sorting nine inputs requires twenty-five comparisons