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>&nbsp; [1] H.-T. Zhang, J.-H. R. Jiang, A. Mishchenko, and L. Amaru. &nbsp;"Improved<br>&nbsp; large-scale SAT sweeping", In Proc. Intl. Work. on Logic Synthesis<br>&nbsp; (IWLS'22).</p> <p>&nbsp; [2] H.-T. Zhang, J.-H. R. Jiang, L. Amaru, A. Mishchenko, and R. Brayton.<br>&nbsp; "Deep integration of circuit simulator and SAT solver". In Proc. of Design<br>&nbsp; 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. &nbsp;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`. &nbsp;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. &nbsp;This reduces not only the number of clauses and variables but has<br>positive effects on solving time. &nbsp;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>