A curated collection of ~27,900 CNF instances for model counting, weighted model
counting, projected model counting, and knowledge-compilation research. Most files are
.cnf.xz — LZMA-compressed DIMACS CNF. Weighted and projected instances declare their
task in comment lines (c t wmc, c p weight, c p show) following the
format of the Model Counting Competition (MCC);
smaller and legacy collections ship plain uncompressed .cnf.
| Directory | Files | Format | Type | Source |
|---|---|---|---|---|
LGSynth89/ |
72 | .cnf |
MC | LGSynth89 logic synthesis circuits |
iscas85b/ |
21 | .cnf |
MC | ISCAS'85 combinational benchmark circuits |
iscas89/ |
31 | .cnf |
MC | ISCAS'89 sequential benchmark circuits |
pmc/ |
1,422 | .cnf |
MC | CRIL pmc-preprocessor benchmark archive (multiple families) |
mcc/2020/ |
600 | .cnf.xz |
MC, WMC, PMC | Model Counting Competition 2020 (track1–track3) |
mcc/2021/ |
800 | .cnf.xz |
MC, WMC, PMC | Model Counting Competition 2021 (track1–track4) |
mcc/2022/ |
800 | .cnf.xz |
MC, WMC, PMC, PWMC | Model Counting Competition 2022 (track1–track4) |
mcc/2022/submitted/ |
4,480 | .cnf.xz |
MC, PMC | MCC 2022 participant-submitted instances |
mcc/2023/ |
800 | .cnf.xz |
MC, WMC, PMC, PWMC | Model Counting Competition 2023 (track1–track4) |
mcc/2024/ |
1,000 | .cnf.xz |
MC, WMC, PMC, PWMC | Model Counting Competition 2024 (track1, track2-bonus, track2-random, track3, track4) |
mcc/2024/submitted/ |
4,712 | .cnf.xz |
MC, WMC, PMC, PWMC | MCC 2024 participant-submitted instances |
mcc/2025/ |
700 | .cnf.xz |
MC, PMC, PWMC, AMC | Model Counting Competition 2025 (track1, track3, track4, track5b; full 200/track except track 4, public 100 only) |
mcc/2026/ |
499 | .cnf.xz |
MC, WMC, PMC, AMC | Model Counting Competition 2026 public halves (track1, track2B, track3, track4, track5B; odd 001–199, 100 each — track4 has 99, instance 199 corrupt upstream) |
mc-in-the-wild/ |
1,195 | .cnf.xz |
WMC | MC-in-the-Wild: real-world Bayesian network instances |
mc-in-the-wild-projected/ |
1,185 | .cnf.xz |
PMC | MC-in-the-Wild: projected counting instances |
cril-kc/BayesianNetwork/ |
1,116 | .cnf.xz |
MC | CRIL knowledge compilation: Bayesian networks |
cril-kc/projectedMC/ |
530 | .cnf.xz |
PMC | CRIL knowledge compilation: projected MC |
cril-kc/qif/ |
7 | .cnf.xz |
PMC | CRIL knowledge compilation: quantitative information flow |
feature-models/ |
2,101 | .cnf.xz |
MC | Software product line feature models (SoftVarE) |
fichte-hecher/ |
1,310 | .cnf.xz |
MC | Fichte, Hecher, Woltran & Zisser 2018 counting benchmarks |
hwmcc/ |
318 | .cnf.xz |
SAT | Hardware Model Checking Competition 2024 miter circuits |
satlib/uf*/ |
2,500 | .cnf.xz |
SAT | SATLIB uniform-random 3-SAT (uf50–uf250) |
satlib/gcp*/ |
1,700 | .cnf.xz |
SAT | SATLIB flat graph coloring (gcp30–gcp200) |
Total: ~27,900 CNF instances
Each collection directory has its own README.md with context, source links, licensing,
and the citation for the associated paper.
There is no single license for this repository — licensing differs per collection.
Each sub-directory retains the license of its original source; the full table is in
docs/licensing.md, and each collection's own README.md states
its specific terms and citation. Several classic suites (ISCAS'85/'89, MCNC/LGSynth89,
SATLIB, the CRIL archives) come with no formal license text at all;
docs/licensing.md documents
the community-benchmark basis on which they are redistributed here. All instances are redistributed here for research
purposes, and a small number of copyright-headed instances with no license grant were
removed (see the affected collections' README.md for the removal lists).
fichte-hecher/ is CC BY-NC 4.0 — non-commercial use only; check the license table
before any commercial use of that collection specifically. If you are a rights holder
and would prefer an instance not be included, open an issue and we will remove it.
cnf_index.ndjson records every file's path, collection, name, vars, clauses,
literals, and primal-graph stats; cnf_index.py is the query layer over it:
from cnf_index import Index
idx = Index()
idx.filter(collection="mcc/2024/track", min_vars=1000) # 2024 competition tracksor python3 cnf_index.py stats|find|resolve.
Duplicates exist within and across collections (MCC recycles instances across years,
and whole archives overlap). canonical_index.ndjson maps every file to a canonical
representative under two identities: the 27,899 files collapse to 23,350 unique
per-task instances, and to 19,788 unique formulas when weights/projection are ignored.
Query via the API (idx.duplicates_of(...), dedup=...) or cnf_index.py dups|dedup.
scripts/convert_task.py strips WMC/PMC/PWMC annotations (weights, projection scope)
down to plain MC, so a d-DNNF/SDD compiler can be benchmarked without the stripped
task's side-channels leaking information the compiled circuit shouldn't have.
Full API, CLI, and field reference: docs/usage.md.
docs/licensing.md— full per-collection license table, attribution, and removed-instance notesdocs/usage.md—cnf_index.pyAPI/CLI, canonical index & duplicates, task conversion
scripts/build_cnf_index.py— rebuildcnf_index.ndjson(incremental, parallel)scripts/build_canonical_index.py— rebuildcanonical_index.ndjson, the corpus-wide duplicate map (see docs/usage.md § Canonical index / duplicates)scripts/convert_task.py— convert an annotated WMC/PMC/PWMC instance to another task variant, e.g. stripped plain MC for compilation benchmarking (see docs/usage.md § Task conversion)scripts/import_benchmarks.py— download and import all benchmark sets from scratch