Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-bm23.opb |
MD5SUM | 9e4c4999c6f95fcef879d3d86840d71a |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 34 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 27 |
Biggest coefficient in the objective function | 9 |
Number of bits for the biggest coefficient in the objective function | 4 |
Sum of the numbers in the objective function | 124 |
Number of bits of the sum of numbers in the objective function | 7 |
Biggest number in a constraint | 65 |
Number of bits of the biggest number in a constraint | 7 |
Biggest sum of numbers in a constraint | 182 |
Number of bits of the biggest sum of numbers | 8 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.25796 |
Number of variables | 27 |
Total number of constraints | 47 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 27 |
Number of constraints which are nor clauses,nor cardinality constraints | 20 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 26 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc5 THE 2005-04-22 03:26:36 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=11752 boxname=wulflinc5 idbench=904 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 9e4c4999c6f95fcef879d3d86840d71a /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-bm23.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-bm23.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-bm23.opb IDLAUNCH: 11752 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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 : 2 cpu MHz : 451.007 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: 391216 kB Buffers: 34092 kB Cached: 588208 kB SwapCached: 444 kB Active: 110524 kB Inactive: 513864 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 390964 kB SwapTotal: 2097136 kB SwapFree: 2095948 kB Dirty: 52 kB Writeback: 0 kB Mapped: 5200 kB Slab: 13316 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-22 03:27:05 (client local time) WITH STATUS 30 IN 28.3417 SECONDS stats: 11752 0 28.3417 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 20 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 19]---> Sorter-cost: 678 Base: 2 2 c ---[ 18]---> Sorter-cost: 689 Base: 3 2 c ---[ 17]---> Sorter-cost: 686 Base: 3 2 c ---[ 16]---> Sorter-cost: 475 Base: 3 3 c ---[ 15]---> Sorter-cost: 776 Base: 3 2 c ---[ 14]---> Sorter-cost: 514 Base: 3 2 c ---[ 13]---> Sorter-cost: 494 Base: 2 2 c ---[ 12]---> Sorter-cost: 661 Base: 3 2 c ---[ 11]---> Sorter-cost: 521 Base: 2 3 c ---[ 10]---> Sorter-cost: 165 Base: 2 c ---[ 9]---> Sorter-cost: 587 Base: 2 3 c ---[ 8]---> Sorter-cost: 562 Base: 2 2 c ---[ 7]---> Sorter-cost: 635 Base: 2 2 c ---[ 6]---> Sorter-cost: 470 Base: 3 3 c ---[ 5]---> Sorter-cost: 583 Base: 2 3 c ---[ 4]---> Sorter-cost: 547 Base: 3 2 c ---[ 3]---> Sorter-cost: 323 Base: 3 2 c ---[ 2]---> Sorter-cost: 477 Base: 2 2 c ---[ 1]---> Sorter-cost: 613 Base: 2 2 2 c ---[ 0]---> Sorter-cost: 530 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 26527 62446 | 8842 0 0 nan | 0.000 % | c | 100 | 26527 62446 | 9726 100 2423 24.2 | 0.232 % | c | 250 | 26527 62446 | 10698 250 5574 22.3 | 0.232 % | c | 475 | 26527 62446 | 11768 475 10512 22.1 | 0.232 % | c | 814 | 26527 62446 | 12945 814 17880 22.0 | 0.232 % | c ============================================================================== c [1mFound solution: 55[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 702 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 905 | 28193 66369 | 9397 905 20379 22.5 | 0.232 % | c | 1006 | 28193 66369 | 10336 1006 22726 22.6 | 0.229 % | c | 1156 | 28193 66369 | 11370 1156 26719 23.1 | 0.229 % | c | 1381 | 28193 66369 | 12507 1381 31200 22.6 | 0.229 % | c | 1720 | 28193 66369 | 13758 1720 38550 22.4 | 0.229 % | c ============================================================================== c [1mFound solution: 54[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1994 | 28269 66559 | 9423 1994 45937 23.0 | 0.229 % | c | 2094 | 28269 66559 | 10365 2094 49011 23.4 | 0.239 % | c | 2247 | 28269 66559 | 11401 2247 52765 23.5 | 0.239 % | c | 2473 | 28269 66559 | 12542 2473 59774 24.2 | 0.239 % | c | 2811 | 28269 66559 | 13796 2811 68498 24.4 | 0.239 % | c ============================================================================== c [1mFound solution: 47[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3040 | 28306 66651 | 9435 3040 74791 24.6 | 0.239 % | c | 3141 | 28306 66651 | 10378 3141 77554 24.7 | 0.250 % | c | 3291 | 28306 66651 | 11416 3291 81689 24.8 | 0.250 % | c | 3517 | 28306 66651 | 12557 3517 87455 24.9 | 0.250 % | c ============================================================================== c [1mFound solution: 35[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3576 | 28338 66727 | 9446 3576 88862 24.8 | 0.250 % | c | 3676 | 28338 66727 | 10390 3676 91971 25.0 | 0.260 % | c | 3827 | 28338 66727 | 11429 3827 95370 24.9 | 0.260 % | c | 4052 | 28338 66727 | 12572 4052 99519 24.6 | 0.260 % | c | 4391 | 28338 66727 | 13829 4391 106112 24.2 | 0.260 % | c ============================================================================== c [1mFound solution: 34[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4596 | 28345 66744 | 9448 4596 111737 24.3 | 0.260 % | c | 4696 | 28345 66744 | 10392 4696 114376 24.4 | 0.271 % | c | 4848 | 28345 66744 | 11432 4848 117979 24.3 | 0.271 % | c | 5074 | 28345 66744 | 12575 5074 120918 23.8 | 0.271 % | c | 5412 | 28275 66586 | 13832 4505 110778 24.6 | 0.488 % | c | 5918 | 28275 66586 | 15216 5011 120501 24.0 | 0.488 % | c | 6677 | 28275 66586 | 16737 5770 135965 23.6 | 0.488 % | c | 7816 | 28275 66586 | 18411 6909 158419 22.9 | 0.488 % | c ============================================================================== c [1mOptimal solution: 34[0m s OPTIMUM FOUND v -C101_bit0 -C102_bit0 C103_bit0 -C104_bit0 C105_bit0 -C106_bit0 -C107_bit0 -C108_bit0 C109_bit0 -C110_bit0 -C111_bit0 -C112_bit0 -C113_bit0 -C114_bit0 C115_bit0 -C116_bit0 C117_bit0 -C118_bit0 -C119_bit0 C120_bit0 -C121_bit0 C122_bit0 -C123_bit0 -C124_bit0 -C125_bit0 -C126_bit0 C127_bit0 c _______________________________________________________________________________ c c restarts : 32 c conflicts : 8766 (310 /sec) c decisions : 11028 (390 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 28.2927 s c _______________________________________________________________________________ #### 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.88 0.95 0.93 2/54 8907 Raw data (stat): 8907 (runsolver) R 8906 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 492249695 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0008 s] Raw data (loadavg): 0.90 0.96 0.93 2/54 8907 Raw data (stat): 8907 (minisat+) R 8906 24215 24214 0 -1 0 1202 0 0 0 995 3 0 0 25 0 1 0 492249695 6930432 1172 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1692 1172 603 41 0 1651 0 vsize: 6768 [startup+20.0017 s] Raw data (loadavg): 0.91 0.96 0.93 2/54 8907 Raw data (stat): 8907 (minisat+) R 8906 24215 24214 0 -1 0 1287 0 0 0 1994 4 0 0 25 0 1 0 492249695 7200768 1257 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1758 1257 603 41 0 1717 0 vsize: 7032 [startup+28.3642 s] Raw data (loadavg): 0.92 0.96 0.93 1/53 8907 Raw data (stat): 8907 (minisat+) R 8906 24215 24214 0 -1 0 1287 0 0 0 1994 4 0 0 25 0 1 0 492249695 7200768 1257 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1758 1257 603 41 0 1717 0 vsize: 0 Child status: 30 Real time (s): 28.3636 CPU time (s): 28.3417 CPU user time (s): 28.2967 CPU system time (s): 0.044993 CPU usage (%): 99.9228 Max. virtual memory (Kb): 7032 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 34 #### END VERIFIER DATA ####