CNF Benchmark Suite: VLIW-SAT-2.1
========================================
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_iq8_bug1 375412488 410707 15613033 46157943 2.956373
9dlx_vliw_at_b_iq8_bug2 374499682 409731 15576332 46049744 2.956392
9dlx_vliw_at_b_iq8_bug3 375002824 410219 15596614 46109634 2.956387
9dlx_vliw_at_b_iq8_bug4 374517060 409220 15574959 46046675 2.956456
9dlx_vliw_at_b_iq8_bug5 375453811 410693 15615653 46165831 2.956382
9dlx_vliw_at_b_iq8_bug6 375040386 410553 15598521 46114703 2.956351
9dlx_vliw_at_b_iq8_bug7 375238152 410729 15606974 46139698 2.956351
9dlx_vliw_at_b_iq8_bug8 375160073 410560 15603495 46129595 2.956363
9dlx_vliw_at_b_iq8_bug9 390189520 449867 16331249 48230709 2.953277
9dlx_vliw_at_b_iq8_bug10 374050867 408558 15554750 45987368 2.956484
output of md5sum:
-------------------------------------------------------------------------------------------------
83e2d02e1e58e25078a50d11a93a270c 9dlx_vliw_at_b_iq8_bug1.cnf
148c708de343028566f9e4d595e6a972 9dlx_vliw_at_b_iq8_bug2.cnf
185bf4c737a118feeb9b64ca052a1e25 9dlx_vliw_at_b_iq8_bug3.cnf
010dcc91019334e73c20cac704a0d9ad 9dlx_vliw_at_b_iq8_bug4.cnf
585defb1183d156ab85881cd7cb5cd21 9dlx_vliw_at_b_iq8_bug5.cnf
57bb69a44ca6de1b104c08c99cae8c19 9dlx_vliw_at_b_iq8_bug6.cnf
7e3e5805c173ca84910b66402aa10212 9dlx_vliw_at_b_iq8_bug7.cnf
b4fb6e639e53a9a50535c6dcff298050 9dlx_vliw_at_b_iq8_bug8.cnf
89967700b960b708baf2d85266936e94 9dlx_vliw_at_b_iq8_bug9.cnf
a26455e8f63b4e8832bd881f5cbdd8a2 9dlx_vliw_at_b_iq8_bug10.cnf