Name | normalized-opb/mps-v2-20-10/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-20-10-maros.opb |
MD5SUM | df23206734a7a5ecc1a5d03632e7fa81 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 344750 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 90 |
Biggest coefficient in the objective function | 4831838208 |
Number of bits for the biggest coefficient in the objective function | 33 |
Sum of the numbers in the objective function | 15032909794 |
Number of bits of the sum of numbers in the objective function | 34 |
Biggest number in a constraint | 4831838208 |
Number of bits of the biggest number in a constraint | 33 |
Biggest sum of numbers in a constraint | 15032909794 |
Number of bits of the biggest sum of numbers | 34 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 29.6805 |
Number of variables | 90 |
Total number of constraints | 6 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 15 |
Maximum length of a constraint | 90 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc4 THE 2005-06-16 13:35:48 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=25883 boxname=wulflinc4 idbench=1183 idsolver=18 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: df23206734a7a5ecc1a5d03632e7fa81 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-maros.opb REAL COMMAND: pb2sat-v2 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-maros.opb IDLAUNCH: 25883 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 846876 kB Buffers: 1052 kB Cached: 164984 kB SwapCached: 904 kB Active: 23996 kB Inactive: 144112 kB HighTotal: 131008 kB HighFree: 74648 kB LowTotal: 903652 kB LowFree: 772228 kB SwapTotal: 2097136 kB SwapFree: 2095236 kB Dirty: 28 kB Writeback: 0 kB Mapped: 4996 kB Slab: 13904 kB Committed_AS: 71884 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-06-16 13:39:19 (client local time) WITH STATUS 30 IN 210.857 SECONDS stats: 25883 0 210.857 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c This solver internally uses Chaff 2004.11.15 Simplified c running zchaff... c got solution with objective value: 408868 c small objective detected c CONFLICT during preprocess c [startup+0.305323 s] setting bit 33 to 0 c CONFLICT during preprocess c [startup+0.323035 s] setting bit 32 to 0 c CONFLICT during preprocess c [startup+0.340824 s] setting bit 31 to 0 c CONFLICT during preprocess c [startup+0.358961 s] setting bit 30 to 0 c CONFLICT during preprocess c [startup+0.377106 s] setting bit 29 to 0 c CONFLICT during preprocess c [startup+0.395499 s] setting bit 28 to 0 c CONFLICT during preprocess c [startup+0.413874 s] setting bit 27 to 0 c CONFLICT during preprocess c [startup+0.432444 s] setting bit 26 to 0 c CONFLICT during preprocess c [startup+0.450992 s] setting bit 25 to 0 c CONFLICT during preprocess c [startup+0.469684 s] setting bit 24 to 0 c CONFLICT during preprocess c [startup+0.488331 s] setting bit 23 to 0 c CONFLICT during preprocess c [startup+0.507073 s] setting bit 22 to 0 c CONFLICT during preprocess c [startup+0.525825 s] setting bit 21 to 0 c CONFLICT during preprocess c [startup+0.5446 s] setting bit 20 to 0 c CONFLICT during preprocess c [startup+0.563448 s] setting bit 19 to 0 c [startup+0.621759 s] setting bit 18 to 0 c [startup+0.943542 s] setting bit 17 to 0 c Decision: 968/6449 Time: 2.76858/86400 c Decision: 990/6449 Time: 4.25135/86400 c Decision: 990/6449 Time: 5.35119/86400 c Decision: 995/6449 Time: 6.52901/86400 c Decision: 1119/6449 Time: 8.32573/86400 c [startup+12.2722 s] setting bit 16 to 0 c Decision: 907/6449 Time: 12.2531/86400 c got solution with objective value: 372032 c [startup+24.63 s] setting bit 15 to 1 c got solution with objective value: 358846 c [startup+24.9505 s] setting bit 14 to 1 c got solution with objective value: 351499 c [startup+25.5432 s] setting bit 13 to 1 c got solution with objective value: 347392 c [startup+26.6313 s] setting bit 12 to 1 c Decision: 926/6449 Time: 1.57976/86400 c Decision: 926/6449 Time: 2.99855/86400 c Decision: 932/6449 Time: 4.18137/86400 c got solution with objective value: 345361 c [startup+31.6167 s] setting bit 11 to 1 c Decision: 933/6449 Time: 1.78173/86400 c Decision: 939/6449 Time: 3.40748/86400 c Decision: 939/6449 Time: 4.92625/86400 c Decision: 951/6449 Time: 7.40887/86400 c Decision: 951/6449 Time: 9.07262/86400 c Decision: 1022/6449 Time: 11.7472/86400 c Decision: 1022/6449 Time: 13.6059/86400 c Decision: 1035/6449 Time: 15.7596/86400 c Decision: 1215/6449 Time: 18.4732/86400 c Decision: 1215/6449 Time: 20.9708/86400 c [startup+53.7177 s] setting bit 10 to 0 c Decision: 1025/6449 Time: 5.12022/86400 c Decision: 1025/6449 Time: 6.55/86400 c Decision: 1031/6449 Time: 9.02263/86400 c Decision: 1031/6449 Time: 10.8773/86400 c got solution with objective value: 344827 c [startup+65.5541 s] setting bit 9 to 1 c Decision: 1049/6449 Time: 5.42018/86400 c Decision: 1049/6449 Time: 7.81781/86400 c Decision: 1224/6449 Time: 11.7762/86400 c Decision: 1333/6449 Time: 14.5698/86400 c Decision: 1333/6449 Time: 16.8744/86400 c Decision: 1333/6449 Time: 19.474/86400 c [startup+88.6158 s] setting bit 8 to 0 c Decision: 1031/6449 Time: 3.79842/86400 c Decision: 1031/6449 Time: 6.74897/86400 c Decision: 1031/6449 Time: 9.12961/86400 c Decision: 1128/6449 Time: 14.2498/86400 c Decision: 1279/6449 Time: 18.4952/86400 c Decision: 1384/6449 Time: 21.5007/86400 c Decision: 1384/6449 Time: 24.5123/86400 c Decision: 1472/6449 Time: 29.3085/86400 c Decision: 1932/6449 Time: 33.2499/86400 c Decision: 1932/6449 Time: 36.2915/86400 c Decision: 1932/6449 Time: 39.494/86400 c Decision: 2149/6449 Time: 45.2171/86400 c Decision: 2360/6449 Time: 53.0619/86400 c [startup+143.526 s] setting bit 7 to 0 c got solution with objective value: 344802 c [startup+148.166 s] setting bit 6 to 1 c got solution with objective value: 344768 c [startup+153.778 s] setting bit 5 to 1 c Decision: 1106/6449 Time: 3.18952/86400 c Decision: 1106/6449 Time: 5.80912/86400 c got solution with objective value: 344751 c [startup+160.941 s] setting bit 4 to 1 c Decision: 1427/6449 Time: 4.39233/86400 c Decision: 1427/6449 Time: 7.35588/86400 c Decision: 1427/6449 Time: 9.98048/86400 c Decision: 1427/6449 Time: 14.2298/86400 c Decision: 1944/6449 Time: 16.5185/86400 c Decision: 2122/6449 Time: 19.426/86400 c Decision: 3026/6449 Time: 24.0493/86400 c Decision: 3026/6449 Time: 26.505/86400 c [startup+189.893 s] setting bit 3 to 0 c got solution with objective value: 344751 c [startup+192.407 s] setting bit 2 to 1 c Decision: 1570/6449 Time: 6.30904/86400 c Decision: 1662/6449 Time: 12.1632/86400 c [startup+209.108 s] setting bit 1 to 0 c got solution with objective value: 344750 c [startup+210.788 s] setting bit 0 to 1 s OPTIMUM FOUND v VOL1_bit0 VOL1_bit1 -VOL1_bit10 -VOL1_bit11 -VOL1_bit12 -VOL1_bit13 -VOL1_bit14 -VOL1_bit15 -VOL1_bit16 -VOL1_bit17 -VOL1_bit18 -VOL1_bit19 -VOL1_bit2 -VOL1_bit3 -VOL1_bit4 -VOL1_bit5 -VOL1_bit6 -VOL1_bit7 -VOL1_bit8 -VOL1_bit9 -VOL1_bit_1 VOL1_bit_10 VOL1_bit_2 -VOL1_bit_3 VOL1_bit_4 -VOL1_bit_5 VOL1_bit_6 -VOL1_bit_7 VOL1_bit_8 -VOL1_bit_9 VOL2_bit0 -VOL2_bit1 -VOL2_bit10 -VOL2_bit11 -VOL2_bit12 -VOL2_bit13 -VOL2_bit14 -VOL2_bit15 -VOL2_bit16 -VOL2_bit17 -VOL2_bit18 -VOL2_bit19 VOL2_bit2 VOL2_bit3 -VOL2_bit4 -VOL2_bit5 -VOL2_bit6 -VOL2_bit7 -VOL2_bit8 -VOL2_bit9 -VOL2_bit_1 VOL2_bit_10 VOL2_bit_2 -VOL2_bit_3 VOL2_bit_4 -VOL2_bit_5 VOL2_bit_6 -VOL2_bit_7 VOL2_bit_8 -VOL2_bit_9 -VOL3_bit0 VOL3_bit1 VOL3_bit2 VOL3_bit3 VOL3_bit4 -VOL3_bit_1 -VOL3_bit_10 -VOL3_bit_2 -VOL3_bit_3 -VOL3_bit_4 -VOL3_bit_5 -VOL3_bit_6 -VOL3_bit_7 -VOL3_bit_8 -VOL3_bit_9 -VOL4_bit0 -VOL4_bit1 -VOL4_bit2 -VOL4_bit3 -VOL4_bit4 -VOL4_bit_1 VOL4_bit_10 -VOL4_bit_2 -VOL4_bit_3 -VOL4_bit_4 -VOL4_bit_5 -VOL4_bit_6 -VOL4_bit_7 -VOL4_bit_8 -VOL4_bit_9 #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Enforcing Stack size limit: 67108864 bytes Current StackSize limit: 67108864 bytes Raw data (loadavg): 0.97 0.99 0.92 2/54 26902 Raw data (stat): 26902 (runsolver) R 26901 21152 21151 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 971158704 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.0012 s] Raw data (loadavg): 0.97 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 1346 0 0 0 994 4 0 0 25 0 1 0 971158704 5308416 1064 4294967295 134512640 135730672 3221224576 3221222864 134747568 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 1296 1064 301 301 0 995 0 vsize: 5184 [startup+20.002 s] Raw data (loadavg): 0.98 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 1825 0 0 0 1991 7 0 0 25 0 1 0 971158704 7544832 1350 4294967295 134512640 135730672 3221224576 3221222864 134747578 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 1842 1350 301 301 0 1541 0 vsize: 7368 [startup+30.0016 s] Raw data (loadavg): 0.98 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 2040 0 0 0 2988 9 0 0 25 0 1 0 971158704 7954432 1565 4294967295 134512640 135730672 3221224576 3221222988 135341601 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 1942 1565 301 301 0 1641 0 vsize: 7768 [startup+40.0018 s] Raw data (loadavg): 0.98 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 2173 0 0 0 3986 11 0 0 25 0 1 0 971158704 10305536 1698 4294967295 134512640 135730672 3221224576 3221222864 134747543 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 2516 1698 301 301 0 2215 0 vsize: 10064 [startup+50.0027 s] Raw data (loadavg): 0.98 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 2390 0 0 0 4984 13 0 0 25 0 1 0 971158704 10428416 1915 4294967295 134512640 135730672 3221224576 3221222988 135341601 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 2546 1915 301 301 0 2245 0 vsize: 10184 [startup+60.0032 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 2714 0 0 0 5982 16 0 0 25 0 1 0 971158704 10768384 2239 4294967295 134512640 135730672 3221224576 3221222864 134747568 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 2629 2239 301 301 0 2328 0 vsize: 10516 [startup+70.0057 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 2749 0 0 0 6979 19 0 0 25 0 1 0 971158704 10768384 2274 4294967295 134512640 135730672 3221224576 3221222864 134747568 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 2629 2274 301 301 0 2328 0 vsize: 10516 [startup+80.0063 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 2810 0 0 0 7977 20 0 0 25 0 1 0 971158704 10997760 2335 4294967295 134512640 135730672 3221224576 3221222864 134747751 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 2685 2335 301 301 0 2384 0 vsize: 10740 [startup+90.0068 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 2862 0 0 0 8977 21 0 0 25 0 1 0 971158704 11137024 2387 4294967295 134512640 135730672 3221224576 3221222864 134747627 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 2719 2387 301 301 0 2418 0 vsize: 10876 [startup+100.007 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 3311 0 0 0 9975 23 0 0 25 0 1 0 971158704 12906496 2451 4294967295 134512640 135730672 3221224576 3221222864 134747651 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3151 2451 301 301 0 2850 0 vsize: 12604 [startup+110.008 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 3463 0 0 0 10974 24 0 0 25 0 1 0 971158704 13041664 2603 4294967295 134512640 135730672 3221224576 3221222880 134746205 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3184 2603 301 301 0 2883 0 vsize: 12736 [startup+120.009 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 3618 0 0 0 11973 25 0 0 25 0 1 0 971158704 17465344 2758 4294967295 134512640 135730672 3221224576 3221222864 134747570 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4264 2758 301 301 0 3963 0 vsize: 17056 [startup+130.008 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 3992 0 0 0 12971 27 0 0 25 0 1 0 971158704 17600512 3132 4294967295 134512640 135730672 3221224576 3221222864 134747751 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4297 3132 301 301 0 3996 0 vsize: 17188 [startup+140.008 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 4039 0 0 0 13970 29 0 0 25 0 1 0 971158704 17866752 3179 4294967295 134512640 135730672 3221224576 3221222992 134748106 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4362 3179 301 301 0 4061 0 vsize: 17448 [startup+150.009 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 4213 0 0 0 14968 30 0 0 25 0 1 0 971158704 17866752 3353 4294967295 134512640 135730672 3221224576 3221222864 134747543 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4362 3353 301 301 0 4061 0 vsize: 17448 [startup+160.01 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 4489 0 0 0 15967 32 0 0 25 0 1 0 971158704 18075648 3629 4294967295 134512640 135730672 3221224576 3221222864 134747570 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4413 3629 301 301 0 4112 0 vsize: 17652 [startup+170.01 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 4544 0 0 0 16966 34 0 0 25 0 1 0 971158704 18210816 3684 4294967295 134512640 135730672 3221224576 3221222864 134747627 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4446 3684 301 301 0 4145 0 vsize: 17784 [startup+180.01 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 4568 0 0 0 17965 34 0 0 25 0 1 0 971158704 18210816 3708 4294967295 134512640 135730672 3221224576 3221222752 134763180 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4446 3708 301 301 0 4145 0 vsize: 17784 [startup+190.011 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 4644 0 0 0 18964 35 0 0 25 0 1 0 971158704 18468864 3784 4294967295 134512640 135730672 3221224576 3221222864 134747563 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4509 3784 301 301 0 4208 0 vsize: 18036 [startup+200.011 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 4676 0 0 0 19963 37 0 0 25 0 1 0 971158704 18554880 3816 4294967295 134512640 135730672 3221224576 3221222988 135341601 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4530 3816 301 301 0 4229 0 vsize: 18120 [startup+210.011 s] Raw data (loadavg): 0.99 0.99 0.92 2/54 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 4714 0 0 0 20962 38 0 0 25 0 1 0 971158704 18653184 3854 4294967295 134512640 135730672 3221224576 3221222704 134767185 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4554 3854 301 301 0 4253 0 vsize: 18216 [startup+211.175 s] Raw data (loadavg): 0.99 0.99 0.92 1/53 26902 Raw data (stat): 26902 (pb2sat-v2) R 26901 21152 21151 0 -1 0 4714 0 0 0 20962 38 0 0 25 0 1 0 971158704 18653184 3854 4294967295 134512640 135730672 3221224576 3221222704 134767185 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4554 3854 301 301 0 4253 0 vsize: 0 Child status: 30 Real time (s): 211.175 CPU time (s): 210.857 CPU user time (s): 210.466 CPU system time (s): 0.39094 CPU usage (%): 99.8494 Max. virtual memory (Kb): 18216 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 344750 #### END VERIFIER DATA ####