Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-rd-rplusc-21.opb |
MD5SUM | 62166f7982a2b3c488537a2a2dbe4149 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 35 |
Biggest coefficient in the objective function | 1048576 |
Number of bits for the biggest coefficient in the objective function | 21 |
Sum of the numbers in the objective function | 3735451 |
Number of bits of the sum of numbers in the objective function | 22 |
Biggest number in a constraint | 383602153706972160 |
Number of bits of the biggest number in a constraint | 59 |
Biggest sum of numbers in a constraint | 772928706545624815 |
Number of bits of the biggest sum of numbers | 60 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 39.177 |
Number of variables | 2644 |
Total number of constraints | 126450 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 699 |
Number of constraints which are nor clauses,nor cardinality constraints | 125751 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 130 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc30 THE 2005-05-25 13:34:59 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=21394 boxname=wulflinc30 idbench=1382 idsolver=14 numberseed=0 MD5SUM SOLVER: d29da23ec752be69e0579424c0f0767e /oldhome/oroussel/solvers/sat4jPseudoBis.jar MD5SUM BENCH: 62166f7982a2b3c488537a2a2dbe4149 /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-rd-rplusc-21.opb REAL COMMAND: java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudoBis.jar /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-rd-rplusc-21.opb IDLAUNCH: 21394 /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: 277924 kB Buffers: 38388 kB Cached: 694344 kB SwapCached: 716 kB Active: 268992 kB Inactive: 465900 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 277672 kB SwapTotal: 2097892 kB SwapFree: 2096344 kB Dirty: 4 kB Writeback: 0 kB Mapped: 5016 kB Slab: 16064 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 13:39:44 (client local time) WITH STATUS 20 IN 294.437 SECONDS stats: 21394 7 294.437 20 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c SAT4J: a SATisfiability library for Java (c) 2004-2005 Daniel Le Berre c This is free software under the GNU LGPL licence. See www.sat4j.org for details. c version Special PB05 Second trial c --- Begin Solver configuration --- c org.sat4j.minisat.uip.FirstUIP@1e4cbc4 c org.sat4j.minisat.constraints.PBMinDataStructure@1fdc96c c org.sat4j.minisat.learning.MiniSATLearning@b2fd8f c conflictBoundIncFactor=1.5 learntBoundIncFactor=1.1 initLearntBoundConstraintFactor=0.5 initConflictBound=100 c c --- End Solver configuration --- c solving /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-rd-rplusc-21.opb c reading problem ... done. Time 228.653 ms. c #vars 2644 c #constraints 125844 c starts : 1 c conflicts : 8 c decisions : 62 c propagations : 2343 c inspects : 58801 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 7 c root simplifications : 1 s UNSATISFIABLE c Total CPU time (ms) : 280.437 #### 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): 1.08 1.01 1.00 2/54 7584 Raw data (stat): 7584 (runsolver) R 7583 22056 22055 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 839275222 1052672 99 4294967295 134512640 135381576 3221224400 3221219620 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.0006 s] Raw data (loadavg): 1.07 1.01 1.00 2/63 7593 Raw data (stat): 7584 (java) S 7583 22056 22055 0 -1 0 18034 0 1 0 776 41 0 0 25 0 10 0 839275222 859758592 22136 4294967295 134512640 134569956 3221224368 3221213632 1073943035 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209902 22139 13086 16 0 209886 0 vsize: 839608 [startup+20.0007 s] Raw data (loadavg): 1.06 1.01 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18036 0 1 0 1638 47 0 0 25 0 10 0 839275222 856743936 28533 4294967295 134512640 134569956 3221224368 3221214808 1131173793 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 28533 13086 16 0 209150 0 vsize: 836664 [startup+30.0007 s] Raw data (loadavg): 1.05 1.01 1.00 2/63 7593 Raw data (stat): 7584 (java) S 7583 22056 22055 0 -1 0 18037 0 1 0 2500 53 0 0 25 0 10 0 839275222 856743936 34360 4294967295 134512640 134569956 3221224368 3221213248 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 34360 13086 16 0 209150 0 vsize: 836664 [startup+40.0059 s] Raw data (loadavg): 1.04 1.01 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18037 0 1 0 3375 59 0 0 25 0 10 0 839275222 856743936 40137 4294967295 134512640 134569956 3221224368 3221214784 1131155090 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 40137 13086 16 0 209150 0 vsize: 836664 [startup+50.0063 s] Raw data (loadavg): 1.04 1.01 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 4227 64 0 0 25 0 10 0 839275222 856743936 46391 4294967295 134512640 134569956 3221224368 3221214800 1131164342 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209166 46391 13086 16 0 209150 0 vsize: 836664 [startup+60.0059 s] Raw data (loadavg): 1.03 1.01 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 5067 70 0 0 25 0 10 0 839275222 856743936 52925 4294967295 134512640 134569956 3221224368 3221214800 1131173818 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 52925 13086 16 0 209150 0 vsize: 836664 [startup+70.0063 s] Raw data (loadavg): 1.02 1.01 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 5956 78 0 0 25 0 10 0 839275222 856743936 57588 4294967295 134512640 134569956 3221224368 3221214736 1131156969 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209166 57588 13086 16 0 209150 0 vsize: 836664 [startup+80.0067 s] Raw data (loadavg): 1.02 1.01 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 6800 85 0 0 25 0 10 0 839275222 856743936 64233 4294967295 134512640 134569956 3221224368 3221214736 1131156936 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209166 64233 13086 16 0 209150 0 vsize: 836664 [startup+90.0074 s] Raw data (loadavg): 1.02 1.01 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 7646 91 0 0 25 0 10 0 839275222 856743936 70773 4294967295 134512640 134569956 3221224368 3221214512 1131219510 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 70773 13086 16 0 209150 0 vsize: 836664 [startup+100.008 s] Raw data (loadavg): 1.01 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 8492 95 0 0 25 0 10 0 839275222 856743936 77390 4294967295 134512640 134569956 3221224368 3221213968 1131214709 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209166 77390 13086 16 0 209150 0 vsize: 836664 [startup+110.008 s] Raw data (loadavg): 1.01 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) S 7583 22056 22055 0 -1 0 18040 0 1 0 9344 102 0 0 25 0 10 0 839275222 856743936 83590 4294967295 134512640 134569956 3221224368 3221213184 1073943035 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209166 83591 13086 16 0 209150 0 vsize: 836664 [startup+120.009 s] Raw data (loadavg): 1.01 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 10229 110 0 0 25 0 10 0 839275222 856743936 88309 4294967295 134512640 134569956 3221224368 3221214784 1131155053 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 88309 13086 16 0 209150 0 vsize: 836664 [startup+130.009 s] Raw data (loadavg): 1.01 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 11065 117 0 0 25 0 10 0 839275222 856743936 95304 4294967295 134512640 134569956 3221224368 3221214816 1131156799 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209166 95304 13086 16 0 209150 0 vsize: 836664 [startup+140.009 s] Raw data (loadavg): 1.01 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 11954 124 0 0 25 0 10 0 839275222 856743936 99967 4294967295 134512640 134569956 3221224368 3221214800 1131173602 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 99967 13086 16 0 209150 0 vsize: 836664 [startup+150.01 s] Raw data (loadavg): 1.00 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 12793 130 0 0 25 0 10 0 839275222 856743936 106959 4294967295 134512640 134569956 3221224368 3221214796 1131155119 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 106959 13086 16 0 209150 0 vsize: 836664 [startup+160.01 s] Raw data (loadavg): 1.00 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 13630 136 0 0 25 0 10 0 839275222 856743936 113965 4294967295 134512640 134569956 3221224368 3221214784 1131155063 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 113965 13086 16 0 209150 0 vsize: 836664 [startup+170.01 s] Raw data (loadavg): 1.00 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 14520 142 0 0 25 0 10 0 839275222 856743936 118669 4294967295 134512640 134569956 3221224368 3221214784 1131157078 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209166 118669 13086 16 0 209150 0 vsize: 836664 [startup+180.01 s] Raw data (loadavg): 1.00 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 15360 147 0 0 25 0 10 0 839275222 856743936 125684 4294967295 134512640 134569956 3221224368 3221214600 1131268075 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 125684 13086 16 0 209150 0 vsize: 836664 [startup+190.01 s] Raw data (loadavg): 1.00 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 16249 154 0 0 25 0 10 0 839275222 856743936 130540 4294967295 134512640 134569956 3221224368 3221214800 1131173892 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 130540 13086 16 0 209150 0 vsize: 836664 [startup+200.01 s] Raw data (loadavg): 1.00 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 17088 159 0 0 25 0 10 0 839275222 856743936 137558 4294967295 134512640 134569956 3221224368 3221214848 1131180417 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 137558 13086 16 0 209150 0 vsize: 836664 [startup+210.01 s] Raw data (loadavg): 1.00 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 17926 165 0 0 25 0 10 0 839275222 856743936 144591 4294967295 134512640 134569956 3221224368 3221214704 1131133039 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 144591 13086 16 0 209150 0 vsize: 836664 [startup+220.011 s] Raw data (loadavg): 1.00 1.00 1.00 2/63 7593 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18040 0 1 0 18816 172 0 0 25 0 10 0 839275222 856743936 149248 4294967295 134512640 134569956 3221224368 3221214736 1131157108 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209166 149248 13086 16 0 209150 0 vsize: 836664 [startup+230.011 s] Raw data (loadavg): 1.00 1.00 1.00 4/64 7594 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18072 0 1 0 19645 178 0 0 24 0 11 0 839275222 858320896 156650 4294967295 134512640 134569956 3221224368 3221214840 1131130688 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209551 156650 13086 16 0 209535 0 vsize: 838204 [startup+240.012 s] Raw data (loadavg): 1.07 1.02 1.00 2/64 7594 Raw data (stat): 7584 (java) S 7583 22056 22055 0 -1 0 18090 0 1 0 19921 178 0 0 25 0 11 0 839275222 861818880 157434 4294967295 134512640 134569956 3221224368 3221213360 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 210405 157434 13086 16 0 210389 0 vsize: 841620 [startup+250.016 s] Raw data (loadavg): 1.06 1.02 1.00 2/64 7594 Raw data (stat): 7584 (java) S 7583 22056 22055 0 -1 0 18090 0 1 0 20139 178 0 0 25 0 11 0 839275222 862515200 159943 4294967295 134512640 134569956 3221224368 3221213232 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 210575 159943 13086 16 0 210559 0 vsize: 842300 [startup+260.02 s] Raw data (loadavg): 1.05 1.01 1.00 2/64 7594 Raw data (stat): 7584 (java) S 7583 22056 22055 0 -1 0 18090 0 1 0 20139 178 0 0 25 0 11 0 839275222 861466624 159770 4294967295 134512640 134569956 3221224368 3221213232 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 210319 159770 13086 16 0 210303 0 vsize: 841276 [startup+270.021 s] Raw data (loadavg): 1.04 1.01 1.00 2/64 7594 Raw data (stat): 7584 (java) S 7583 22056 22055 0 -1 0 18100 0 1 0 20258 178 0 0 25 0 11 0 839275222 861466624 159716 4294967295 134512640 134569956 3221224368 3221213296 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 210319 159716 13086 16 0 210303 0 vsize: 841276 [startup+280.041 s] Raw data (loadavg): 1.04 1.01 1.00 4/64 7594 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18100 0 1 0 20316 178 0 0 21 0 11 0 839275222 861466624 160141 4294967295 134512640 134569956 3221224368 3221213812 1073952732 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 210319 160141 13086 16 0 210303 0 vsize: 841276 [startup+281.755 s] Raw data (loadavg): 1.04 1.01 1.00 1/53 7595 Raw data (stat): 7584 (java) R 7583 22056 22055 0 -1 0 18100 0 1 0 20316 178 0 0 21 0 11 0 839275222 861466624 160141 4294967295 134512640 134569956 3221224368 3221213812 1073952732 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 210319 160141 13086 16 0 210303 0 vsize: 0 Child status: 20 Real time (s): 281.755 CPU time (s): 294.437 CPU user time (s): 289.216 CPU system time (s): 5.22121 CPU usage (%): 104.501 Max. virtual memory (Kb): 842300 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####