Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga35_33_sat_pb.cnf.cr.opb |
MD5SUM | d4fd8917eebbcee2e1b2df9714e1fab8 |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 36 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.59276 |
Number of variables | 1733 |
Total number of constraints | 1256 |
Number of constraints which are clauses | 1188 |
Number of constraints which are cardinality constraints (but not clauses) | 68 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 17 |
Maximum length of a constraint | 35 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc13 THE 2005-04-13 19:27:45 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3433 boxname=wulflinc13 idbench=49 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: d4fd8917eebbcee2e1b2df9714e1fab8 /oldhome/oroussel/tmp/wulflinc13/normalized-fpga35_33_sat_pb.cnf.cr.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc13/normalized-fpga35_33_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc13/normalized-fpga35_33_sat_pb.cnf.cr.opb IDLAUNCH: 3433 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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.242 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: 925392 kB Buffers: 33872 kB Cached: 55632 kB SwapCached: 392 kB Active: 47984 kB Inactive: 44816 kB HighTotal: 131008 kB HighFree: 71372 kB LowTotal: 903652 kB LowFree: 854020 kB SwapTotal: 2097136 kB SwapFree: 2096744 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6928 kB Slab: 10860 kB Committed_AS: 63480 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 19:29:20 (client local time) WITH STATUS 30 IN 94.6636 SECONDS stats: 3433 7 94.6636 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 1256 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ---[ 67]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 66]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 65]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 64]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 63]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 62]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 61]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 60]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 59]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 58]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 57]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 56]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 55]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 54]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 53]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 52]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 51]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 50]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 49]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 48]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 47]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 46]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 45]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 44]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 43]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 42]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 41]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 40]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 39]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 38]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 37]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 36]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 35]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 34]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 33]---> Adder-cost: 62 maxlim: 31 bits: 6/5 c ---[ 32]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 31]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 30]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 29]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 28]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 27]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 26]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 25]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 24]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 23]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 22]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 21]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 20]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 19]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 18]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 17]---> Adder-cost: 30 maxlim: 15 bits: 5/4 c ---[ 16]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 15]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 14]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 13]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 12]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 11]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 10]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 9]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 8]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 7]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 6]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 5]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 4]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 3]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 2]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 1]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ---[ 0]---> Adder-cost: 32 maxlim: 16 bits: 5/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 18996 84463 | 6332 0 0 nan | 0.000 % | c | 100 | 18728 83549 | 6965 62 215 3.5 | 9.494 % | c | 250 | 18562 82985 | 7661 186 662 3.6 | 10.102 % | c | 475 | 18403 82442 | 8427 388 1380 3.6 | 10.710 % | c | 812 | 18200 81725 | 9270 701 3049 4.3 | 11.493 % | c | 1318 | 17425 79052 | 10197 1105 5046 4.6 | 14.534 % | c | 2077 | 15801 73402 | 11217 1630 8241 5.1 | 20.878 % | c | 3219 | 12811 63424 | 12339 2237 81267 36.3 | 32.935 % | c | 4932 | 12674 62971 | 13573 3924 650848 165.9 | 33.478 % | c | 7494 | 12085 61036 | 14930 6367 1549272 243.3 | 35.933 % | c | 11338 | 11847 60246 | 16423 10171 2789227 274.2 | 36.911 % | c | 17105 | 11798 60083 | 18065 15926 4585118 287.9 | 37.106 % | c | 25754 | 11714 59803 | 19872 14058 4980985 354.3 | 37.454 % | c | 38728 | 10738 56541 | 21859 15561 4292876 275.9 | 41.234 % | c ============================================================================== c [1mSATISFIABLE: No goal function specified.[0m s SATISFIABLE v c _______________________________________________________________________________ c c restarts : 14 c conflicts : 39279 (416 /sec) c decisions : 1158171 (12271 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 94.3857 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.22 0.06 0.02 2/54 544 Raw data (stat): 544 (runsolver) R 543 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420250191 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.0003 s] Raw data (loadavg): 0.34 0.09 0.03 2/54 544 Raw data (stat): 544 (minisat+) R 543 30701 30700 0 -1 0 1700 0 0 0 994 4 0 0 25 0 1 0 420250191 8683520 1678 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2120 1678 603 41 0 2079 0 vsize: 8480 [startup+20.0014 s] Raw data (loadavg): 0.44 0.12 0.04 2/54 544 Raw data (stat): 544 (minisat+) R 543 30701 30700 0 -1 0 3687 0 0 0 1989 9 0 0 25 0 1 0 420250191 16814080 3665 4294967295 134512640 134672761 3221224528 3221223712 134558843 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4105 3665 603 41 0 4064 0 vsize: 16420 [startup+30.0017 s] Raw data (loadavg): 0.53 0.15 0.05 2/54 544 Raw data (stat): 544 (minisat+) R 543 30701 30700 0 -1 0 5551 0 0 0 2985 13 0 0 25 0 1 0 420250191 24494080 5529 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5980 5529 603 41 0 5939 0 vsize: 23920 [startup+40.0013 s] Raw data (loadavg): 0.60 0.17 0.06 2/54 544 Raw data (stat): 544 (minisat+) R 543 30701 30700 0 -1 0 7423 0 0 0 3979 18 0 0 25 0 1 0 420250191 32202752 7401 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7862 7401 603 41 0 7821 0 vsize: 31448 [startup+50.0024 s] Raw data (loadavg): 0.66 0.20 0.07 2/54 544 Raw data (stat): 544 (minisat+) R 543 30701 30700 0 -1 0 8046 0 0 0 4977 20 0 0 25 0 1 0 420250191 34643968 8024 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8458 8024 603 41 0 8417 0 vsize: 33832 [startup+60.0016 s] Raw data (loadavg): 0.71 0.23 0.08 2/54 544 Raw data (stat): 544 (minisat+) R 543 30701 30700 0 -1 0 8046 0 0 0 5977 20 0 0 25 0 1 0 420250191 34643968 8024 4294967295 134512640 134672761 3221224528 3221223736 1075346913 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8458 8024 603 41 0 8417 0 vsize: 33832 [startup+70.0023 s] Raw data (loadavg): 0.76 0.25 0.09 2/54 544 Raw data (stat): 544 (minisat+) R 543 30701 30700 0 -1 0 8046 0 0 0 6977 21 0 0 25 0 1 0 420250191 34643968 8024 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8458 8024 603 41 0 8417 0 vsize: 33832 [startup+80.0033 s] Raw data (loadavg): 0.79 0.28 0.10 2/54 544 Raw data (stat): 544 (minisat+) R 543 30701 30700 0 -1 0 9105 0 0 0 7974 24 0 0 25 0 1 0 420250191 39108608 9083 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9548 9083 603 41 0 9507 0 vsize: 38192 [startup+90.0026 s] Raw data (loadavg): 0.82 0.30 0.10 2/54 544 Raw data (stat): 544 (minisat+) R 543 30701 30700 0 -1 0 9721 0 0 0 8972 25 0 0 25 0 1 0 420250191 41541632 9699 4294967295 134512640 134672761 3221224528 3221223716 1075346949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10142 9699 603 41 0 10101 0 vsize: 40568 [startup+94.6842 s] Raw data (loadavg): 0.84 0.31 0.11 1/53 544 Raw data (stat): 544 (minisat+) R 543 30701 30700 0 -1 0 9721 0 0 0 8972 25 0 0 25 0 1 0 420250191 41541632 9699 4294967295 134512640 134672761 3221224528 3221223716 1075346949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10142 9699 603 41 0 10101 0 vsize: 0 Child status: 30 Real time (s): 94.6839 CPU time (s): 94.6636 CPU user time (s): 94.3876 CPU system time (s): 0.275958 CPU usage (%): 99.9786 Max. virtual memory (Kb): 40568 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####