CNF Benchmark Suite: VLIW-UNSAT-2.0
========================================
Description: unsatisfiable formulas from formal verification of VLIW processors with instruction queues
# of instances: 9
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_iq1 4889224 24604 261473 744579 2.847632
9dlx_vliw_at_b_iq2 10499959 44095 542253 1554259 2.866299
9dlx_vliw_at_b_iq3 19198883 69789 968295 2788367 2.879667
9dlx_vliw_at_b_iq4 32381935 106013 1598301 4617403 2.888945
9dlx_vliw_at_b_iq5 52115994 151669 2465731 7141423 2.896270
9dlx_vliw_at_b_iq6 78608335 209724 3634677 10547961 2.902035
9dlx_vliw_at_b_iq7 134777596 306095 6069108 17675754 2.912414
9dlx_vliw_at_b_iq8 160050945 371419 7170909 20872419 2.910708
9dlx_vliw_at_b_iq9 218325589 482093 9676386 28195028 2.913797
output of md5sum:
-------------------------------------------------------------------------------------------------
9158de01004aff62af67cbb9db5bcbbb 9dlx_vliw_at_b_iq1.cnf
f0f4556999ccb446384994a4148fca28 9dlx_vliw_at_b_iq2.cnf
ba6236c6cc840bb0208f73665843c375 9dlx_vliw_at_b_iq3.cnf
6fcbaf8c6c7ed0c41d8ac12258cafaee 9dlx_vliw_at_b_iq4.cnf
79c983ee7a6671238604da3040f85341 9dlx_vliw_at_b_iq5.cnf
580dc3969c4e46e50013253fd4ac9139 9dlx_vliw_at_b_iq6.cnf
0fbc00fde383cec371bb97d621c5e7e5 9dlx_vliw_at_b_iq7.cnf
776da55785376fd8eac6989ca812b102 9dlx_vliw_at_b_iq8.cnf
9a43349587a435e7109b46b3aceb156e 9dlx_vliw_at_b_iq9.cnf