Sorting nine inputs requires twenty-five comparisons

DOI10.1016/J.JCSS.2015.11.014MaRDI QIDQ899586zbMATH OpenOpenAlexFDO

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

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 breakingSAT solvingsorting networkscomputer-assisted proofs

Mathematics Subject Classification ID

Searching and sorting (68P10)

Recommendations

• A computer-assisted optimal depth lower bound for nine-input sorting networks
• Optimal sorting networks
• Optimal-depth sorting networks
• New Bounds on Optimal Sorting Networks
• Sorting networks: to the end and back again

Cites work

• scientific article; zbMATH DE number 3473265 (Why is no real title available?)
• scientific article; zbMATH DE number 3409355 (Why is no real title available?)
• A Sorting Problem
• A computer-assisted optimal depth lower bound for nine-input sorting networks
• An Improved Lower Bound for Sorting Networks
• Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems
• Bounds on the size of test sets for sorting and related networks
• Efficient CNF encoding of Boolean cardinality constraints
• Efficient generation of the binary reflected gray code and its applications
• Extraction in Coq: An Overview
• Formalizing size-optimal sorting networks: extracting a certified proof checker
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Optimal sorting networks
• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• Sorting in \(c \log n\) parallel steps
• The challenge of computer mathematics
• Toward a lower bound for sorting networks

Cited in

(13)

• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• Sorting networks: to the end and back again
• Expressing symmetry breaking in DRAT proofs
• How to get more out of your oracles
• A computer-assisted optimal depth lower bound for nine-input sorting networks
• The half cleaner lemma: constructing efficient interconnection networks from sorting networks
• Optimal conclusive sets for comparator networks
• Logic Programming with Graph Automorphism: Integratingnautywith Prolog (Tool Description)
• Optimal-depth sorting networks
• Formalizing size-optimal sorting networks: extracting a certified proof checker
• Optimizing sorting algorithms by using sorting networks
• Formally proving size optimality of sorting networks
• Optimal sorting networks

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q899586)