Name | submitted/manquinho/logic-synthesis/normalized-test4.pi.opb |
MD5SUM | 09c7b63b87fdc5a38ccb26d9b87fe2d9 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 137 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 6140 |
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 | 6140 |
Number of bits of the sum of numbers in the objective function | 13 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 6140 |
Number of bits of the biggest sum of numbers | 13 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.95 |
Number of variables | 6139 |
Total number of constraints | 1437 |
Number of constraints which are clauses | 1437 |
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 | 5 |
Maximum length of a constraint | 172 |
LAUNCH ON wulflinc4 THE 2005-09-23 14:20:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8275 boxname=wulflinc4 idbench=71 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 09c7b63b87fdc5a38ccb26d9b87fe2d9 /oldhome/oroussel/tmp/wulflinc4/normalized-test4.pi.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc4/normalized-test4.pi.opb IDLAUNCH: 8275 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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 : 2 cpu MHz : 451.191 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: 936672 kB Buffers: 11392 kB Cached: 69528 kB SwapCached: 0 kB Active: 44824 kB Inactive: 38952 kB HighTotal: 131008 kB HighFree: 57204 kB LowTotal: 903652 kB LowFree: 879468 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6976 kB Slab: 8668 kB Committed_AS: 63656 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-23 14:22:45 (client local time) WITH STATUS 1 IN 112.857 SECONDS stats: 8275 7 112.857 1
c This solver internally uses Chaff 2004.11.15 Simplified c running zchaff... c got solution with objective value: 6140 c big objective detected c trying from 0 to 511 Unexpected exception : St9bad_alloc
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/6833/stat): 6833 (pb2sat) R 6832 6833 4060 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 20880616 1527808 2 4294967295 134512640 135987407 3221224576 3221224576 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/6833/statm): 373 2 364 364 0 9 0 [pid=6833] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-test4.pi.opb [startup+10.0019 s] Raw data (loadavg): 0.93 0.98 0.99 2/55 6833 Raw data (/proc/6833/stat): 6833 (pb2sat) R 6832 6833 4060 0 -1 0 26359 0 0 0 933 62 0 0 25 0 1 0 20880616 84963328 15291 4294967295 134512640 135987407 3221224576 3220744800 134537491 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6833/statm): 20743 15291 364 364 0 20379 0 [pid=6833] vsize: 82972 Current children cumulated CPU time (s) 9.95 Current children cumulated vsize (Kb) 82972 [startup+20.0028 s] Raw data (loadavg): 0.94 0.98 0.99 2/55 6833 Raw data (/proc/6833/stat): 6833 (pb2sat) R 6832 6833 4060 0 -1 0 56898 0 0 0 1860 133 0 0 25 0 1 0 20880616 187826176 34620 4294967295 134512640 135987407 3221224576 3219896028 134637035 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6833/statm): 45856 34620 364 364 0 45492 0 [pid=6833] vsize: 183424 Current children cumulated CPU time (s) 19.93 Current children cumulated vsize (Kb) 183424 [startup+30.0026 s] Raw data (loadavg): 0.95 0.98 0.99 2/55 6833 Raw data (/proc/6833/stat): 6833 (pb2sat) R 6832 6833 4060 0 -1 0 96215 0 0 0 2775 215 0 0 25 0 1 0 20880616 371388416 64025 4294967295 134512640 135987407 3221224576 3220536192 134887487 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6833/statm): 90671 64025 364 364 0 90307 0 [pid=6833] vsize: 362684 Current children cumulated CPU time (s) 29.9 Current children cumulated vsize (Kb) 362684 [startup+40.0035 s] Raw data (loadavg): 0.96 0.98 0.99 2/55 6833 Raw data (/proc/6833/stat): 6833 (pb2sat) R 6832 6833 4060 0 -1 0 117653 0 0 0 3723 265 0 0 25 0 1 0 20880616 377044992 72965 4294967295 134512640 135987407 3221224576 3219719292 134636992 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6833/statm): 92052 72965 364 364 0 91688 0 [pid=6833] vsize: 368208 Current children cumulated CPU time (s) 39.88 Current children cumulated vsize (Kb) 368208 [startup+50.0043 s] Raw data (loadavg): 0.96 0.98 0.99 2/55 6833 Raw data (/proc/6833/stat): 6833 (pb2sat) R 6832 6833 4060 0 -1 0 136452 0 0 0 4679 308 0 0 25 0 1 0 20880616 401240064 91539 4294967295 134512640 135987407 3221224576 3221014080 134854943 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6833/statm): 97959 91539 364 364 0 97595 0 [pid=6833] vsize: 391836 Current children cumulated CPU time (s) 49.87 Current children cumulated vsize (Kb) 391836 [startup+60.0052 s] Raw data (loadavg): 0.97 0.98 0.99 2/55 6833 Raw data (/proc/6833/stat): 6833 (pb2sat) R 6832 6833 4060 0 -1 0 202537 0 0 0 5539 444 0 0 25 0 1 0 20880616 641064960 113474 4294967295 134512640 135987407 3221224576 3219420960 134537491 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6833/statm): 156510 113474 364 364 0 156146 0 [pid=6833] vsize: 626040 Current children cumulated CPU time (s) 59.83 Current children cumulated vsize (Kb) 626040 [startup+70.0061 s] Raw data (loadavg): 0.97 0.98 0.99 2/55 6833 Raw data (/proc/6833/stat): 6833 (pb2sat) R 6832 6833 4060 0 -1 0 218559 0 0 0 6500 481 0 0 25 0 1 0 20880616 695300096 129304 4294967295 134512640 135987407 3221224576 3219734588 135499903 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6833/statm): 169751 129304 364 364 0 169387 0 [pid=6833] vsize: 679004 Current children cumulated CPU time (s) 69.81 Current children cumulated vsize (Kb) 679004 [startup+80.0069 s] Raw data (loadavg): 0.98 0.98 0.99 2/55 6833 Raw data (/proc/6833/stat): 6833 (pb2sat) R 6832 6833 4060 0 -1 0 236933 0 0 0 7461 518 0 0 25 0 1 0 20880616 718954496 147458 4294967295 134512640 135987407 3221224576 3221000492 134669203 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6833/statm): 175526 147458 364 364 0 175162 0 [pid=6833] vsize: 702104 Current children cumulated CPU time (s) 79.79 Current children cumulated vsize (Kb) 702104 [startup+90.0078 s] Raw data (loadavg): 0.98 0.98 0.99 2/55 6833 Raw data (/proc/6833/stat): 6833 (pb2sat) R 6832 6833 4060 0 -1 0 255037 0 0 0 8423 553 0 0 25 0 1 0 20880616 742338560 165344 4294967295 134512640 135987407 3221224576 3221215868 135480732 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6833/statm): 181235 165344 364 364 0 180871 0 [pid=6833] vsize: 724940 Current children cumulated CPU time (s) 89.76 Current children cumulated vsize (Kb) 724940 [startup+100.008 s] Raw data (loadavg): 0.98 0.98 0.99 2/55 6833 Raw data (/proc/6833/stat): 6833 (pb2sat) R 6832 6833 4060 0 -1 0 269502 0 0 0 9394 582 0 0 25 0 1 0 20880616 811458560 179635 4294967295 134512640 135987407 3221224576 3219869568 134558532 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6833/statm): 198110 179635 364 364 0 197746 0 [pid=6833] vsize: 792440 Current children cumulated CPU time (s) 99.76 Current children cumulated vsize (Kb) 792440 [startup+110.008 s] Raw data (loadavg): 0.98 0.98 0.99 2/55 6833 Raw data (/proc/6833/stat): 6833 (pb2sat) R 6832 6833 4060 0 -1 0 284099 0 0 0 10362 612 0 0 25 0 1 0 20880616 831160320 194032 4294967295 134512640 135987407 3221224576 3221222884 134893008 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6833/statm): 202920 194032 364 364 0 202556 0 [pid=6833] vsize: 811680 Current children cumulated CPU time (s) 109.74 Current children cumulated vsize (Kb) 811680 One traced child (pid=6833) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 113.118 CPU time (s): 112.857 CPU user time (s): 106.333 CPU system time (s): 6.52401 CPU usage (%): 99.7692 Max. virtual memory (cumulated for all children) (Kb): 811680
ERROR: no interpretation found !