CNF Benchmark Suite: VLIW-SAT-2.0
========================================
Description: satisfiable formulas from formal verification of VLIW processors with instruction queues
# of instances: 10
Author: Miroslav N. Velev (mvelev@ece.cmu.edu)
http://www.ece.cmu.edu/~mvelev
Date: August 23, 2003
The formula sizes are:
CNF Formula Size [Bytes] Variables Clauses Literals Avg. Literals/Clause
-------------------------------------------------------------------------------------------------
9dlx_vliw_at_b_iq6_bug1 190601752 236038 8084666 23869718 2.952468
9dlx_vliw_at_b_iq6_bug2 190394653 235928 8076545 23845551 2.952445
9dlx_vliw_at_b_iq6_bug3 190015294 235402 8060882 23799590 2.952480
9dlx_vliw_at_b_iq6_bug4 190113993 235277 8063780 23808550 2.952530
9dlx_vliw_at_b_iq6_bug5 190394160 235923 8076534 23845522 2.952445
9dlx_vliw_at_b_iq6_bug6 190394297 235926 8076539 23845537 2.952445
9dlx_vliw_at_b_iq6_bug7 130525776 173811 5609632 16549078 2.950118
9dlx_vliw_at_b_iq6_bug8 185923109 229942 7882655 23275209 2.952712
9dlx_vliw_at_b_iq6_bug9 190083276 235184 8063818 23808532 2.952514
9dlx_vliw_at_b_iq6_bug10 190394348 235926 8076542 23845546 2.952445
output of md5sum:
-------------------------------------------------------------------------------------------------
4eca9a78507fb94a30f4968e8f322f63 9dlx_vliw_at_b_iq6_bug1.cnf
355e02f23ddb2151ec3dcf292d98c77f 9dlx_vliw_at_b_iq6_bug2.cnf
83dc8e6d23a7d134be381881958d7a74 9dlx_vliw_at_b_iq6_bug3.cnf
8b382f9597922ad987b05376afd6937d 9dlx_vliw_at_b_iq6_bug4.cnf
a9b54dbfe3a1ed106b2306529064f761 9dlx_vliw_at_b_iq6_bug5.cnf
78fc734e7b7229aa546d9fb784ae2bb2 9dlx_vliw_at_b_iq6_bug6.cnf
e96e23fe7066b29ce5b534eb51bdd31f 9dlx_vliw_at_b_iq6_bug7.cnf
9569ae2dfbe1c697b48ee716ac94e58d 9dlx_vliw_at_b_iq6_bug8.cnf
591fe606eb98c3d5d1065355150e98e6 9dlx_vliw_at_b_iq6_bug9.cnf
3d54fed7409ea6ba19cc4572d8e0c4a4 9dlx_vliw_at_b_iq6_bug10.cnf