CNF Benchmarks from SMT-LIB QF_BV

---

The zip file below contains 15447 SAT problems in DIMACS that were produced by bit-blasting the QF_BV benchmarks of SMT-LIB.

There are 41696 QF_BV problems in SMT-LIB. We converted them to CNF using Yices 2.

Yices 2 solves 18940 problems by preprocessing and simplification. We converted the rest (22756 problems) to CNF. Out of these CNF problems, we removed trivial benchmarks and duplicates. There were

• 325 empty formulas (trivially SAT)
• 2695 formulas that contain the empty clause (trivially UNSAT)
• 4286 duplicates.

This leaves 15450 CNF files. Three of them are very large (more than 5GB). This zip file contains the remaining CNF files, compressed with xz. The file is approximately 7GB.

---

New versions (produced by newer versions of Yices 2).

• CNFs-16c3cb92.zip (7GB)
• CNFs-b36f92fb.zip (4.4GB)

---