Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8a1.opb |
MD5SUM | b3cc2686c19f6e4ddbbeb52b8905fbf9 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 54 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 132 |
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 | 132 |
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 | 132 |
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.763883 |
Number of variables | 132 |
Total number of constraints | 252 |
Number of constraints which are clauses | 252 |
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 | 8 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc32 THE 2005-04-14 04:00:16 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4675 boxname=wulflinc32 idbench=163 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b3cc2686c19f6e4ddbbeb52b8905fbf9 /oldhome/oroussel/tmp/wulflinc32/normalized-ii8a1.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc32/normalized-ii8a1.opb /oldhome/oroussel/tmp/wulflinc32/normalized-ii8a1.opb IDLAUNCH: 4675 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.085 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.085 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: 1034724 kB MemFree: 701556 kB Buffers: 35348 kB Cached: 186140 kB SwapCached: 1212 kB Active: 147444 kB Inactive: 154364 kB HighTotal: 131072 kB HighFree: 256 kB LowTotal: 903652 kB LowFree: 701300 kB SwapTotal: 2097892 kB SwapFree: 2096680 kB Dirty: 2340 kB Writeback: 0 kB Mapped: 81768 kB Slab: 25428 kB Committed_AS: 174000 kB PageTables: 432 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 04:00:18 (client local time) WITH STATUS 30 IN 2.20966 SECONDS stats: 4675 0 2.20966 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 252 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................ c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 252 582 | 84 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 61[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3660 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5 | 8382 19635 | 2794 5 46 9.2 | 0.000 % | c ============================================================================== c [1mFound solution: 60[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15 | 8167 19141 | 2722 14 238 17.0 | 0.000 % | c | 115 | 7400 17390 | 2994 89 665 7.5 | 10.221 % | c | 265 | 5953 14082 | 3293 115 729 6.3 | 26.211 % | c ============================================================================== c [1mFound solution: 59[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 275 | 5489 13016 | 1829 79 537 6.8 | 26.211 % | c | 377 | 4893 11640 | 2011 167 2620 15.7 | 37.766 % | c | 529 | 4806 11441 | 2213 316 6361 20.1 | 38.688 % | c ============================================================================== c [1mFound solution: 58[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 688 | 4490 10705 | 1496 460 10554 22.9 | 38.688 % | c ============================================================================== c [1mFound solution: 57[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 696 | 4539 10828 | 1513 468 10819 23.1 | 38.688 % | c | 796 | 4539 10828 | 1664 568 14060 24.8 | 42.083 % | c | 949 | 4539 10828 | 1830 721 17969 24.9 | 42.083 % | c ============================================================================== c [1mFound solution: 56[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1094 | 4464 10647 | 1488 848 20298 23.9 | 42.083 % | c ============================================================================== c [1mFound solution: 55[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1104 | 4503 10746 | 1501 858 20509 23.9 | 42.083 % | c | 1205 | 4503 10746 | 1651 959 23821 24.8 | 42.787 % | c | 1356 | 4393 10490 | 1816 1107 27945 25.2 | 44.118 % | c | 1581 | 4149 9926 | 1997 1324 33474 25.3 | 46.919 % | c | 1920 | 3890 9327 | 2197 1650 42188 25.6 | 49.895 % | c ============================================================================== c [1mFound solution: 54[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1974 | 3869 9267 | 1289 1691 42726 25.3 | 49.895 % | c | 2076 | 3869 9267 | 1417 1793 45035 25.1 | 50.142 % | c | 2234 | 3869 9267 | 1559 1951 48697 25.0 | 50.140 % | c | 2460 | 3737 8958 | 1715 2174 53463 24.6 | 51.680 % | c | 2797 | 3737 8958 | 1887 2511 60489 24.1 | 51.680 % | c | 3303 | 3652 8760 | 2075 2551 58557 23.0 | 52.555 % | c ============================================================================== c [1mOptimal solution: 54[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 c _______________________________________________________________________________ c c restarts : 24 c conflicts : 3558 (1625 /sec) c decisions : 7756 (3542 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 2.18967 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.96 0.96 0.91 2/53 15194 Raw data (stat): 15194 (runsolver) R 15193 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481538845 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+2.221 s] Raw data (loadavg): 0.96 0.96 0.91 1/52 15194 Raw data (stat): 15194 (runsolver) R 15193 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481538845 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 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): 2.22012 CPU time (s): 2.20966 CPU user time (s): 2.19067 CPU system time (s): 0.018997 CPU usage (%): 99.529 Max. virtual memory (Kb): 1028 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 54 #### END VERIFIER DATA ####