CNF Encoded Hard Miters from IWLS'22 Paper
DOI10.5281/zenodo.10823099Zenodo10823099MaRDI QIDQ6700825FDOQ6700825
Dataset published at Zenodo repository.
Publication date: 15 March 2024
Copyright license: Creative Commons Attribution 4.0 International
Five Hard Miters from an IWLS'22 Paper Encoded into CNF in two Ways The IWLS'22 paper [1] by He-Teng Zhang, Jie-Hong R. Jiang, Alan Mishchenko,and Luca Amaru, which can be considered an update on their DAC'21 [2] paperwas focusing on a hybrid approach to SAT-sweeping, i.e., using a SAT solverincrementally, taking the circuit structure into account. Experiments in [1] used a subset of the benchmarks from [2] which alsocontains five miters `n01`, `n04`, `n06`, and `test01` and `test02` providedto us by Alan Mishchenko and which were considered hard for SAT sweeping,and particularly for monolithic CNF-level SAT solving. [1] H.-T. Zhang, J.-H. R. Jiang, A. Mishchenko, and L. Amaru. "Improved large-scale SAT sweeping", In Proc. Intl. Work. on Logic Synthesis (IWLS'22). [2] H.-T. Zhang, J.-H. R. Jiang, L. Amaru, A. Mishchenko, and R. Brayton. "Deep integration of circuit simulator and SAT solver". In Proc. of Design Automation Conference (DAC'21), 2021. It turned out, confirmed by Alan Mishchenko, that the outputs of `test01`and `test02`, were flipped in the process they were generated. This doesnot invalidate the SAT sweeping experiments in [1] and [2] at all, but needsto be taken care off, when encoding them into CNF with `aigtocnf`, by simplyfirst negating the outputs with `aigflip`. Further note, that the otherthree AIGs `n01`, `n04`, and `n06` are not negated but have multiple outputsand thus we joined them by disjunction with `aigor`. We have extended `aigtocnf` to detect XOR and ITE gates in AIGER circuits,i.e., during Tseitin encoding we check whether and an AND gate has twonegated AND gates as children and actually implements an XOR or ITE gate.In this case we use a direct CNF encoding of four clauses, instead of 9clauses for three AND gates, skipping the two child AND gates of the top ANDgate. This reduces not only the number of clauses and variables but haspositive effects on solving time. Thus all the CNF benchmarks come in twoflavors tagged `xits` with special treatment of XOR and ITE gates duringTseitin encoding and `ands` without.
This page was built for dataset: CNF Encoded Hard Miters from IWLS'22 Paper
