Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-jnh217.opb |
MD5SUM | c4040960fadc5a0c2fe39dd858a66385 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 89 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 200 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 200 |
Number of bits of the sum of numbers in the objective function | 8 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 200 |
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 | 1.02284 |
Number of variables | 200 |
Total number of constraints | 900 |
Number of constraints which are clauses | 900 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 11 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc24 THE 2005-04-14 00:21:28 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3948 boxname=wulflinc24 idbench=188 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c4040960fadc5a0c2fe39dd858a66385 /oldhome/oroussel/tmp/wulflinc24/normalized-jnh217.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc24/normalized-jnh217.opb /oldhome/oroussel/tmp/wulflinc24/normalized-jnh217.opb IDLAUNCH: 3948 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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: 843132 kB Buffers: 34356 kB Cached: 114748 kB SwapCached: 3828 kB Active: 50816 kB Inactive: 104952 kB HighTotal: 131008 kB HighFree: 13972 kB LowTotal: 903652 kB LowFree: 829160 kB SwapTotal: 2097892 kB SwapFree: 2094064 kB Dirty: 4 kB Writeback: 0 kB Mapped: 6924 kB Slab: 30116 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 00:21:38 (client local time) WITH STATUS 30 IN 9.56954 SECONDS stats: 3948 0 9.56954 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 900 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 887 4042 | 266 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 200/200 c | 0 | 880 3989 | -- 0 -- -- | -- | -7/-53 c | 0 | 880 3989 | 352 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 0.047992 s) c ============================================================================== c [1mFound solution: 95[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5812 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 59 | 7609 19740 | 2282 59 936 15.9 | 0.000 % | c -- subsuming c -- var.elim.: 1000/4524 c -- var.elim.: 2000/4524 c -- var.elim.: 3000/4524 c -- var.elim.: 4000/4524 c -- var.elim.: 4524/4524 c -- var.elim.: 1000/2203 c -- var.elim.: 2000/2203 c -- var.elim.: 2203/2203 c -- var.elim.: 1000/1272 c -- var.elim.: 1272/1272 c -- var.elim.: 848/848 c -- var.elim.: 608/608 c -- var.elim.: 339/339 c -- var.elim.: 24/24 c -- subsuming c -- var.elim.: 565/565 c -- var.elim.: 24/24 c | 59 | 2657 13735 | -- 59 -- -- | -- | -4952/-6004 c | 59 | 2657 13735 | 1062 59 936 15.9 | 0.000 % | c ============================================================================== c (current CPU-time: 1.39979 s) c ============================================================================== c [1mFound solution: 93[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 119 | 7340 25220 | 2201 119 3622 30.4 | 0.000 % | c -- subsuming c -- var.elim.: 1000/4238 c -- var.elim.: 2000/4238 c -- var.elim.: 3000/4238 c -- var.elim.: 4000/4238 c -- var.elim.: 4238/4238 c -- var.elim.: 1000/2002 c -- var.elim.: 2000/2002 c -- var.elim.: 2002/2002 c -- var.elim.: 1000/1222 c -- var.elim.: 1222/1222 c -- var.elim.: 786/786 c -- var.elim.: 631/631 c -- var.elim.: 221/221 c -- subsuming c -- var.elim.: 360/360 c -- var.elim.: 42/42 c | 119 | 2719 14622 | -- 119 -- -- | -- | -4621/-10597 c | 119 | 2719 14622 | 1087 119 3622 30.4 | 0.000 % | c ============================================================================== c (current CPU-time: 2.76958 s) c ============================================================================== c [1mFound solution: 92[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 150 | 2735 14674 | 820 150 5402 36.0 | 0.000 % | c -- subsuming c -- var.elim.: 97/97 c -- var.elim.: 23/23 c | 150 | 2715 14568 | -- 150 -- -- | -- | -11/-30 c | 150 | 2715 14568 | 1086 150 5402 36.0 | 0.000 % | c ============================================================================== c (current CPU-time: 2.97155 s) c ============================================================================== c [1mFound solution: 91[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 177 | 7060 25201 | 2117 177 9300 52.5 | 0.000 % | c -- subsuming c -- var.elim.: 1000/3960 c -- var.elim.: 2000/3960 c -- var.elim.: 3000/3960 c -- var.elim.: 3960/3960 c -- var.elim.: 1000/1851 c -- var.elim.: 1851/1851 c -- var.elim.: 1000/1100 c -- var.elim.: 1100/1100 c -- var.elim.: 716/716 c -- var.elim.: 557/557 c -- var.elim.: 259/259 c -- var.elim.: 26/26 c -- subsuming c -- var.elim.: 51/51 c | 177 | 2762 14912 | -- 177 -- -- | -- | -4298/-10288 c | 177 | 2762 14912 | 1104 177 9300 52.5 | 0.000 % | c | 281 | 2762 14912 | 1215 281 19908 70.8 | 0.763 % | c | 436 | 2762 14912 | 1336 436 42791 98.1 | 0.763 % | c | 667 | 2762 14912 | 1470 667 87259 130.8 | 0.763 % | c | 1004 | 2737 14629 | 1602 1002 105687 105.5 | 1.622 % | c ============================================================================== c (current CPU-time: 4.83926 s) c ============================================================================== c [1mFound solution: 90[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1307 | 2753 14677 | 825 1305 153323 117.5 | 1.622 % | c -- subsuming c -- var.elim.: 442/442 c -- var.elim.: 92/92 c -- var.elim.: 172/172 c -- var.elim.: 86/86 c | 1307 | 2726 14153 | -- 1305 -- -- | -- | -14/-190 c | 1307 | 2726 14153 | 1090 772 29235 37.9 | 1.622 % | c | 1407 | 2726 14153 | 1199 872 42174 48.4 | 2.108 % | c | 1564 | 2726 14153 | 1319 1029 73221 71.2 | 2.107 % | c | 1791 | 2726 14153 | 1451 1256 120926 96.3 | 2.109 % | c | 2129 | 2726 14153 | 1596 1594 164323 103.1 | 2.107 % | c ============================================================================== c (current CPU-time: 5.87511 s) c ============================================================================== c [1mFound solution: 89[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2456 | 7364 25531 | 2209 1921 229991 119.7 | 2.107 % | c -- subsuming c -- var.elim.: 1000/4219 c -- var.elim.: 2000/4219 c -- var.elim.: 3000/4219 c -- var.elim.: 4000/4219 c -- var.elim.: 4219/4219 c -- var.elim.: 1000/1999 c -- var.elim.: 1999/1999 c -- var.elim.: 1000/1220 c -- var.elim.: 1220/1220 c -- var.elim.: 808/808 c -- var.elim.: 686/686 c -- var.elim.: 448/448 c -- var.elim.: 104/104 c -- var.elim.: 3/3 c -- subsuming c -- var.elim.: 367/367 c -- var.elim.: 33/33 c | 2456 | 2786 15102 | -- 1921 -- -- | -- | -4578/-10428 c | 2456 | 2786 15102 | 1114 1919 229744 119.7 | 2.107 % | c | 2559 | 2786 15102 | 1225 957 122734 128.2 | 2.414 % | c | 2712 | 2786 15102 | 1348 1110 142597 128.5 | 2.414 % | c | 2937 | 2786 15102 | 1483 1335 173492 130.0 | 2.412 % | c | 3277 | 2786 15102 | 1631 1145 117573 102.7 | 2.412 % | c | 3783 | 2786 15102 | 1794 1651 167625 101.5 | 2.413 % | c | 4544 | 2786 15102 | 1974 1786 139649 78.2 | 2.413 % | c ============================================================================== c [1mOptimal solution: 89[0m s OPTIMUM FOUND v -x1 x2 -x3 x4 -x5 x6 x7 -x8 x9 -x10 -x11 x12 x13 -x14 -x15 x16 -x17 x18 -x19 -x20 x21 -x22 -x23 x24 x25 -x26 x27 -x28 x29 -x30 -x31 x32 x33 -x34 -x35 -x36 -x37 x38 -x39 x40 -x41 -x42 -x43 -x44 -x45 x46 -x47 -x48 -x49 x50 x51 -x52 x53 -x54 -x55 x56 x57 -x58 x59 -x60 -x61 -x62 x63 -x64 -x65 x66 x67 -x68 -x69 x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 x79 -x80 -x81 x82 -x83 x84 x85 -x86 -x87 x88 -x89 x90 -x91 x92 x93 -x94 x95 -x96 x97 -x98 -x99 x100 -x101 -x102 -x103 x104 x105 -x106 -x107 x108 x109 -x110 x111 -x112 -x113 -x114 -x115 x116 x117 -x118 -x119 x120 x121 -x122 x123 -x124 -x125 x126 -x127 x128 x129 -x130 -x131 -x132 x133 -x134 -x135 x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 -x147 -x148 x149 -x150 -x151 x152 -x153 x154 x155 -x156 -x157 x158 x159 -x160 -x161 x162 x163 -x164 x165 -x166 -x167 x168 -x169 x170 x171 -x172 x173 -x174 x175 -x176 -x177 x178 -x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 x189 -x190 x191 -x192 x193 -x194 -x195 x196 x197 -x198 x199 -x200 c _______________________________________________________________________________ c c restarts : 21 c conflicts : 5470 (581 /sec) c decisions : 11808 (1254 /sec) c propagations : 754879 (80165 /sec) c inspects : 3585395 (380754 /sec) c CPU time : 9.41657 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.67 0.88 0.88 2/54 1248 Raw data (stat): 1248 (runsolver) R 1247 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480226820 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.58694 s] Raw data (loadavg): 0.72 0.89 0.88 1/53 1248 Raw data (stat): 1248 (runsolver) R 1247 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480226820 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 0 Child status: 30 Real time (s): 9.58664 CPU time (s): 9.56954 CPU user time (s): 9.41857 CPU system time (s): 0.150977 CPU usage (%): 99.8217 Max. virtual memory (Kb): 1028 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 89 #### END VERIFIER DATA ####