Name | submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-c8.opb |
MD5SUM | 9b291040ec2b77d0bffb739c0db80d53 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1194 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 239 |
Biggest coefficient in the objective function | 61 |
Number of bits for the biggest coefficient in the objective function | 6 |
Sum of the numbers in the objective function | 10012 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 61 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 10012 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 33.9268 |
Number of variables | 239 |
Total number of constraints | 524 |
Number of constraints which are clauses | 520 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 4 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 36 |
LAUNCH ON wulflinc22 THE 2005-09-18 09:05:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=249 boxname=wulflinc22 idbench=249 idsolver=1 numberseed=0 MD5SUM SOLVER: 38f99674050b34630888bf623b924b59 /oldhome/oroussel/solvers/bsolo MD5SUM BENCH: 9b291040ec2b77d0bffb739c0db80d53 /oldhome/oroussel/tmp/wulflinc22/normalized-c8.opb REAL COMMAND: bsolo /oldhome/oroussel/tmp/wulflinc22/normalized-c8.opb IDLAUNCH: 249 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 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.031 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: 950100 kB Buffers: 33132 kB Cached: 24336 kB SwapCached: 536 kB Active: 53204 kB Inactive: 6768 kB HighTotal: 131008 kB HighFree: 104720 kB LowTotal: 903652 kB LowFree: 845380 kB SwapTotal: 2097892 kB SwapFree: 2096832 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5856 kB Slab: 18964 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 09:06:27 (client local time) WITH STATUS 30 IN 33.9268 SECONDS stats: 249 0 33.9268 30
c INFO: OSL Context initialized. c Initial problem consists of 239 variables and 524 constraints. c preprocess terminated. Elapsed time: 0.15 c After prepocess the problem consists of 228 variables and 485 constraints. c Initial Lower Bound: 59 c NEW SOLUTION FOUND: 2079 @ 0.182 @ #Dec. 34 c NEW SOLUTION FOUND: 2046 @ 0.184 @ #Dec. 35 c NEW SOLUTION FOUND: 2030 @ 0.186 @ #Dec. 38 c NEW SOLUTION FOUND: 2023 @ 0.19 @ #Dec. 44 c NEW SOLUTION FOUND: 2007 @ 0.194 @ #Dec. 48 c NEW SOLUTION FOUND: 2000 @ 0.197 @ #Dec. 54 c NEW SOLUTION FOUND: 1984 @ 0.2 @ #Dec. 58 c NEW SOLUTION FOUND: 1977 @ 0.212 @ #Dec. 75 c NEW SOLUTION FOUND: 1961 @ 0.214 @ #Dec. 78 c NEW SOLUTION FOUND: 1943 @ 0.248 @ #Dec. 122 c NEW SOLUTION FOUND: 1938 @ 0.358 @ #Dec. 251 c NEW SOLUTION FOUND: 1915 @ 0.384 @ #Dec. 285 c NEW SOLUTION FOUND: 1911 @ 0.458 @ #Dec. 388 c NEW SOLUTION FOUND: 1906 @ 0.525 @ #Dec. 467 c NEW SOLUTION FOUND: 1883 @ 0.539 @ #Dec. 495 c NEW SOLUTION FOUND: 1879 @ 0.628 @ #Dec. 628 c NEW SOLUTION FOUND: 1858 @ 0.708 @ #Dec. 714 c NEW SOLUTION FOUND: 1854 @ 0.816 @ #Dec. 860 c NEW SOLUTION FOUND: 1849 @ 0.884 @ #Dec. 914 c NEW SOLUTION FOUND: 1839 @ 0.912 @ #Dec. 953 c NEW SOLUTION FOUND: 1837 @ 0.918 @ #Dec. 960 c NEW SOLUTION FOUND: 1816 @ 0.919 @ #Dec. 962 c NEW SOLUTION FOUND: 1812 @ 1.011 @ #Dec. 1081 c NEW SOLUTION FOUND: 1798 @ 1.127 @ #Dec. 1188 c NEW SOLUTION FOUND: 1794 @ 1.257 @ #Dec. 1345 c Restart #1 #Var: 228 #Dec: 1575 LB: 59 @ 1.928 c NEW SOLUTION FOUND: 1789 @ 2.271 @ #Dec. 1794 c Restart #2 #Var: 228 #Dec: 2319 LB: 59 @ 3.001 c NEW SOLUTION FOUND: 1630 @ 4.45 @ #Dec. 2387 c NEW SOLUTION FOUND: 1605 @ 4.45 @ #Dec. 2387 c NEW SOLUTION FOUND: 1566 @ 4.45 @ #Dec. 2388 c NEW SOLUTION FOUND: 1541 @ 4.466 @ #Dec. 2408 c NEW SOLUTION FOUND: 1536 @ 4.489 @ #Dec. 2438 c NEW SOLUTION FOUND: 1518 @ 4.493 @ #Dec. 2443 c NEW SOLUTION FOUND: 1515 @ 4.545 @ #Dec. 2512 c NEW SOLUTION FOUND: 1476 @ 4.546 @ #Dec. 2512 c NEW SOLUTION FOUND: 1458 @ 4.556 @ #Dec. 2526 c Restart #3 #Var: 222 #Dec: 3137 LB: 159 @ 5.406 c Restart #4 #Var: 222 #Dec: 4027 LB: 159 @ 7.277 c NEW SOLUTION FOUND: 1455 @ 9.003 @ #Dec. 5212 c Restart #5 #Var: 222 #Dec: 6347 LB: 159 @ 10.797 c Restart #6 #Var: 222 #Dec: 8107 LB: 159 @ 13.853 c Restart #7 #Var: 222 #Dec: 10035 LB: 159 @ 19.432 c Restart #8 #Var: 222 #Dec: 11923 LB: 159 @ 25.351 c CHANGE to LPR mode... UB: 1455 MIS: 799 LPR: 1191 (0.06125) Diff: 0.67086 c Restart #0 #Var: 222 #Dec: 14179 LB: 159 @ 30.929 c NEW SOLUTION FOUND: 1194 @ 31.085 @ #Dec. 14180 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 -x201 -x202 -x203 -x204 -x205 -x206 -x207 x208 -x209 -x210 -x211 -x212 x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 x237 -x238 -x239 c Cost: 1194 c Exit Code: 30 c Total time: 33.879 s
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/22366/stat): 22366 (bsolo) R 22365 22366 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1840041073 438272 3 4294967295 134512640 134736556 3221224576 3221224576 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/22366/statm): 107 3 90 68 0 39 0 [pid=22366] vsize: 428 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libosl.so open syscall for file tls/i686/libosl.so open syscall for file tls/mmx/libosl.so open syscall for file tls/libosl.so open syscall for file i686/mmx/libosl.so open syscall for file i686/libosl.so open syscall for file mmx/libosl.so open syscall for file libosl.so open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libosl.so open syscall for file /oldhome/oroussel/lib/tls/i686/libosl.so open syscall for file /oldhome/oroussel/lib/tls/mmx/libosl.so open syscall for file /oldhome/oroussel/lib/tls/libosl.so open syscall for file /oldhome/oroussel/lib/i686/mmx/libosl.so open syscall for file /oldhome/oroussel/lib/i686/libosl.so open syscall for file /oldhome/oroussel/lib/mmx/libosl.so open syscall for file /oldhome/oroussel/lib/libosl.so open syscall for file tls/i686/mmx/libstdc++-libc6.2-2.so.3 open syscall for file tls/i686/libstdc++-libc6.2-2.so.3 open syscall for file tls/mmx/libstdc++-libc6.2-2.so.3 open syscall for file tls/libstdc++-libc6.2-2.so.3 open syscall for file i686/mmx/libstdc++-libc6.2-2.so.3 open syscall for file i686/libstdc++-libc6.2-2.so.3 open syscall for file mmx/libstdc++-libc6.2-2.so.3 open syscall for file libstdc++-libc6.2-2.so.3 open syscall for file /oldhome/oroussel/lib/libstdc++-libc6.2-2.so.3 open syscall for file /etc/ld.so.cache open syscall for file /usr/lib/libstdc++-libc6.2-2.so.3 open syscall for file tls/i686/mmx/libm.so.6 open syscall for file tls/i686/libm.so.6 open syscall for file tls/mmx/libm.so.6 open syscall for file tls/libm.so.6 open syscall for file i686/mmx/libm.so.6 open syscall for file i686/libm.so.6 open syscall for file mmx/libm.so.6 open syscall for file libm.so.6 open syscall for file /oldhome/oroussel/lib/libm.so.6 open syscall for file /lib/tls/libm.so.6 open syscall for file tls/i686/mmx/libpthread.so.0 open syscall for file tls/i686/libpthread.so.0 open syscall for file tls/mmx/libpthread.so.0 open syscall for file tls/libpthread.so.0 open syscall for file i686/mmx/libpthread.so.0 open syscall for file i686/libpthread.so.0 open syscall for file mmx/libpthread.so.0 open syscall for file libpthread.so.0 open syscall for file /oldhome/oroussel/lib/libpthread.so.0 open syscall for file /lib/tls/libpthread.so.0 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file tls/i686/mmx/libgcc_s.so.1 open syscall for file tls/i686/libgcc_s.so.1 open syscall for file tls/mmx/libgcc_s.so.1 open syscall for file tls/libgcc_s.so.1 open syscall for file i686/mmx/libgcc_s.so.1 open syscall for file i686/libgcc_s.so.1 open syscall for file mmx/libgcc_s.so.1 open syscall for file libgcc_s.so.1 open syscall for file /oldhome/oroussel/lib/libgcc_s.so.1 open syscall for file /lib/libgcc_s.so.1 open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /etc/localtime open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-c8.opb [startup+10.0037 s] Raw data (loadavg): 0.92 0.95 0.91 2/56 22366 Raw data (/proc/22366/stat): 22366 (bsolo) R 22365 22366 21452 0 -1 0 9940 0 0 0 931 40 0 0 25 0 1 0 1840041073 44584960 9812 4294967295 134512640 134736556 3221224576 3221223100 134634644 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/22366/statm): 10885 9812 1116 68 0 10817 0 [pid=22366] vsize: 43540 Current children cumulated CPU time (s) 9.71 Current children cumulated vsize (Kb) 43540 [startup+20.0044 s] Raw data (loadavg): 0.93 0.96 0.91 2/56 22366 Raw data (/proc/22366/stat): 22366 (bsolo) R 22365 22366 21452 0 -1 0 14909 0 0 0 1893 62 0 0 25 0 1 0 1840041073 65732608 14693 4294967295 134512640 134736556 3221224576 3221223104 134543910 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/22366/statm): 16048 14693 1116 68 0 15980 0 [pid=22366] vsize: 64192 Current children cumulated CPU time (s) 19.55 Current children cumulated vsize (Kb) 64192 [startup+30.0051 s] Raw data (loadavg): 0.94 0.96 0.91 2/56 22366 Raw data (/proc/22366/stat): 22366 (bsolo) R 22365 22366 21452 0 -1 0 20898 0 0 0 2852 87 0 0 25 0 1 0 1840041073 90660864 20454 4294967295 134512640 134736556 3221224576 3221223264 134529155 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/22366/statm): 22134 20454 1116 68 0 22066 0 [pid=22366] vsize: 88536 Current children cumulated CPU time (s) 29.39 Current children cumulated vsize (Kb) 88536 One traced child (pid=22366) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 34.5981 CPU time (s): 33.9268 CPU user time (s): 32.971 CPU system time (s): 0.955854 CPU usage (%): 98.0599 Max. virtual memory (cumulated for all children) (Kb): 88536
Verifier: OK 1194