CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2024 Models
收藏资源简介:
These are isomorphic and optimized miters for 318 HWMCC'24 AIGER benchmarks. There is one excessive benchmark 'Problem17.aig' which we omitted of original size of 2.3 GB (AIGER file size in bytes) as all others are at most16 MB in file size. We first normalized the original sequential benchmarks (removed constraints, forced reset zero and turned the bad state constraint into an output). Then we optimized the resulting AIG with combinational synthesis with ABC using the dc2 script. Then we produced combinational miters between two copies of the original AIGER circuit, and between the original and its optimized variant. Finally we encoded these miters into CNF using an optimized XOR and ITE encoding with 'aigmiter' and zipped them with 'xz'. This produced 3 identical isomorphic and optimized miter CNFs which we still keep - 9aa3105732c2485f4a08d7b4dc496802 cnf/iso/a16-p018.cnf.xz - 9aa3105732c2485f4a08d7b4dc496802 cnf/iso/a16-p139.cnf.xz - 9aa3105732c2485f4a08d7b4dc496802 cnf/iso/a16-p160.cnf.xz while there were no identical isomorphic nor optimized miter AIGs.



