Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-dg012142.opb |
MD5SUM | bc2dcc682f209df3faf1b0ad321ee43d |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 2147483647 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 24640 |
Biggest coefficient in the objective function | 5368709120000 |
Number of bits for the biggest coefficient in the objective function | 43 |
Sum of the numbers in the objective function | 1723417105498688 |
Number of bits of the sum of numbers in the objective function | 51 |
Biggest number in a constraint | 5368709120000 |
Number of bits of the biggest number in a constraint | 43 |
Biggest sum of numbers in a constraint | 1723417105498688 |
Number of bits of the biggest sum of numbers | 51 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1293.53 |
Number of variables | 43840 |
Total number of constraints | 6310 |
Number of constraints which are clauses | 40 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 6270 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 371 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc30 THE 2005-05-24 23:45:34 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=15096 boxname=wulflinc30 idbench=1162 idsolver=3 numberseed=0 MD5SUM SOLVER: 03a6a792daea978e4202f78851741568 /oldhome/oroussel/solvers/bsolo_mis MD5SUM BENCH: bc2dcc682f209df3faf1b0ad321ee43d /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-dg012142.opb REAL COMMAND: bsolo_mis /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-dg012142.opb IDLAUNCH: 15096 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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 : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 828412 kB Buffers: 19192 kB Cached: 164276 kB SwapCached: 1628 kB Active: 50728 kB Inactive: 135792 kB HighTotal: 131008 kB HighFree: 16912 kB LowTotal: 903652 kB LowFree: 811500 kB SwapTotal: 2097892 kB SwapFree: 2095420 kB Dirty: 44 kB Writeback: 0 kB Mapped: 5016 kB Slab: 14024 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-24 23:49:20 (client local time) WITH STATUS 20 IN 225.559 SECONDS stats: 15096 7 225.559 20 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Initial problem consists of 43840 variables and 2617 constraints. s UNSATISFIABLE c Exit Code: 20 c Total time: 225.49 s #### 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 Raw data (loadavg): 0.93 0.94 0.92 2/54 29259 Raw data (stat): 29259 (runsolver) R 29258 22056 22055 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 834297783 1052672 99 4294967295 134512640 135381576 3221224480 3221219696 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99969 s] Raw data (loadavg): 0.94 0.95 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 882 0 0 0 996 2 0 0 25 0 1 0 834297783 16392192 860 4294967295 134512640 134714540 3221224592 3221221116 1077196853 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4002 860 1111 63 0 3939 0 vsize: 16008 [startup+20.0004 s] Raw data (loadavg): 0.95 0.95 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 1255 0 0 0 1996 2 0 0 25 0 1 0 834297783 18014208 1233 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4398 1233 1111 63 0 4335 0 vsize: 17592 [startup+30.0032 s] Raw data (loadavg): 0.95 0.95 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 1632 0 0 0 2995 4 0 0 25 0 1 0 834297783 19472384 1610 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4754 1610 1111 63 0 4691 0 vsize: 19016 [startup+40.003 s] Raw data (loadavg): 0.96 0.95 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 2017 0 0 0 3995 4 0 0 25 0 1 0 834297783 21098496 1995 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 5151 1995 1111 63 0 5088 0 vsize: 20604 [startup+50.0039 s] Raw data (loadavg): 0.97 0.95 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 2417 0 0 0 4994 5 0 0 25 0 1 0 834297783 22769664 2395 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 5559 2395 1111 63 0 5496 0 vsize: 22236 [startup+60.0036 s] Raw data (loadavg): 0.97 0.95 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 2840 0 0 0 5993 6 0 0 25 0 1 0 834297783 24424448 2818 4294967295 134512640 134714540 3221224592 3221222820 1077414376 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 5963 2818 1111 63 0 5900 0 vsize: 23852 [startup+70.0044 s] Raw data (loadavg): 0.97 0.95 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 3271 0 0 0 6993 6 0 0 25 0 1 0 834297783 26247168 3249 4294967295 134512640 134714540 3221224592 3221222820 1077414433 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 6408 3249 1111 63 0 6345 0 vsize: 25632 [startup+80.0069 s] Raw data (loadavg): 0.98 0.95 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 3740 0 0 0 7991 8 0 0 25 0 1 0 834297783 28188672 3718 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 6882 3718 1111 63 0 6819 0 vsize: 27528 [startup+90.0061 s] Raw data (loadavg): 0.98 0.95 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 4251 0 0 0 8991 9 0 0 25 0 1 0 834297783 30310400 4229 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 7400 4229 1111 63 0 7337 0 vsize: 29600 [startup+100.006 s] Raw data (loadavg): 0.98 0.95 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 4802 0 0 0 9990 10 0 0 25 0 1 0 834297783 32624640 4780 4294967295 134512640 134714540 3221224592 3221222820 1077414410 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 7965 4780 1111 63 0 7902 0 vsize: 31860 [startup+110.006 s] Raw data (loadavg): 0.99 0.95 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 5368 0 0 0 10989 11 0 0 25 0 1 0 834297783 34893824 5346 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 8519 5346 1111 63 0 8456 0 vsize: 34076 [startup+120.006 s] Raw data (loadavg): 0.99 0.96 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 5963 0 0 0 11987 12 0 0 25 0 1 0 834297783 37326848 5941 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 9113 5941 1111 63 0 9050 0 vsize: 36452 [startup+130.007 s] Raw data (loadavg): 0.99 0.96 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 6595 0 0 0 12986 14 0 0 25 0 1 0 834297783 39907328 6573 4294967295 134512640 134714540 3221224592 3221222820 1077414360 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 9743 6573 1111 63 0 9680 0 vsize: 38972 [startup+140.006 s] Raw data (loadavg): 0.99 0.96 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 7337 0 0 0 13985 15 0 0 25 0 1 0 834297783 42905600 7315 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 10475 7315 1111 63 0 10412 0 vsize: 41900 [startup+150.007 s] Raw data (loadavg): 0.99 0.96 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 8231 0 0 0 14983 18 0 0 25 0 1 0 834297783 46546944 8209 4294967295 134512640 134714540 3221224592 3221222820 1077414376 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 11364 8209 1111 63 0 11301 0 vsize: 45456 [startup+160.007 s] Raw data (loadavg): 0.99 0.96 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 9267 0 0 0 15981 19 0 0 25 0 1 0 834297783 50835456 9245 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 12411 9245 1111 63 0 12348 0 vsize: 49644 [startup+170.008 s] Raw data (loadavg): 0.99 0.96 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 13670 0 0 0 16973 28 0 0 25 0 1 0 834297783 68960256 13648 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 16836 13648 1111 63 0 16773 0 vsize: 67344 [startup+180.008 s] Raw data (loadavg): 0.99 0.96 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 15226 0 0 0 17971 30 0 0 25 0 1 0 834297783 75276288 15204 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 18378 15204 1111 63 0 18315 0 vsize: 73512 [startup+190.009 s] Raw data (loadavg): 0.99 0.96 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 16845 0 0 0 18967 34 0 0 25 0 1 0 834297783 81932288 16823 4294967295 134512640 134714540 3221224592 3221222872 1077358896 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 20003 16823 1111 63 0 19940 0 vsize: 80012 [startup+200.009 s] Raw data (loadavg): 0.99 0.96 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 18120 0 0 0 19962 38 0 0 25 0 1 0 834297783 87068672 18098 4294967295 134512640 134714540 3221224592 3221222868 1077414382 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21257 18098 1111 63 0 21194 0 vsize: 85028 [startup+210.009 s] Raw data (loadavg): 0.99 0.96 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 25206 0 0 0 20944 56 0 0 25 0 1 0 834297783 116232192 25184 4294967295 134512640 134714540 3221224592 3221222252 1077253148 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 28377 25184 1111 63 0 28314 0 vsize: 113508 [startup+220.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 31109 0 0 0 21930 71 0 0 25 0 1 0 834297783 140468224 31087 4294967295 134512640 134714540 3221224592 3221221468 1077244281 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 34294 31087 1111 63 0 34231 0 vsize: 137176 [startup+225.555 s] Raw data (loadavg): 0.99 0.97 0.92 1/53 29259 Raw data (stat): 29259 (bsolo_mis) R 29258 22056 22055 0 -1 0 31109 0 0 0 21930 71 0 0 25 0 1 0 834297783 140468224 31087 4294967295 134512640 134714540 3221224592 3221221468 1077244281 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 34294 31087 1111 63 0 34231 0 vsize: 0 Child status: 20 Real time (s): 225.555 CPU time (s): 225.559 CPU user time (s): 224.661 CPU system time (s): 0.897863 CPU usage (%): 100.002 Max. virtual memory (Kb): 137176 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####