Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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 wulflinc9 THE 2005-04-21 19:07:54 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=16736 boxname=wulflinc9 idbench=1288 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 9e4c4999c6f95fcef879d3d86840d71a /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-bm23.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-bm23.opb IDLAUNCH: 16736 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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.242 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: 477640 kB Buffers: 30760 kB Cached: 504264 kB SwapCached: 0 kB Active: 363164 kB Inactive: 174672 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 477388 kB SwapTotal: 2097136 kB SwapFree: 2097048 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6824 kB Slab: 13592 kB Committed_AS: 63580 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 19:08:26 (client local time) WITH STATUS 30 IN 31.5022 SECONDS stats: 16736 0 31.5022 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: 476 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 | 19873 46623 | 6624 0 0 nan | 0.000 % | c | 102 | 19873 46623 | 7286 102 2443 24.0 | 0.232 % | c | 252 | 19873 46623 | 8015 252 5446 21.6 | 0.232 % | c | 478 | 19873 46623 | 8816 478 10041 21.0 | 0.231 % | c | 815 | 19873 46623 | 9698 815 18385 22.6 | 0.231 % | c ============================================================================== c [1mFound solution: 56[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 703 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1306 | 21179 49678 | 7059 1306 28955 22.2 | 0.231 % | c | 1407 | 21179 49678 | 7764 1407 31490 22.4 | 0.228 % | c | 1557 | 21179 49678 | 8541 1557 34783 22.3 | 0.228 % | c | 1784 | 21179 49678 | 9395 1784 39218 22.0 | 0.229 % | c | 2123 | 21179 49678 | 10335 2123 47892 22.6 | 0.228 % | c | 2629 | 21179 49678 | 11368 2629 60968 23.2 | 0.228 % | c | 3392 | 21179 49678 | 12505 3392 82200 24.2 | 0.228 % | c | 4531 | 21179 49678 | 13755 4531 114424 25.3 | 0.228 % | c ============================================================================== c [1mFound solution: 55[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 | 4689 | 21190 49713 | 7063 4689 118099 25.2 | 0.228 % | c | 4789 | 21190 49713 | 7769 4789 120288 25.1 | 0.239 % | c | 4940 | 21190 49713 | 8546 4940 124042 25.1 | 0.239 % | c | 5165 | 21190 49713 | 9400 5165 129504 25.1 | 0.239 % | c | 5505 | 21190 49713 | 10340 5505 136992 24.9 | 0.239 % | c ============================================================================== c [1mFound solution: 48[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 | 5973 | 21208 49761 | 7069 5973 150436 25.2 | 0.239 % | c | 6073 | 21208 49761 | 7775 6073 153259 25.2 | 0.250 % | c | 6223 | 21208 49761 | 8553 6223 157315 25.3 | 0.250 % | c | 6448 | 21208 49761 | 9408 6448 163986 25.4 | 0.250 % | c ============================================================================== c [1mFound solution: 45[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6591 | 21213 49775 | 7071 6591 167843 25.5 | 0.250 % | c | 6692 | 21213 49775 | 7778 6692 170216 25.4 | 0.261 % | c | 6842 | 21213 49775 | 8555 6842 173791 25.4 | 0.261 % | c | 7067 | 21213 49775 | 9411 7067 178477 25.3 | 0.261 % | c | 7404 | 21213 49775 | 10352 7404 185776 25.1 | 0.261 % | c | 7910 | 21213 49775 | 11387 7910 198125 25.0 | 0.260 % | c ============================================================================== c [1mFound solution: 39[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 | 8134 | 21226 49807 | 7075 8134 204355 25.1 | 0.260 % | c | 8235 | 21226 49807 | 7782 4168 100571 24.1 | 0.271 % | c | 8385 | 21226 49807 | 8560 4318 104623 24.2 | 0.271 % | c ============================================================================== c [1mFound solution: 37[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8398 | 21231 49821 | 7077 4331 104903 24.2 | 0.271 % | c | 8498 | 21231 49821 | 7784 4431 107306 24.2 | 0.282 % | c | 8651 | 21231 49821 | 8563 4584 109439 23.9 | 0.282 % | c | 8876 | 21231 49821 | 9419 4809 113165 23.5 | 0.282 % | c | 9214 | 21231 49821 | 10361 5147 118064 22.9 | 0.282 % | c | 9720 | 21231 49821 | 11397 5653 125121 22.1 | 0.282 % | c ============================================================================== c [1mFound solution: 34[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 | 10353 | 21236 49838 | 7078 6286 140504 22.4 | 0.282 % | c | 10454 | 21236 49838 | 7785 6387 142965 22.4 | 0.293 % | c | 10605 | 21236 49838 | 8564 6538 146788 22.5 | 0.293 % | c | 10830 | 21236 49838 | 9420 6763 151820 22.4 | 0.293 % | c | 11168 | 21236 49838 | 10362 7101 159017 22.4 | 0.292 % | c | 11675 | 21236 49838 | 11399 7608 168410 22.1 | 0.292 % | 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 : 43 c conflicts : 12344 (393 /sec) c decisions : 19824 (631 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 31.4352 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.85 0.95 0.90 2/54 23714 Raw data (stat): 23714 (runsolver) R 23713 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489256848 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0002 s] Raw data (loadavg): 0.87 0.95 0.90 2/54 23714 Raw data (stat): 23714 (minisat+) R 23713 30854 30853 0 -1 0 1199 0 0 0 995 3 0 0 25 0 1 0 489256848 6905856 1169 4294967295 134512640 134672761 3221224624 3221223792 134561256 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1686 1169 603 41 0 1645 0 vsize: 6744 [startup+20.0014 s] Raw data (loadavg): 0.89 0.96 0.91 2/54 23714 Raw data (stat): 23714 (minisat+) R 23713 30854 30853 0 -1 0 1346 0 0 0 1994 5 0 0 25 0 1 0 489256848 7569408 1316 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1848 1316 603 41 0 1807 0 vsize: 7392 [startup+30.0032 s] Raw data (loadavg): 0.91 0.96 0.91 2/54 23714 Raw data (stat): 23714 (minisat+) R 23713 30854 30853 0 -1 0 1364 0 0 0 2994 5 0 0 25 0 1 0 489256848 7569408 1334 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1848 1334 603 41 0 1807 0 vsize: 7392 [startup+31.5082 s] Raw data (loadavg): 0.91 0.96 0.91 1/53 23714 Raw data (stat): 23714 (minisat+) R 23713 30854 30853 0 -1 0 1364 0 0 0 2994 5 0 0 25 0 1 0 489256848 7569408 1334 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1848 1334 603 41 0 1807 0 vsize: 0 Child status: 30 Real time (s): 31.5079 CPU time (s): 31.5022 CPU user time (s): 31.4392 CPU system time (s): 0.06299 CPU usage (%): 99.982 Max. virtual memory (Kb): 7392 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 34 #### END VERIFIER DATA ####