CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2012 Models
DOI10.5281/zenodo.10823128Zenodo10823128MaRDI QIDQ6700826FDOQ6700826
Dataset published at Zenodo repository.
Publication date: 15 March 2024
Copyright license: Creative Commons Attribution 4.0 International
These miter benchmarks are used in a paper on congruence closure in 2024. The miter AIGs in the [aig `aig`] directory are the same as those used togenerate CNFs of miter benchmarks submitted to the SAT Challenge in 2012.Some of them have regularly been used in the SAT Competitions since then. The AIGs are separated into two sets: - [aig/iso `aig/iso`] miters of isomorphic circuits- [aig/opt `aig/opt`] miters of optimized versus original circuit The first set checks equivalence of one circuit with itself in the[aig/iso `aig/iso`] (isomorphic) sub-directory and second set containsequivalence checking problems (aka miters) comparing the original circuitwith an optimized version in the [aig/opt `aig/opt`] (optimized)sub-directory. The optimized versions of the circuits were obtained in 2012by the `dc2` script for ABC.We did not re-run ABC with a newer version in order to make sure we have asbase-line in our experiments the same CNFs, as they are well-known, i.e.,they have been used in the SAT competitions for several years. Note that the original AIGER models have state elements (called "latches"in AIGER terminology), but both the optimization with ABC as well as ourequivalence checking is purely combinational, by treating latches asadditional pseudo inputs, and next-state functions as output-functions. Themiters were accordingly generated (by the 2011 version) of `aigmiter` usingthe `-c` option. For the same reason as for ABC explained above, we did notrerun `aigmiter` either. We then encoded the two sets of AIGs into CNF in two different ways.The first encoding just uses a simple Tseitin encoding, withoutPlaisted-Greenbaum optimization, i.e., using the `--no-pg` option, as in 2012.Even though we use a new version of `aigtocnf` in `src/aiger/aigtocnf.c` wemade sure that identical CNFs are generated for this first encoding variantby checking that the MD5 sum of the (actually compressed) CNF files match.This required to disable a newly introduced cone-of-influence (COI)optimization with `--no-coi` which skips unreachable gates even when thePlaisted-Greenbaum optimization is disabled. The second variant of the encoding detects XOR and ITE gates by patternmatching and produces more concise CNFs by skipping internal AND gatesof detected XOR and ITE gates producing a direct encoding instead. This gives the following sets of CNFs; - [cnf/ands/iso `cnf/ands/iso`] isomorphic circuits with ANDs only- [cnf/ands/opt `cnf/ands/opt`] optimized versus original with ANDs only- [cnf/xits/isor `cnf/xits/iso`] isomorphic circuits with ANDs, XORs, ITEs- [cnf/xits/opt `cnf/xits/opt`] optimized versus original with ANDs, XORs, ITEs All the CNFs in these directories have the same original file name of theAIGER model to simplify run-time comparison. In `cnf/all` we furtherprovide links with qualified names to distinguish them.
This page was built for dataset: CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2012 Models
