Name | normalized-opb/submitted/sorensson/garden/normalized-g9x9.opb |
MD5SUM | 3682f861aa46be9df7d6903cb35a0651 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 20 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 81 |
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 | 81 |
Number of bits of the sum of numbers in the objective function | 7 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 81 |
Number of bits of the biggest sum of numbers | 7 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.676896 |
Number of variables | 81 |
Total number of constraints | 81 |
Number of constraints which are clauses | 81 |
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 | 3 |
Maximum length of a constraint | 5 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc11 THE 2005-04-14 05:33:17 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4979 boxname=wulflinc11 idbench=383 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3682f861aa46be9df7d6903cb35a0651 /oldhome/oroussel/tmp/wulflinc11/normalized-g9x9.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc11/normalized-g9x9.opb /oldhome/oroussel/tmp/wulflinc11/normalized-g9x9.opb IDLAUNCH: 4979 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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.028 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: 891940 kB Buffers: 36392 kB Cached: 81960 kB SwapCached: 4932 kB Active: 60072 kB Inactive: 66008 kB HighTotal: 131008 kB HighFree: 45332 kB LowTotal: 903652 kB LowFree: 846608 kB SwapTotal: 2097136 kB SwapFree: 2092204 kB Dirty: 52 kB Writeback: 0 kB Mapped: 6924 kB Slab: 11032 kB Committed_AS: 63488 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 05:33:25 (client local time) WITH STATUS 30 IN 7.74782 SECONDS stats: 4979 0 7.74782 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 81 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 | 81 369 | 27 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 27[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1728 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 3862 9246 | 1287 0 0 nan | 0.000 % | c | 101 | 3837 9189 | 1415 100 769 7.7 | 0.983 % | c | 251 | 3808 9126 | 1557 246 2083 8.5 | 1.584 % | c ============================================================================== c [1mFound solution: 26[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 | 279 | 3855 9244 | 1285 274 2289 8.4 | 1.584 % | c ============================================================================== c [1mFound solution: 25[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 | 371 | 3805 9126 | 1268 366 4224 11.5 | 1.584 % | c | 471 | 3805 9126 | 1394 466 5103 11.0 | 2.977 % | c ============================================================================== c [1mFound solution: 24[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 | 499 | 3818 9163 | 1272 491 5338 10.9 | 2.977 % | c ============================================================================== c [1mFound solution: 23[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 | 505 | 3790 9093 | 1263 454 4049 8.9 | 2.977 % | c | 605 | 3790 9093 | 1389 554 5153 9.3 | 4.275 % | c | 757 | 3790 9093 | 1528 706 6991 9.9 | 4.275 % | c ============================================================================== c [1mFound solution: 22[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 | 811 | 3827 9186 | 1275 760 7799 10.3 | 4.275 % | c | 913 | 3827 9186 | 1402 862 9454 11.0 | 4.380 % | c | 1064 | 3827 9186 | 1542 1013 12224 12.1 | 4.380 % | c | 1289 | 3763 9042 | 1697 1228 14513 11.8 | 5.840 % | c | 1628 | 3738 8986 | 1866 1564 19588 12.5 | 6.351 % | c ============================================================================== c [1mFound solution: 21[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 | 1732 | 3689 8866 | 1229 1623 19442 12.0 | 6.351 % | c | 1833 | 3668 8818 | 1351 897 8832 9.8 | 8.164 % | c | 1983 | 3668 8818 | 1487 1047 11190 10.7 | 8.164 % | c | 2209 | 3668 8818 | 1635 1273 15409 12.1 | 8.164 % | c | 2546 | 3559 8567 | 1799 1534 20254 13.2 | 10.569 % | c | 3052 | 3559 8567 | 1979 2040 30150 14.8 | 10.569 % | c | 3812 | 3559 8567 | 2177 1621 23367 14.4 | 10.569 % | c | 4952 | 3559 8567 | 2394 1523 18798 12.3 | 10.569 % | c ============================================================================== c [1mFound solution: 20[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 | 5072 | 3581 8621 | 1193 1643 20552 12.5 | 10.569 % | c | 5172 | 3581 8621 | 1312 922 8976 9.7 | 10.710 % | c | 5323 | 3556 8564 | 1443 1072 11335 10.6 | 11.144 % | c | 5551 | 3556 8564 | 1587 1300 14694 11.3 | 11.144 % | c | 5888 | 3556 8564 | 1746 1637 20236 12.4 | 11.144 % | c | 6398 | 3556 8564 | 1921 1115 11236 10.1 | 11.144 % | c | 7159 | 3556 8564 | 2113 1876 22435 12.0 | 11.144 % | c | 8299 | 3556 8564 | 2324 1675 18667 11.1 | 11.144 % | c | 10007 | 3556 8564 | 2557 2037 23001 11.3 | 11.144 % | c | 12569 | 3556 8564 | 2813 1624 15510 9.6 | 11.146 % | c | 16416 | 3457 8339 | 3094 2329 22394 9.6 | 13.244 % | c | 22182 | 3453 8330 | 3403 2962 32276 10.9 | 13.315 % | c ============================================================================== c [1mOptimal solution: 20[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 c _______________________________________________________________________________ c c restarts : 36 c conflicts : 23981 (3102 /sec) c decisions : 33050 (4276 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 7.72982 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.92 0.95 0.94 2/54 7967 Raw data (stat): 7967 (runsolver) R 7966 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423878069 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+7.76343 s] Raw data (loadavg): 0.93 0.95 0.94 1/53 7967 Raw data (stat): 7967 (runsolver) R 7966 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423878069 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): 7.76313 CPU time (s): 7.74782 CPU user time (s): 7.73082 CPU system time (s): 0.016997 CPU usage (%): 99.8028 Max. virtual memory (Kb): 1028 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 20 #### END VERIFIER DATA ####