Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/595
Title: | Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation | Authors: | Marić, Filip | Affiliations: | Informatics and Computer Science | Keywords: | Isabelle/HOL;Isomorph-free exhaustive generation;Orderly;Software verification | Issue Date: | 1-Jan-2020 | Journal: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Abstract: | Many applications require generating catalogues of combinatorial objects, that do not contain isomorphs. Several efficient abstract schemes for this problem exist. One is described independently by I. A. Faradžev and R. C. Read and has since been applied to catalogue many different combinatorial structures. We present an Isabelle/HOL verification of this abstract scheme. To show its practicality, we instantiate it on two concrete problems: enumerating digraphs and enumerating union-closed families of sets. In the second example abstract algorithm specification is refined to an implementation that can quite efficiently enumerate all canonical union-closed families over a six element universe (there is more than 100 million such families). |
URI: | https://research.matf.bg.ac.rs/handle/123456789/595 | ISBN: | 9783030510534 | ISSN: | 03029743 | DOI: | 10.1007/978-3-030-51054-1_16 |
Appears in Collections: | Research outputs |
Show full item record
SCOPUSTM
Citations
3
checked on Dec 21, 2024
Page view(s)
11
checked on Dec 23, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.