Name | normalized-opb/submitted/een/normalized-stein45.opb |
MD5SUM | 34647f6a75058de4a92f0ff94f3c9005 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 30 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 45 |
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 | 45 |
Number of bits of the sum of numbers in the objective function | 6 |
Biggest number in a constraint | 22 |
Number of bits of the biggest number in a constraint | 5 |
Biggest sum of numbers in a constraint | 67 |
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 | 1.01484 |
Number of variables | 45 |
Total number of constraints | 331 |
Number of constraints which are clauses | 330 |
Number of constraints which are cardinality constraints (but not clauses) | 1 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 45 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc6 THE 2005-04-14 21:33:50 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=5211 boxname=wulflinc6 idbench=401 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 34647f6a75058de4a92f0ff94f3c9005 /oldhome/oroussel/tmp/wulflinc6/normalized-stein45.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc6/normalized-stein45.opb /oldhome/oroussel/tmp/wulflinc6/normalized-stein45.opb IDLAUNCH: 5211 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 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.042 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: 856848 kB Buffers: 36836 kB Cached: 118552 kB SwapCached: 2644 kB Active: 62076 kB Inactive: 98816 kB HighTotal: 131008 kB HighFree: 8568 kB LowTotal: 903652 kB LowFree: 848280 kB SwapTotal: 2097136 kB SwapFree: 2094492 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6932 kB Slab: 11292 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 21:35:35 (client local time) WITH STATUS 30 IN 104.879 SECONDS stats: 5211 0 104.879 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 331 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................... c ---[ 0]---> Sorter-cost: 718 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 1097 2792 | 329 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 499/499 c -- var.elim.: 273/273 c -- subsuming c -- var.elim.: 204/204 c -- var.elim.: 113/113 c -- var.elim.: 99/99 c -- var.elim.: 100/100 c | 0 | 810 3254 | -- 0 -- -- | -- | -287/463 c | 0 | 810 3254 | 324 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 0.116982 s) c ============================================================================== c [1mFound solution: 35[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 288 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 1528 4950 | 458 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 541/541 c -- var.elim.: 305/305 c -- subsuming c -- var.elim.: 64/64 c -- var.elim.: 10/10 c | 0 | 1437 4873 | -- 0 -- -- | -- | -87/-65 c | 0 | 1437 4873 | 574 0 0 nan | 0.000 % | c | 101 | 1437 4873 | 632 101 789 7.8 | 1.481 % | c ============================================================================== c (current CPU-time: 0.209968 s) c ============================================================================== c [1mFound solution: 33[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 | 109 | 1564 5202 | 469 109 825 7.6 | 1.481 % | c -- subsuming c -- var.elim.: 187/187 c -- var.elim.: 102/102 c | 109 | 1470 5038 | -- 109 -- -- | -- | -81/-69 c | 109 | 1470 5038 | 588 109 825 7.6 | 1.481 % | c ============================================================================== c (current CPU-time: 0.237963 s) c ============================================================================== c [1mFound solution: 32[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 | 109 | 1534 5209 | 460 109 825 7.6 | 1.481 % | c -- subsuming c -- var.elim.: 121/121 c -- var.elim.: 53/53 c | 109 | 1491 5159 | -- 109 -- -- | -- | -43/-49 c | 109 | 1491 5159 | 596 109 825 7.6 | 1.481 % | c ============================================================================== c (current CPU-time: 0.26296 s) c ============================================================================== c [1mFound solution: 31[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 | 113 | 1501 5186 | 450 113 972 8.6 | 1.481 % | c -- subsuming c -- var.elim.: 73/73 c -- var.elim.: 15/15 c | 113 | 1486 5073 | -- 113 -- -- | -- | -3/14 c | 113 | 1486 5073 | 594 113 972 8.6 | 1.481 % | c | 213 | 1486 5073 | 653 213 3717 17.5 | 3.558 % | c | 363 | 1486 5073 | 719 363 7883 21.7 | 3.558 % | c | 588 | 1486 5073 | 791 588 15889 27.0 | 3.558 % | c | 925 | 1486 5073 | 870 925 26810 29.0 | 3.558 % | c ============================================================================== c (current CPU-time: 0.493924 s) c ============================================================================== c [1mFound solution: 30[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 | 1217 | 1577 5290 | 473 908 25914 28.5 | 3.558 % | c -- subsuming c -- var.elim.: 172/172 c -- var.elim.: 89/89 c | 1217 | 1502 5216 | -- 908 -- -- | -- | -75/-73 c | 1217 | 1502 5216 | 600 899 25688 28.6 | 3.558 % | c | 1317 | 1502 5216 | 660 480 10348 21.6 | 5.134 % | c | 1467 | 1502 5216 | 726 630 15012 23.8 | 5.131 % | c | 1692 | 1502 5216 | 799 855 22108 25.9 | 5.131 % | c | 2030 | 1493 5180 | 874 907 23929 26.4 | 5.597 % | c | 2537 | 1493 5180 | 961 786 18687 23.8 | 5.599 % | c | 3296 | 1493 5180 | 1057 796 18509 23.3 | 5.597 % | c | 4435 | 1493 5180 | 1163 1141 28311 24.8 | 5.602 % | c | 6145 | 1493 5180 | 1280 1142 28244 24.7 | 5.602 % | c | 8707 | 1493 5180 | 1408 1346 30576 22.7 | 5.606 % | c | 12552 | 1493 5180 | 1548 1110 21519 19.4 | 5.600 % | c | 18319 | 1493 5180 | 1703 1276 34723 27.2 | 5.604 % | c | 26971 | 1480 5135 | 1857 1922 50815 26.4 | 6.312 % | c | 39946 | 1480 5135 | 2043 1621 41857 25.8 | 6.304 % | c | 59407 | 1466 5092 | 2226 2079 52213 25.1 | 7.000 % | c | 88599 | 1439 4872 | 2404 2065 56938 27.6 | 8.178 % | c | 132389 | 1379 4544 | 2534 1982 56562 28.5 | 10.257 % | c | 198073 | 1337 4251 | 2703 2123 48288 22.7 | 13.301 % | c | 296599 | 1265 3997 | 2813 2137 51097 23.9 | 16.094 % | c ============================================================================== c [1mOptimal solution: 30[0m s OPTIMUM FOUND v x0 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 c _______________________________________________________________________________ c c restarts : 29 c conflicts : 383854 (3661 /sec) c decisions : 441586 (4211 /sec) c propagations : 27638388 (263574 /sec) c inspects : 251921872 (2402458 /sec) c CPU time : 104.86 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.91 0.95 0.90 2/54 7704 Raw data (stat): 7704 (runsolver) R 7703 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429643771 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+10.0009 s] Raw data (loadavg): 0.92 0.95 0.91 2/54 7704 Raw data (stat): 7704 (minisat+) R 7703 29653 29652 0 -1 0 555 0 0 0 998 1 0 0 25 0 1 0 429643771 3735552 533 4294967295 134512640 134672761 3221224576 3221223760 134615643 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 912 533 603 41 0 871 0 vsize: 3648 [startup+20.0017 s] Raw data (loadavg): 0.93 0.95 0.91 2/54 7704 Raw data (stat): 7704 (minisat+) R 7703 29653 29652 0 -1 0 578 0 0 0 1998 1 0 0 25 0 1 0 429643771 3858432 556 4294967295 134512640 134672761 3221224576 3221223760 134615681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 942 556 603 41 0 901 0 vsize: 3768 [startup+30.0022 s] Raw data (loadavg): 0.94 0.95 0.91 2/54 7704 Raw data (stat): 7704 (minisat+) R 7703 29653 29652 0 -1 0 606 0 0 0 2998 1 0 0 25 0 1 0 429643771 3989504 584 4294967295 134512640 134672761 3221224576 3221223616 134612644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 974 584 603 41 0 933 0 vsize: 3896 [startup+40.0023 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 7704 Raw data (stat): 7704 (minisat+) R 7703 29653 29652 0 -1 0 620 0 0 0 3998 1 0 0 25 0 1 0 429643771 3989504 598 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 974 598 603 41 0 933 0 vsize: 3896 [startup+50.0031 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 7704 Raw data (stat): 7704 (minisat+) R 7703 29653 29652 0 -1 0 621 0 0 0 4999 1 0 0 25 0 1 0 429643771 3989504 599 4294967295 134512640 134672761 3221224576 3221223536 134645408 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 974 599 603 41 0 933 0 vsize: 3896 [startup+60.0036 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 7704 Raw data (stat): 7704 (minisat+) R 7703 29653 29652 0 -1 0 643 0 0 0 5999 1 0 0 25 0 1 0 429643771 4108288 621 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1003 621 603 41 0 962 0 vsize: 4012 [startup+70.0037 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 7704 Raw data (stat): 7704 (minisat+) R 7703 29653 29652 0 -1 0 643 0 0 0 7000 1 0 0 25 0 1 0 429643771 4108288 621 4294967295 134512640 134672761 3221224576 3221223760 134615686 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1003 621 603 41 0 962 0 vsize: 4012 [startup+80.0046 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 7704 Raw data (stat): 7704 (minisat+) R 7703 29653 29652 0 -1 0 646 0 0 0 8000 1 0 0 25 0 1 0 429643771 4108288 624 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1003 624 603 41 0 962 0 vsize: 4012 [startup+90.005 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 7704 Raw data (stat): 7704 (minisat+) R 7703 29653 29652 0 -1 0 655 0 0 0 9000 1 0 0 25 0 1 0 429643771 4108288 633 4294967295 134512640 134672761 3221224576 3221223760 134615785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1003 633 603 41 0 962 0 vsize: 4012 [startup+100.005 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 7704 Raw data (stat): 7704 (minisat+) R 7703 29653 29652 0 -1 0 655 0 0 0 10001 1 0 0 25 0 1 0 429643771 4108288 633 4294967295 134512640 134672761 3221224576 3221222800 134645608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1003 633 603 41 0 962 0 vsize: 4012 [startup+104.859 s] Raw data (loadavg): 0.98 0.96 0.91 1/53 7704 Raw data (stat): 7704 (minisat+) R 7703 29653 29652 0 -1 0 655 0 0 0 10001 1 0 0 25 0 1 0 429643771 4108288 633 4294967295 134512640 134672761 3221224576 3221222800 134645608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1003 633 603 41 0 962 0 vsize: 0 Child status: 30 Real time (s): 104.859 CPU time (s): 104.879 CPU user time (s): 104.861 CPU system time (s): 0.017997 CPU usage (%): 100.019 Max. virtual memory (Kb): 4012 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 30 #### END VERIFIER DATA ####