Find research datasets worth reusing
Search datasets from major research repositories and use ShareScore to quickly assess how well each record supports discovery, access, and reuse.
3
datasets available to search
ShareScore release 0.9.0
Dataset results
3 results for “CNF encoding”
CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2012 Models
<p>These miter benchmarks are used in a paper on congruence closure in 2024.</p> <p>The miter AIGs in the [`aig`](aig) directory are the same as those used to<br>generate CNFs of miter benchmarks submitted to the SAT Challenge in 2012.<br>Some of them have regularly been used in the SAT Competitions since then.</p> <p>The AIGs are separated into two sets:</p> <p>- [`aig/iso`](aig/iso) miters of isomorphic circuits<br>- [`aig/opt`](aig/opt) miters of optimized versus original circuit</p> <p>The first set checks equivalence of one circuit with itself in the<br>[`aig/iso`](aig/iso) (isomorphic) sub-directory and second set contains<br>equivalence checking problems (aka miters) comparing the original circuit<br>with an optimized version in the [`aig/opt`](aig/opt) (optimized)<br>sub-directory. The optimized versions of the circuits were obtained in 2012<br>by the `dc2` script for [ABC](https://people.eecs.berkeley.edu/~alanmi/abc).<br>We did not re-run ABC with a newer version in order to make sure we have as<br>base-line in our experiments the same CNFs, as they are well-known, i.e., <br>they have been used in the SAT competitions for several years.</p> <p>Note that the original AIGER models have state elements (called "latches"<br>in AIGER terminology), but both the optimization with ABC as well as our<br>equivalence checking is purely combinational, by treating latches as<br>additional pseudo inputs, and next-state functions as output-functions. The<br>miters were accordingly generated (by the 2011 version) of `aigmiter` using<br>the `-c` option. For the same reason as for ABC explained above, we did not<br>rerun `aigmiter` either.</p> <p>We then encoded the two sets of AIGs into CNF in two different ways.<br>The first encoding just uses a simple Tseitin encoding, without<br>Plaisted-Greenbaum optimization, i.e., using the `--no-pg` option, as in 2012.<br>Even though we use a new version of `aigtocnf` in `src/aiger/aigtocnf.c` we<br>made sure that identical CNFs are generated for this first encoding variant<br>by checking that the MD5 sum of the (actually compressed) CNF files match.<br>This required to disable a newly introduced cone-of-influence (COI)<br>optimization with `--no-coi` which skips unreachable gates even when the<br>Plaisted-Greenbaum optimization is disabled.</p> <p>The second variant of the encoding detects XOR and ITE gates by pattern<br>matching and produces more concise CNFs by skipping internal AND gates<br>of detected XOR and ITE gates producing a direct encoding instead.</p> <p>This gives the following sets of CNFs;</p> <p>- [`cnf/ands/iso`](cnf/ands/iso) isomorphic circuits with ANDs only<br>- [`cnf/ands/opt`](cnf/ands/opt) optimized versus original with ANDs only<br>- [`cnf/xits/iso`](cnf/xits/isor) isomorphic circuits with ANDs, XORs, ITEs<br>- [`cnf/xits/opt`](cnf/xits/opt) optimized versus original with ANDs, XORs, ITEs</p> <p>All the CNFs in these directories have the same original file name of the<br>AIGER model to simplify run-time comparison. In `cnf/all` we further<br>provide links with qualified names to distinguish them.</p>
CNF Encoded Hard Miters from IWLS'22 Paper
<h3>Five Hard Miters from an IWLS'22 Paper Encoded into CNF in two Ways</h3> <p><br>The IWLS'22 paper [1] by He-Teng Zhang, Jie-Hong R. Jiang, Alan Mishchenko,<br>and Luca Amaru, which can be considered an update on their DAC'21 [2] paper<br>was focusing on a hybrid approach to SAT-sweeping, i.e., using a SAT solver<br>incrementally, taking the circuit structure into account.</p> <p>Experiments in [1] used a subset of the benchmarks from [2] which also<br>contains five miters `n01`, `n04`, `n06`, and `test01` and `test02` provided<br>to us by Alan Mishchenko and which were considered hard for SAT sweeping,<br>and particularly for monolithic CNF-level SAT solving.</p> <p> [1] H.-T. Zhang, J.-H. R. Jiang, A. Mishchenko, and L. Amaru. "Improved<br> large-scale SAT sweeping", In Proc. Intl. Work. on Logic Synthesis<br> (IWLS'22).</p> <p> [2] H.-T. Zhang, J.-H. R. Jiang, L. Amaru, A. Mishchenko, and R. Brayton.<br> "Deep integration of circuit simulator and SAT solver". In Proc. of Design<br> Automation Conference (DAC'21), 2021.</p> <p>It turned out, confirmed by Alan Mishchenko, that the outputs of `test01`<br>and `test02`, were flipped in the process they were generated. This does<br>not invalidate the SAT sweeping experiments in [1] and [2] at all, but needs<br>to be taken care off, when encoding them into CNF with `aigtocnf`, by simply<br>first negating the outputs with `aigflip`. Further note, that the other<br>three AIGs `n01`, `n04`, and `n06` are not negated but have multiple outputs<br>and thus we joined them by disjunction with `aigor`.</p> <p>We have extended `aigtocnf` to detect XOR and ITE gates in AIGER circuits,<br>i.e., during Tseitin encoding we check whether and an AND gate has two<br>negated AND gates as children and actually implements an XOR or ITE gate.<br>In this case we use a direct CNF encoding of four clauses, instead of 9<br>clauses for three AND gates, skipping the two child AND gates of the top AND<br>gate. This reduces not only the number of clauses and variables but has<br>positive effects on solving time. Thus all the CNF benchmarks come in two<br>flavors tagged `xits` with special treatment of XOR and ITE gates during<br>Tseitin encoding and `ands` without.</p>
CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2020 Models
<p>From the Hardware Model Checking Competition 2020 we have collected 324<br>sequential model checking problems and for each generated an isomorphic and<br>an optimized miter. The isomorphic miters just compares two identical<br>copies while for the optimized miter one copy went through optimization<br>with ABC using the `dc2` command.</p> <p>The CNFs are generated with a new version of `aigtocnf` which detects<br>XOR and ITE gates in the AIGER circuit and if detected uses a more compact<br>encoding (4 clauses clauses instead of 9) for each detected gate.</p>
ScienceDex guides
Understand access before you commit
These curated guides explain access requirements, typical timelines, costs, and reuse considerations for widely used research datasets.
Allen Brain Atlas
Allen Brain Atlas is an Allen Institute collection of brain map atlases, datasets, APIs, and analysis tools covering mouse, human, and non-human primate brain resources.
Annotated Behaviour and Observability Dataset (ABODe)
ABODe is a University of Edinburgh DataShare dataset for behavior classification in group-housed mice using home-cage video, identities, bounding boxes, ground-plate positions, and annotator labels.
DANDI Archive for NWB datasets
DANDI is a BRAIN Initiative archive for publishing and sharing neurophysiology data, including electrophysiology, optophysiology, and behavioral data packaged as NWB and related standards.
International Brain Laboratory public data
The International Brain Laboratory public data releases expose standardized mouse decision-making experiments, including Neuropixels recordings, widefield calcium imaging, behavior, and session metadata accessed through the ONE API.
OpenNeuro
OpenNeuro is a free, open platform for sharing neuroimaging datasets, with public search, dataset pages, and download paths for web, S3, DataLad, and the OpenNeuro CLI.