Full per-collection licensing detail for the CNF benchmark corpus. See the top-level
README.md for the corpus overview, and each collection's own
README.md for source links, citation, and removal notes specific to that collection.
| Collection | Source | License |
|---|---|---|
mcc/* |
Model Counting Competition (Zenodo records in the mcc/ section of the README) |
CC BY 4.0 — the competition publishes accepted instances under CC-BY |
mc-in-the-wild/, mc-in-the-wild-projected/ |
Zenodo 13284883 | CC BY 4.0 |
fichte-hecher/ |
Zenodo 1299752 | CC BY-NC 4.0 — non-commercial use only |
hwmcc/ |
Zenodo 15207209 | CC BY 4.0 |
feature-models/ |
SoftVarE feature-model-benchmark | The collection repo is MIT; the individual feature models retain the terms of the systems they were extracted from (see the upstream per-model Source metadata) |
cril-kc/ |
CRIL Knowledge Compilation page | As stated by CRIL at the source link; no explicit benchmark license is published |
pmc/ |
CRIL pmc preprocessor archive |
As per the original sources; no explicit license published |
satlib/ |
SATLIB | No license text (see below); the maintainers request citation of Hoos & Stützle (SAT 2000) |
LGSynth89/, iscas85b/, iscas89/ |
Classic MCNC / ISCAS benchmark suites | No license text (see below) |
Several classic collections predate the practice of attaching license text, and none exists for them. What is documented is their purpose and distribution history: the ISCAS'85/'89 circuits were created as community benchmarks (distributed at the 1985 and 1989 IEEE ISCAS conferences as "neutral netlists" for tool evaluation), the MCNC/LGSynth suites were distributed free of charge by the Microelectronics Center of North Carolina under ACM/SIGDA sponsorship, SATLIB is a long-running public benchmark archive that requests citation, and the CRIL archives are published for download by the lab that curated them. All have been mirrored openly by academic archives for decades — many of the same formulas also appear in the Model Counting Competition's CC BY 4.0 Zenodo releases (the canonical index in this repo maps the overlap). We redistribute CNF encodings of these instances on that basis, for research purposes. There is no explicit written grant; if you need one for your use case, contact the original maintainers. If you are a rights holder and object to an instance being included, open an issue and we will remove it.
Attribution: the CC BY collections require credit — the Model Counting Competition
organizers (Fichte, Hecher et al.) for mcc/*, Shaw & Meel for mc-in-the-wild*,
and Biere, Fazekas, Fleury & Froleyks for hwmcc/. When using any
collection in a publication, cite its original source, not this repository.
Some instances additionally carry an in-file license header (e.g. several MCC 2023 track-1 instances are CC BY 4.0 Petri-net conversions by Bouvier & Garavel, INRIA); those headers are preserved verbatim, as CC BY requires.
Conversely, 64 LGSynth89 *_mince.cnf variants were removed from this distribution in
July 2026 because their headers carry a bare copyright notice with no license grant.
Instance counts here are therefore lower than in papers that evaluated on the original
collection — see LGSynth89/README.md for the full removal list.