CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2020 Models

From the Hardware Model Checking Competition 2020 we have collected 324sequential model checking problems and for each generated an isomorphic andan optimized miter. The isomorphic miters just compares two identicalcopies while for the optimized miter one copy went through optimizationwith ABC using the `dc2` command. The CNFs are generated with a new version of `aigtocnf` which detectsXOR and ITE gates in the AIGER circuit and if detected uses a more compactencoding (4 clauses clauses instead of 9) for each detected gate.我们从2020年硬件模型检测竞赛（Hardware Model Checking Competition 2020）中收集了324个顺序模型检测问题，并为每个问题生成了同构米特电路（isomorphic miter）与优化型米特电路。其中，同构米特电路仅对两份完全一致的电路副本进行比较；而优化型米特电路中的其中一份副本，已通过使用`dc2`命令的ABC工具完成了优化。 本数据集的合取范式（Conjunctive Normal Form，CNF）由新版`aigtocnf`工具生成，该工具可检测AIGER电路中的异或（XOR）门与如果-那么-否则（ITE）门；若检测到上述门电路，则为每个被检测门采用更紧凑的编码方式，仅需4个子句而非原有的9个子句。