Name | normalized-opb/mps-v2-13-7/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-13-7-maros.opb |
MD5SUM | 1ae5b04b2d0e1f5ab82e29e98b8350c0 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 43097 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 64 |
Biggest coefficient in the objective function | 4718592 |
Number of bits for the biggest coefficient in the objective function | 23 |
Sum of the numbers in the objective function | 14745570 |
Number of bits of the sum of numbers in the objective function | 24 |
Biggest number in a constraint | 4718592 |
Number of bits of the biggest number in a constraint | 23 |
Biggest sum of numbers in a constraint | 14745570 |
Number of bits of the biggest sum of numbers | 24 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02384 |
Number of variables | 64 |
Total number of constraints | 6 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 12 |
Maximum length of a constraint | 64 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc27 THE 2005-04-20 23:10:17 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=20383 boxname=wulflinc27 idbench=1568 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1ae5b04b2d0e1f5ab82e29e98b8350c0 /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-maros.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-maros.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-maros.opb IDLAUNCH: 20383 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 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.169 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: 776720 kB Buffers: 33632 kB Cached: 191924 kB SwapCached: 136 kB Active: 106888 kB Inactive: 121100 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 776468 kB SwapTotal: 2097892 kB SwapFree: 2097324 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6220 kB Slab: 24300 kB Committed_AS: 63488 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-20 23:10:34 (client local time) WITH STATUS 30 IN 16.5525 SECONDS stats: 20383 0 16.5525 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 6 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: # c -- Clauses(.)/Splits(s): s c ---[ 5]---> BDD-cost: 11 c ---[ 3]---> BDD-cost: 1360 c ---[ 2]---> BDD-cost: 276 c ---[ 1]---> BDD-cost: 265 c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 4739 13501 | 1579 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 48652[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1011 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2 | 7087 18983 | 2362 2 24 12.0 | 0.000 % | c ============================================================================== c [1mFound solution: 48516[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 80 | 7113 19067 | 2371 80 1209 15.1 | 0.000 % | c ============================================================================== c [1mFound solution: 48481[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 102 | 7124 19098 | 2374 102 1410 13.8 | 0.000 % | c ============================================================================== c [1mFound solution: 48089[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 109 | 7135 19129 | 2378 109 1454 13.3 | 0.000 % | c ============================================================================== c [1mFound solution: 46048[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 204 | 7145 19158 | 2381 204 2340 11.5 | 0.000 % | c | 306 | 7145 19158 | 2619 306 3181 10.4 | 0.905 % | c | 458 | 7145 19158 | 2881 458 4399 9.6 | 0.905 % | c ============================================================================== c [1mFound solution: 45282[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 501 | 7156 19188 | 2385 501 5114 10.2 | 0.905 % | c ============================================================================== c [1mFound solution: 44658[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 572 | 7171 19229 | 2390 572 6065 10.6 | 0.905 % | c | 672 | 7171 19229 | 2629 672 7614 11.3 | 0.973 % | c | 822 | 7171 19229 | 2891 822 10008 12.2 | 0.973 % | c | 1048 | 7171 19229 | 3181 1048 12326 11.8 | 0.973 % | c | 1385 | 7171 19229 | 3499 1385 17396 12.6 | 0.973 % | c | 1891 | 7171 19229 | 3849 1891 21578 11.4 | 0.973 % | c | 2652 | 7171 19229 | 4234 2652 33079 12.5 | 0.973 % | c ============================================================================== c [1mFound solution: 44002[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2896 | 7178 19248 | 2392 2896 37410 12.9 | 0.973 % | c ============================================================================== c [1mFound solution: 43997[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2927 | 7187 19276 | 2395 1479 19308 13.1 | 0.973 % | c ============================================================================== c [1mFound solution: 43755[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2995 | 7199 19305 | 2399 1547 20198 13.1 | 0.973 % | c | 3096 | 7199 19305 | 2638 1648 21917 13.3 | 1.075 % | c | 3248 | 7199 19305 | 2902 1800 23874 13.3 | 1.075 % | c | 3473 | 7199 19305 | 3193 2025 27924 13.8 | 1.075 % | c | 3810 | 7199 19305 | 3512 2362 35825 15.2 | 1.075 % | c ============================================================================== c [1mFound solution: 43488[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4302 | 7207 19331 | 2402 2854 51462 18.0 | 1.075 % | c | 4403 | 7207 19331 | 2642 1528 28263 18.5 | 1.108 % | c | 4557 | 7207 19331 | 2906 1682 30104 17.9 | 1.109 % | c ============================================================================== c [1mFound solution: 43394[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4679 | 7219 19361 | 2406 1804 32233 17.9 | 1.109 % | c | 4780 | 7219 19361 | 2646 1905 33385 17.5 | 1.142 % | c | 4930 | 7208 19334 | 2911 2054 36158 17.6 | 1.177 % | c | 5155 | 7208 19334 | 3202 2279 39364 17.3 | 1.177 % | c | 5494 | 7208 19334 | 3522 2618 43872 16.8 | 1.177 % | c ============================================================================== c [1mFound solution: 43374[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5525 | 7223 19371 | 2407 2649 44649 16.9 | 1.177 % | c | 5626 | 7223 19371 | 2647 1426 16454 11.5 | 1.209 % | c | 5776 | 7223 19371 | 2912 1576 18316 11.6 | 1.209 % | c | 6001 | 7223 19371 | 3203 1801 21924 12.2 | 1.209 % | c | 6340 | 7223 19371 | 3524 2140 29444 13.8 | 1.209 % | c | 6849 | 7223 19371 | 3876 2649 36814 13.9 | 1.209 % | c | 7610 | 7223 19371 | 4264 3410 48648 14.3 | 1.209 % | c | 8749 | 7223 19371 | 4690 4549 69705 15.3 | 1.209 % | c ============================================================================== c [1mFound solution: 43371[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9180 | 7234 19398 | 2411 4980 77272 15.5 | 1.209 % | c | 9281 | 7234 19398 | 2652 1346 16381 12.2 | 1.242 % | c | 9432 | 7234 19398 | 2917 1497 18073 12.1 | 1.242 % | c | 9657 | 7234 19398 | 3209 1722 20910 12.1 | 1.242 % | c | 9995 | 7234 19398 | 3529 2060 27102 13.2 | 1.242 % | c ============================================================================== c [1mFound solution: 43360[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10393 | 7244 19427 | 2414 2458 34283 13.9 | 1.242 % | c ============================================================================== c [1mFound solution: 43359[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10423 | 7254 19455 | 2418 1259 13513 10.7 | 1.242 % | c ============================================================================== c [1mFound solution: 43358[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10450 | 7264 19482 | 2421 1286 13883 10.8 | 1.242 % | c | 10551 | 7264 19482 | 2663 1387 16613 12.0 | 1.338 % | c | 10701 | 7264 19482 | 2929 1537 19922 13.0 | 1.338 % | c | 10927 | 7264 19482 | 3222 1763 24655 14.0 | 1.338 % | c | 11264 | 7264 19482 | 3544 2100 29806 14.2 | 1.338 % | c ============================================================================== c [1mFound solution: 43357[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11614 | 7274 19510 | 2424 2450 36059 14.7 | 1.338 % | c | 11714 | 7274 19510 | 2666 2550 38775 15.2 | 1.370 % | c | 11864 | 7274 19510 | 2933 2700 42047 15.6 | 1.370 % | c | 12089 | 7274 19510 | 3226 2925 45109 15.4 | 1.370 % | c | 12427 | 7274 19510 | 3548 3263 50275 15.4 | 1.370 % | c | 12934 | 7274 19510 | 3903 3770 58952 15.6 | 1.370 % | c ============================================================================== c [1mFound solution: 43234[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13012 | 7281 19527 | 2427 3848 60507 15.7 | 1.370 % | c | 13112 | 7281 19527 | 2669 2024 24987 12.3 | 1.403 % | c | 13262 | 7281 19527 | 2936 2174 27019 12.4 | 1.403 % | c | 13488 | 7281 19527 | 3230 2400 30717 12.8 | 1.403 % | c | 13827 | 7281 19527 | 3553 2739 36064 13.2 | 1.403 % | c ============================================================================== c [1mFound solution: 43231[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13936 | 7289 19547 | 2429 2848 38080 13.4 | 1.403 % | c | 14036 | 7289 19547 | 2671 1524 17081 11.2 | 1.436 % | c | 14186 | 7289 19547 | 2939 1674 19710 11.8 | 1.436 % | c | 14411 | 7289 19547 | 3232 1899 24532 12.9 | 1.436 % | c | 14748 | 7289 19547 | 3556 2236 28811 12.9 | 1.436 % | c ============================================================================== c [1mFound solution: 43230[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14960 | 7297 19567 | 2432 2448 31800 13.0 | 1.436 % | c | 15060 | 7297 19567 | 2675 2548 34437 13.5 | 1.468 % | c | 15210 | 7297 19567 | 2942 2698 37340 13.8 | 1.468 % | c | 15435 | 7297 19567 | 3236 2923 41220 14.1 | 1.468 % | c | 15773 | 7297 19567 | 3560 3261 46459 14.2 | 1.468 % | c ============================================================================== c [1mFound solution: 43229[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16018 | 7305 19587 | 2435 3506 50837 14.5 | 1.468 % | c | 16119 | 7305 19587 | 2678 1854 21977 11.9 | 1.501 % | c | 16269 | 7305 19587 | 2946 2004 24281 12.1 | 1.501 % | c ============================================================================== c [1mFound solution: 43226[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16370 | 7316 19617 | 2438 2105 26006 12.4 | 1.501 % | c ============================================================================== c [1mFound solution: 43225[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16379 | 7324 19640 | 2441 2114 26076 12.3 | 1.501 % | c ============================================================================== c [1mFound solution: 43217[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16387 | 7335 19669 | 2445 2122 26193 12.3 | 1.501 % | c | 16489 | 7335 19669 | 2689 2224 28251 12.7 | 1.595 % | c | 16639 | 7335 19669 | 2958 2374 30696 12.9 | 1.595 % | c | 16865 | 7335 19669 | 3254 2600 34254 13.2 | 1.595 % | c | 17202 | 7335 19669 | 3579 2937 39796 13.5 | 1.595 % | c | 17708 | 7335 19669 | 3937 3443 52216 15.2 | 1.595 % | c | 18469 | 7335 19669 | 4331 2117 26496 12.5 | 1.594 % | c | 19608 | 7335 19669 | 4764 3256 46885 14.4 | 1.595 % | c ============================================================================== c [1mFound solution: 43216[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20589 | 7346 19699 | 2448 4237 65453 15.4 | 1.595 % | c ============================================================================== c [1mFound solution: 43211[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20609 | 7356 19725 | 2452 2139 25601 12.0 | 1.595 % | c ============================================================================== c [1mFound solution: 43206[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20649 | 7367 19753 | 2455 2179 26115 12.0 | 1.595 % | c | 20752 | 7367 19753 | 2700 2282 28765 12.6 | 1.688 % | c ============================================================================== c [1mFound solution: 43181[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20811 | 7379 19783 | 2459 2341 29625 12.7 | 1.688 % | c ============================================================================== c [1mFound solution: 43177[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20813 | 7390 19810 | 2463 2343 29653 12.7 | 1.688 % | c | 20913 | 7390 19810 | 2709 2443 31241 12.8 | 1.748 % | c ============================================================================== c [1mFound solution: 43165[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21045 | 7401 19838 | 2467 2575 33733 13.1 | 1.748 % | c ============================================================================== c [1mFound solution: 43164[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21119 | 7412 19866 | 2470 1362 12656 9.3 | 1.748 % | c ============================================================================== c [1mFound solution: 43161[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21128 | 7423 19894 | 2474 1371 12784 9.3 | 1.748 % | c | 21228 | 7423 19894 | 2721 1471 14477 9.8 | 1.838 % | c | 21378 | 7423 19894 | 2993 1621 16555 10.2 | 1.838 % | c | 21603 | 7423 19894 | 3292 1846 19792 10.7 | 1.838 % | c | 21940 | 7423 19894 | 3622 2183 25509 11.7 | 1.838 % | c | 22446 | 7423 19894 | 3984 2689 33546 12.5 | 1.838 % | c | 23205 | 7423 19894 | 4382 3448 49454 14.3 | 1.838 % | c ============================================================================== c [1mFound solution: 43160[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23832 | 7437 19929 | 2479 4075 63017 15.5 | 1.838 % | c ============================================================================== c [1mFound solution: 43157[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23875 | 7450 19961 | 2483 2081 28131 13.5 | 1.838 % | c | 23975 | 7450 19961 | 2731 2181 29632 13.6 | 1.895 % | c | 24126 | 7450 19961 | 3004 2332 32042 13.7 | 1.895 % | c | 24352 | 7450 19961 | 3304 2558 36970 14.5 | 1.895 % | c | 24693 | 7450 19961 | 3635 2899 43998 15.2 | 1.895 % | c ============================================================================== c [1mFound solution: 43155[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24849 | 7461 19988 | 2487 3055 46679 15.3 | 1.895 % | c | 24952 | 7461 19988 | 2735 1631 18429 11.3 | 1.925 % | c | 25102 | 7461 19988 | 3009 1781 21196 11.9 | 1.925 % | c ============================================================================== c [1mFound solution: 43150[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25305 | 7474 20019 | 2491 1984 24747 12.5 | 1.925 % | c ============================================================================== c [1mFound solution: 43139[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25327 | 7484 20043 | 2494 2006 25047 12.5 | 1.925 % | c ============================================================================== c [1mFound solution: 43131[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25337 | 7496 20072 | 2498 2016 25162 12.5 | 1.925 % | c | 25437 | 7496 20072 | 2747 2116 27422 13.0 | 2.012 % | c | 25587 | 7496 20072 | 3022 2266 29710 13.1 | 2.011 % | c | 25813 | 7496 20072 | 3324 2492 33720 13.5 | 2.012 % | c ============================================================================== c [1mFound solution: 43130[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25892 | 7508 20101 | 2502 2571 35018 13.6 | 2.012 % | c | 25992 | 7508 20101 | 2752 1386 12756 9.2 | 2.040 % | c | 26143 | 7508 20101 | 3027 1537 15719 10.2 | 2.040 % | c | 26371 | 7508 20101 | 3330 1765 19859 11.3 | 2.040 % | c | 26708 | 7508 20101 | 3663 2102 26194 12.5 | 2.040 % | c ============================================================================== c [1mFound solution: 43129[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26938 | 7520 20130 | 2506 2332 30243 13.0 | 2.040 % | c ============================================================================== c [1mFound solution: 43127[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26961 | 7534 20163 | 2511 2355 30584 13.0 | 2.040 % | c | 27061 | 7534 20163 | 2762 2455 32777 13.4 | 2.097 % | c ============================================================================== c [1mFound solution: 43121[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27148 | 7545 20189 | 2515 2542 34760 13.7 | 2.097 % | c ============================================================================== c [1mFound solution: 43117[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27204 | 7555 20213 | 2518 2598 35935 13.8 | 2.097 % | c | 27306 | 7555 20213 | 2769 1401 14405 10.3 | 2.156 % | c | 27457 | 7555 20213 | 3046 1552 17100 11.0 | 2.155 % | c | 27682 | 7555 20213 | 3351 1777 21845 12.3 | 2.155 % | c ============================================================================== c [1mFound solution: 43113[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27899 | 7565 20237 | 2521 1994 25715 12.9 | 2.155 % | c | 27999 | 7565 20237 | 2773 2094 27976 13.4 | 2.183 % | c | 28149 | 7565 20237 | 3050 2244 30570 13.6 | 2.183 % | c | 28374 | 7565 20237 | 3355 2469 33987 13.8 | 2.183 % | c | 28712 | 7565 20237 | 3690 2807 39183 14.0 | 2.184 % | c | 29218 | 7565 20237 | 4060 3313 48987 14.8 | 2.183 % | c | 29977 | 7565 20237 | 4466 4072 62540 15.4 | 2.183 % | c | 31118 | 7565 20237 | 4912 2737 41176 15.0 | 2.184 % | c ============================================================================== c [1mFound solution: 43106[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31600 | 7574 20260 | 2524 3219 49915 15.5 | 2.184 % | c | 31700 | 7574 20260 | 2776 1710 17826 10.4 | 2.213 % | c ============================================================================== c [1mFound solution: 43105[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31807 | 7581 20277 | 2527 1817 19757 10.9 | 2.213 % | c | 31911 | 7581 20277 | 2779 1921 21581 11.2 | 2.243 % | c ============================================================================== c [1mFound solution: 43102[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31972 | 7588 20294 | 2529 1982 22241 11.2 | 2.243 % | c | 32073 | 7588 20294 | 2781 2083 24222 11.6 | 2.273 % | c ============================================================================== c [1mFound solution: 43100[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32138 | 7597 20316 | 2532 2148 25277 11.8 | 2.273 % | c | 32238 | 7597 20316 | 2785 2248 26982 12.0 | 2.302 % | c ============================================================================== c [1mFound solution: 43099[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32321 | 7606 20339 | 2535 2331 28192 12.1 | 2.302 % | c | 32422 | 7606 20339 | 2788 2432 30125 12.4 | 2.331 % | c | 32572 | 7606 20339 | 3067 2582 32490 12.6 | 2.331 % | c | 32799 | 7606 20339 | 3374 2809 35471 12.6 | 2.331 % | c ============================================================================== c [1mFound solution: 43097[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32993 | 7615 20361 | 2538 3003 38515 12.8 | 2.331 % | c | 33093 | 7615 20361 | 2791 1602 15367 9.6 | 2.360 % | c | 33244 | 7615 20361 | 3070 1753 18473 10.5 | 2.360 % | c | 33470 | 7615 20361 | 3378 1979 23281 11.8 | 2.360 % | c | 33808 | 7615 20361 | 3715 2317 27311 11.8 | 2.360 % | c | 34315 | 7615 20361 | 4087 2824 37272 13.2 | 2.360 % | c | 35074 | 7615 20361 | 4496 3583 48437 13.5 | 2.360 % | c | 36213 | 7503 20097 | 4945 2642 26301 10.0 | 3.278 % | c ============================================================================== c [1mOptimal solution: 43097[0m s OPTIMUM FOUND v -VOL1_bit_7 -VOL1_bit_6 VOL1_bit_5 VOL1_bit_4 -VOL1_bit_3 VOL1_bit_2 -VOL1_bit_1 VOL1_bit0 VOL1_bit1 -VOL1_bit2 -VOL1_bit3 -VOL1_bit4 -VOL1_bit5 -VOL1_bit6 -VOL1_bit7 -VOL1_bit8 -VOL1_bit9 -VOL1_bit10 -VOL1_bit11 -VOL1_bit12 VOL2_bit_7 -VOL2_bit_6 -VOL2_bit_5 VOL2_bit_4 -VOL2_bit_3 VOL2_bit_2 -VOL2_bit_1 VOL2_bit0 -VOL2_bit1 VOL2_bit2 VOL2_bit3 -VOL2_bit4 -VOL2_bit5 -VOL2_bit6 -VOL2_bit7 -VOL2_bit8 -VOL2_bit9 -VOL2_bit10 -VOL2_bit11 -VOL2_bit12 -VOL3_bit_7 -VOL3_bit_6 -VOL3_bit_5 -VOL3_bit_4 -VOL3_bit_3 -VOL3_bit_2 -VOL3_bit_1 -VOL3_bit0 VOL3_bit1 VOL3_bit2 VOL3_bit3 VOL3_bit4 -VOL4_bit_7 -VOL4_bit_6 -VOL4_bit_5 -VOL4_bit_4 -VOL4_bit_3 -VOL4_bit_2 -VOL4_bit_1 -VOL4_bit0 -VOL4_bit1 -VOL4_bit2 -VOL4_bit3 -VOL4_bit4 c _______________________________________________________________________________ c c restarts : 157 c conflicts : 36278 (2197 /sec) c decisions : 72750 (4406 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 16.5125 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.78 0.95 0.95 2/54 6287 Raw data (stat): 6287 (runsolver) R 6286 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540288734 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0008 s] Raw data (loadavg): 0.82 0.95 0.95 2/54 6287 Raw data (stat): 6287 (minisat+) R 6286 18865 18864 0 -1 0 679 0 0 0 996 2 0 0 25 0 1 0 540288734 4366336 657 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1066 657 603 41 0 1025 0 vsize: 4264 [startup+16.5703 s] Raw data (loadavg): 0.84 0.95 0.95 1/53 6287 Raw data (stat): 6287 (minisat+) R 6286 18865 18864 0 -1 0 679 0 0 0 996 2 0 0 25 0 1 0 540288734 4366336 657 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1066 657 603 41 0 1025 0 vsize: 0 Child status: 30 Real time (s): 16.5701 CPU time (s): 16.5525 CPU user time (s): 16.5145 CPU system time (s): 0.037994 CPU usage (%): 99.8939 Max. virtual memory (Kb): 4264 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 43097 #### END VERIFIER DATA ####