Daniela Kaufmann, Armin Biere, Manuel Kauers,
"Arithmetic Verification Problems Submitted to the SAT Race 2019"
, in Marijn Heule, Matti Järvisalo, Martin Suda: Proc. of SAT Race 2019 - Solver and Benchmark Descriptions, Vol. B-2019-1, Department of Computer Science Series of Publications B, University of Helsinki, Seite(n) 49, 2019
Arithmetic Verification Problems Submitted to the SAT Race 2019
Sprache des Titels:
Proc. of SAT Race 2019 - Solver and Benchmark Descriptions
In the benchmark description of our arithmetic challenge problems  submitted to the SAT Competition 2016, we have mentioned that there is another source of multiplier designs, which we could not retrieve back then. These circuits described in  were used in  and then synthesized and translated to AIGs in our related work . Furthermore, the corresponding web-service ?Arithmetic Module Generator? for generating the circuits (in Verilog) became recently available again at https://www.ecsis.riec.tohoku.ac.jp/topics/amg/. For the SAT Race 2019 we generated AIG miters and encoded them into CNF for interesting bit-widths 10, 12 and 14, where SAT solvers not using algebraic reasoning start to have a hard time. These benchmarks compare pairwise several multipliers with different architectures and characteristics. We also considered unsigned multipliers and a few signed multipliers (these are all n × n inputs to 2n bits outputs multipliers where signedness makes a difference). We compare two signed architectures ?2cbpwtcl? and ?2csparrc? with pre?x ?eq2...? which gives 6 signed benchmarks for bit-widths 10,12,14. The 12 unsigned multiplier architectures we compare are bparcl, bparrc, bpctbk, bpdtlf, bpwtcl, bpwtrc, sparcl, sparrc, spctbk, spdtlf, spwtcl, spwtrc for bit-widths 10,12 and 14, which gives 396 = 3 · 12 · 11 unsigned benchmarks (all with ?eq...? but without ?eq2?, ?btor? nor ?ktsb? in their name).
Sprache der Kurzfassung:
Department of Computer Science Series of Publications B