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 wulflinc20 THE 2005-04-21 05:46:11 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=16741 boxname=wulflinc20 idbench=1288 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 9e4c4999c6f95fcef879d3d86840d71a /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-bm23.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-bm23.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-bm23.opb IDLAUNCH: 16741 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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.215 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: 868596 kB Buffers: 8608 kB Cached: 134016 kB SwapCached: 516 kB Active: 30480 kB Inactive: 114112 kB HighTotal: 131008 kB HighFree: 35784 kB LowTotal: 903652 kB LowFree: 832812 kB SwapTotal: 2097892 kB SwapFree: 2096480 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5112 kB Slab: 15856 kB Committed_AS: 63584 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 05:47:50 (client local time) WITH STATUS 30 IN 98.1501 SECONDS stats: 16741 0 98.1501 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]---> Adder-cost: 72 maxlim: 51 bits: 7/6 c ---[ 18]---> Adder-cost: 72 maxlim: 66 bits: 7/7 c ---[ 17]---> Adder-cost: 68 maxlim: 67 bits: 7/7 c ---[ 16]---> Adder-cost: 72 maxlim: 30 bits: 6/5 c ---[ 15]---> Adder-cost: 82 maxlim: 67 bits: 8/7 c ---[ 14]---> Adder-cost: 79 maxlim: 51 bits: 7/6 c ---[ 13]---> Adder-cost: 62 maxlim: 48 bits: 7/6 c ---[ 12]---> Adder-cost: 76 maxlim: 55 bits: 7/6 c ---[ 11]---> Adder-cost: 64 maxlim: 50 bits: 7/6 c ---[ 10]---> Adder-cost: 28 maxlim: 4 bits: 4/3 c ---[ 9]---> Adder-cost: 68 maxlim: 53 bits: 7/6 c ---[ 8]---> Adder-cost: 68 maxlim: 54 bits: 7/6 c ---[ 7]---> Adder-cost: 59 maxlim: 36 bits: 7/6 c ---[ 6]---> Adder-cost: 71 maxlim: 45 bits: 7/6 c ---[ 5]---> Adder-cost: 66 maxlim: 53 bits: 7/6 c ---[ 4]---> Adder-cost: 86 maxlim: 54 bits: 7/6 c ---[ 3]---> Adder-cost: 59 maxlim: 40 bits: 7/6 c ---[ 2]---> Adder-cost: 61 maxlim: 47 bits: 7/6 c ---[ 1]---> Adder-cost: 74 maxlim: 92 bits: 8/7 c ---[ 0]---> Adder-cost: 59 maxlim: 49 bits: 7/6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 8702 30830 | 2900 0 0 nan | 0.000 % | c | 100 | 8702 30830 | 3190 100 992 9.9 | 4.796 % | c | 250 | 8702 30830 | 3509 250 4170 16.7 | 4.796 % | c | 477 | 8702 30830 | 3859 477 8399 17.6 | 4.796 % | c | 815 | 8702 30830 | 4245 815 13930 17.1 | 4.796 % | c | 1321 | 8702 30830 | 4670 1321 23833 18.0 | 4.796 % | c | 2080 | 8702 30830 | 5137 2080 38152 18.3 | 4.796 % | c | 3220 | 8702 30830 | 5651 3220 60851 18.9 | 4.796 % | c | 4928 | 8702 30830 | 6216 4928 90899 18.4 | 4.796 % | c | 7493 | 8702 30830 | 6838 4286 66931 15.6 | 4.796 % | c | 11337 | 8702 30830 | 7521 4627 70269 15.2 | 4.796 % | c | 17103 | 8702 30830 | 8274 6493 110380 17.0 | 4.796 % | c | 25754 | 8702 30830 | 9101 6695 106041 15.8 | 4.796 % | c ============================================================================== c [1mFound solution: 56[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 72 maxlim: 68 bits: 7/7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28685 | 9175 32513 | 3058 4998 78635 15.7 | 4.796 % | c | 28785 | 9175 32513 | 3363 2599 38590 14.8 | 4.759 % | c | 28937 | 9175 32513 | 3700 2751 40869 14.9 | 4.759 % | c | 29164 | 9175 32513 | 4070 2978 44987 15.1 | 4.759 % | c | 29502 | 9175 32513 | 4477 3316 50929 15.4 | 4.759 % | c | 30009 | 9175 32513 | 4924 3823 59454 15.6 | 4.759 % | c | 30768 | 9175 32513 | 5417 4582 72551 15.8 | 4.759 % | c | 31907 | 9175 32513 | 5959 2914 41883 14.4 | 4.759 % | c | 33616 | 9175 32513 | 6555 4623 72973 15.8 | 4.759 % | c ============================================================================== c [1mFound solution: 45[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 79 bits: 7/7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35319 | 9176 32516 | 3058 6326 103508 16.4 | 4.759 % | c | 35419 | 9176 32516 | 3363 1682 22307 13.3 | 4.823 % | c | 35569 | 9176 32516 | 3700 1832 25475 13.9 | 4.823 % | c | 35794 | 9176 32516 | 4070 2057 29800 14.5 | 4.823 % | c | 36133 | 9176 32516 | 4477 2396 35615 14.9 | 4.823 % | c | 36639 | 9176 32516 | 4924 2902 45030 15.5 | 4.823 % | c | 37399 | 9176 32516 | 5417 3662 57069 15.6 | 4.823 % | c | 38540 | 9176 32516 | 5959 4803 74556 15.5 | 4.823 % | c | 40249 | 9176 32516 | 6555 3472 51085 14.7 | 4.823 % | c | 42811 | 9176 32516 | 7210 6034 91019 15.1 | 4.823 % | c | 46655 | 9176 32516 | 7931 6190 89046 14.4 | 4.823 % | c | 52421 | 9176 32516 | 8724 7916 133950 16.9 | 4.823 % | c | 61073 | 9176 32516 | 9597 7686 122000 15.9 | 4.823 % | c | 74047 | 9176 32516 | 10557 5951 90564 15.2 | 4.823 % | c ============================================================================== c [1mFound solution: 42[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 82 bits: 7/7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 76283 | 9184 32551 | 3061 8187 137734 16.8 | 4.823 % | c | 76384 | 9184 32551 | 3367 2148 33182 15.4 | 4.950 % | c | 76536 | 9184 32551 | 3703 2300 35366 15.4 | 4.950 % | c | 76761 | 9184 32551 | 4074 2525 38962 15.4 | 4.950 % | c | 77100 | 9184 32551 | 4481 2864 43988 15.4 | 4.950 % | c | 77608 | 9184 32551 | 4929 3372 53292 15.8 | 4.950 % | c | 78368 | 9184 32551 | 5422 4132 68777 16.6 | 4.950 % | c | 79509 | 9184 32551 | 5965 5273 91157 17.3 | 4.950 % | c | 81217 | 9184 32551 | 6561 3869 60774 15.7 | 4.950 % | c | 83779 | 9184 32551 | 7217 6431 106245 16.5 | 4.950 % | c ============================================================================== c [1mFound solution: 41[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 83 bits: 7/7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 85280 | 9185 32556 | 3061 4250 63901 15.0 | 4.950 % | c | 85380 | 9185 32556 | 3367 2225 30397 13.7 | 5.013 % | c | 85531 | 9185 32556 | 3703 2376 32873 13.8 | 5.013 % | c | 85757 | 9185 32556 | 4074 2602 37961 14.6 | 5.013 % | c | 86094 | 9185 32556 | 4481 2939 45113 15.3 | 5.013 % | c ============================================================================== c [1mFound solution: 34[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 90 bits: 7/7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86225 | 9193 32591 | 3064 3070 47511 15.5 | 5.013 % | c | 86325 | 9193 32591 | 3370 3170 49330 15.6 | 5.200 % | c | 86475 | 9193 32591 | 3707 3320 51694 15.6 | 5.200 % | c | 86700 | 9193 32591 | 4078 3545 56099 15.8 | 5.200 % | c | 87039 | 9193 32591 | 4486 3884 62679 16.1 | 5.200 % | c | 87547 | 9193 32591 | 4934 4392 72877 16.6 | 5.200 % | c | 88306 | 9193 32591 | 5428 5151 86336 16.8 | 5.200 % | c | 89445 | 9193 32591 | 5970 3432 54446 15.9 | 5.200 % | c | 91153 | 9193 32591 | 6567 5140 78633 15.3 | 5.200 % | c | 93715 | 9193 32591 | 7224 4337 62992 14.5 | 5.200 % | c | 97560 | 9193 32591 | 7947 4515 59962 13.3 | 5.200 % | c | 103328 | 9193 32591 | 8741 6256 79727 12.7 | 5.200 % | c | 111977 | 9193 32591 | 9616 6005 75297 12.5 | 5.200 % | c | 124953 | 9193 32591 | 10577 9225 120036 13.0 | 5.200 % | 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 : 65 c conflicts : 138624 (1413 /sec) c decisions : 159065 (1621 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 98.1121 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.83 0.93 0.91 2/54 29226 Raw data (stat): 29226 (runsolver) R 29225 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542666553 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0017 s] Raw data (loadavg): 0.85 0.93 0.91 2/54 29226 Raw data (stat): 29226 (minisat+) R 29225 27565 27564 0 -1 0 679 0 0 0 997 1 0 0 25 0 1 0 542666553 4366336 657 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1066 657 603 41 0 1025 0 vsize: 4264 [startup+20.002 s] Raw data (loadavg): 0.88 0.93 0.91 2/54 29226 Raw data (stat): 29226 (minisat+) R 29225 27565 27564 0 -1 0 744 0 0 0 1996 2 0 0 25 0 1 0 542666553 4632576 722 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1131 722 603 41 0 1090 0 vsize: 4524 [startup+30.0015 s] Raw data (loadavg): 0.89 0.93 0.91 2/54 29226 Raw data (stat): 29226 (minisat+) R 29225 27565 27564 0 -1 0 756 0 0 0 2995 2 0 0 25 0 1 0 542666553 4632576 734 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1131 734 603 41 0 1090 0 vsize: 4524 [startup+40.0015 s] Raw data (loadavg): 0.91 0.93 0.91 2/54 29226 Raw data (stat): 29226 (minisat+) R 29225 27565 27564 0 -1 0 778 0 0 0 3995 2 0 0 25 0 1 0 542666553 4780032 756 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1167 756 603 41 0 1126 0 vsize: 4668 [startup+50.002 s] Raw data (loadavg): 0.92 0.94 0.91 2/54 29226 Raw data (stat): 29226 (minisat+) R 29225 27565 27564 0 -1 0 803 0 0 0 4995 2 0 0 25 0 1 0 542666553 4911104 781 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1199 781 603 41 0 1158 0 vsize: 4796 [startup+60.0017 s] Raw data (loadavg): 0.93 0.94 0.91 2/54 29226 Raw data (stat): 29226 (minisat+) R 29225 27565 27564 0 -1 0 810 0 0 0 5995 2 0 0 25 0 1 0 542666553 4911104 788 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1199 788 603 41 0 1158 0 vsize: 4796 [startup+70.003 s] Raw data (loadavg): 0.94 0.94 0.91 2/54 29226 Raw data (stat): 29226 (minisat+) R 29225 27565 27564 0 -1 0 811 0 0 0 6995 3 0 0 25 0 1 0 542666553 4911104 789 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1199 789 603 41 0 1158 0 vsize: 4796 [startup+80.0031 s] Raw data (loadavg): 0.95 0.94 0.91 2/54 29226 Raw data (stat): 29226 (minisat+) R 29225 27565 27564 0 -1 0 821 0 0 0 7994 3 0 0 25 0 1 0 542666553 4911104 799 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1199 799 603 41 0 1158 0 vsize: 4796 [startup+90.0028 s] Raw data (loadavg): 0.96 0.94 0.91 2/54 29226 Raw data (stat): 29226 (minisat+) R 29225 27565 27564 0 -1 0 827 0 0 0 8994 3 0 0 25 0 1 0 542666553 5054464 805 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1234 805 603 41 0 1193 0 vsize: 4936 [startup+98.1717 s] Raw data (loadavg): 0.96 0.94 0.91 1/53 29226 Raw data (stat): 29226 (minisat+) R 29225 27565 27564 0 -1 0 827 0 0 0 8994 3 0 0 25 0 1 0 542666553 5054464 805 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1234 805 603 41 0 1193 0 vsize: 0 Child status: 30 Real time (s): 98.1715 CPU time (s): 98.1501 CPU user time (s): 98.1131 CPU system time (s): 0.036994 CPU usage (%): 99.9782 Max. virtual memory (Kb): 4936 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 34 #### END VERIFIER DATA ####