Combinatorial Enumeration Algorithms

Paul Hofmeier 📧 and Emin Karayel 📧

November 11, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

Combinatorial objects have configurations which can be enumerated by algorithms, but especially for imperative programs, it is difficult to find out if they produce the correct output and don’t generate duplicates. Therefore, for some of the most common combinatorial objects, namely n_Sequences, n_Permutations, n_Subsets, Powerset, Integer_Compositions, Integer_Partitions, Weak_Integer_Compositions, Derangements and Trees, this entry formalizes efficient functional programs and verifies their correctness. In addition, it provides cardinality proofs for those combinatorial objects. Some cardinalities are verified using the enumeration functions and others are shown using existing libraries including other AFP entries.

License

BSD License

Topics

Related publications

  • Hofmeier, Paul. (2022). Verification of Combinatorial Algorithms [Bachelor's Thesis, Technische Universität MĂĽnchen]. mediaTUM. https://mediatum.ub.tum.de/1693026

Session Combinatorial_Enumeration_Algorithms