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
Original Titel:
Arithmetic Verification Problems Submitted to the SAT Race 2019
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. of SAT Race 2019 - Solver and Benchmark Descriptions
Original Kurzfassung:
In the benchmark description of our arithmetic challenge problems [1] 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 [2] were used in [3] and then synthesized and translated to AIGs in our related work [4]. 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:
Englisch
Veröffentlicher:
Department of Computer Science Series of Publications B