Name | submitted/aloul/FPGA_SAT05/normalized-fpga11_11_sat_pb.cnf.cr.opb |
MD5SUM | c8e6fe6db41022cd334d76fea54bd93c |
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 | 12 |
Number of bits of the biggest sum of numbers | 4 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.035993 |
Number of variables | 182 |
Total number of constraints | 154 |
Number of constraints which are clauses | 132 |
Number of constraints which are cardinality constraints (but not clauses) | 22 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 5 |
Maximum length of a constraint | 11 |
LAUNCH ON wulflinc21 THE 2005-09-18 07:59:54 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23 boxname=wulflinc21 idbench=23 idsolver=1 numberseed=0 MD5SUM SOLVER: 38f99674050b34630888bf623b924b59 /oldhome/oroussel/solvers/bsolo MD5SUM BENCH: c8e6fe6db41022cd334d76fea54bd93c /oldhome/oroussel/tmp/wulflinc21/normalized-fpga11_11_sat_pb.cnf.cr.opb REAL COMMAND: bsolo /oldhome/oroussel/tmp/wulflinc21/normalized-fpga11_11_sat_pb.cnf.cr.opb IDLAUNCH: 23 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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: 938928 kB Buffers: 33340 kB Cached: 35248 kB SwapCached: 908 kB Active: 64900 kB Inactive: 6324 kB HighTotal: 131008 kB HighFree: 93324 kB LowTotal: 903652 kB LowFree: 845604 kB SwapTotal: 2097892 kB SwapFree: 2096472 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5804 kB Slab: 18868 kB Committed_AS: 64368 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 08:00:53 (client local time) WITH STATUS 10 IN 58.0932 SECONDS stats: 23 0 58.0932 10
c INFO: OSL Context initialized. c INFO: No cost function. Find solution and finish. c Initial problem consists of 182 variables and 154 constraints. c Using non-optimization problem switches. c No problem reductions applied in OPT. instance. c preprocess terminated. Elapsed time: 0.077 c After prepocess the problem consists of 182 variables and 154 constraints. c Restart #1 #Var: 182 #Dec: 297 LB: 0 @ 0.218 c Restart #2 #Var: 182 #Dec: 1137 LB: 0 @ 0.553 c Restart #3 #Var: 182 #Dec: 1976 LB: 0 @ 1.076 c Restart #4 #Var: 182 #Dec: 3269 LB: 0 @ 2.152 c Restart #5 #Var: 182 #Dec: 4586 LB: 0 @ 3.743 c Restart #6 #Var: 182 #Dec: 5869 LB: 0 @ 6.085 c Restart #7 #Var: 182 #Dec: 7300 LB: 0 @ 9.807 c Restart #8 #Var: 182 #Dec: 8918 LB: 0 @ 14.811 c Restart #9 #Var: 182 #Dec: 10749 LB: 0 @ 22.104 c Restart #10 #Var: 182 #Dec: 12787 LB: 0 @ 30.566 c Restart #11 #Var: 182 #Dec: 15012 LB: 0 @ 42.833 c NEW SOLUTION FOUND: 0 @ 58.072 @ #Dec. 16791 s SATISFIABLE v -v83 -v147 -v148 -v149 -v150 v151 -v152 -v81 v137 -v138 -v139 -v140 -v141 -v78 -v122 v123 -v124 -v125 -v126 -v80 -v132 -v133 -v134 -v135 v136 v26 v57 -v127 -v128 -v129 v130 -v131 -v96 -v159 -v160 v161 -v162 -v163 -v164 -v53 -v165 v166 -v167 -v168 -v169 -v170 -v66 v177 -v178 -v179 -v180 -v181 -v182 -v44 -v40 -v153 -v154 -v155 v156 -v157 -v158 -v50 -v2 -v64 -v35 -v45 -v46 -v47 -v48 -v49 -v51 -v52 -v54 v55 -v74 -v92 -v111 v86 -v30 -v13 -v70 -v79 -v82 -v84 -v85 -v87 -v88 -v90 -v56 -v58 -v59 -v60 -v61 -v62 -v63 -v65 -v114 -v118 -v5 -v142 -v143 v144 -v145 -v146 -v121 -v76 -v171 -v172 -v173 -v174 -v175 v176 -v16 -v10 -v77 -v22 -v15 -v120 -v89 -v12 -v14 -v17 v18 -v19 -v20 -v21 -v67 -v68 -v69 v71 -v72 -v73 -v75 -v115 -v24 -v112 -v113 v116 -v117 -v119 -v11 -v8 -v97 -v27 -v110 -v7 -v42 v107 -v99 -v38 -v91 -v109 -v108 -v9 v34 -v36 -v37 -v39 -v41 -v43 -v102 -v32 v3 -v28 -v93 -v94 -v95 v98 -v23 -v25 -v29 -v31 -v33 -v1 -v4 -v6 -v105 -v104 -v100 -v101 -v103 -v106 c Cost: 0 c Exit Code: 10 c Total time: 58.074 s
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/20844/stat): 20844 (bsolo) R 20843 20844 20602 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1716914538 438272 3 4294967295 134512640 134736556 3221224560 3221224560 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/20844/statm): 107 3 90 68 0 39 0 [pid=20844] vsize: 428 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libosl.so open syscall for file tls/i686/libosl.so open syscall for file tls/mmx/libosl.so open syscall for file tls/libosl.so open syscall for file i686/mmx/libosl.so open syscall for file i686/libosl.so open syscall for file mmx/libosl.so open syscall for file libosl.so open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libosl.so open syscall for file /oldhome/oroussel/lib/tls/i686/libosl.so open syscall for file /oldhome/oroussel/lib/tls/mmx/libosl.so open syscall for file /oldhome/oroussel/lib/tls/libosl.so open syscall for file /oldhome/oroussel/lib/i686/mmx/libosl.so open syscall for file /oldhome/oroussel/lib/i686/libosl.so open syscall for file /oldhome/oroussel/lib/mmx/libosl.so open syscall for file /oldhome/oroussel/lib/libosl.so open syscall for file tls/i686/mmx/libstdc++-libc6.2-2.so.3 open syscall for file tls/i686/libstdc++-libc6.2-2.so.3 open syscall for file tls/mmx/libstdc++-libc6.2-2.so.3 open syscall for file tls/libstdc++-libc6.2-2.so.3 open syscall for file i686/mmx/libstdc++-libc6.2-2.so.3 open syscall for file i686/libstdc++-libc6.2-2.so.3 open syscall for file mmx/libstdc++-libc6.2-2.so.3 open syscall for file libstdc++-libc6.2-2.so.3 open syscall for file /oldhome/oroussel/lib/libstdc++-libc6.2-2.so.3 open syscall for file /etc/ld.so.cache open syscall for file /usr/lib/libstdc++-libc6.2-2.so.3 open syscall for file tls/i686/mmx/libm.so.6 open syscall for file tls/i686/libm.so.6 open syscall for file tls/mmx/libm.so.6 open syscall for file tls/libm.so.6 open syscall for file i686/mmx/libm.so.6 open syscall for file i686/libm.so.6 open syscall for file mmx/libm.so.6 open syscall for file libm.so.6 open syscall for file /oldhome/oroussel/lib/libm.so.6 open syscall for file /lib/tls/libm.so.6 open syscall for file tls/i686/mmx/libpthread.so.0 open syscall for file tls/i686/libpthread.so.0 open syscall for file tls/mmx/libpthread.so.0 open syscall for file tls/libpthread.so.0 open syscall for file i686/mmx/libpthread.so.0 open syscall for file i686/libpthread.so.0 open syscall for file mmx/libpthread.so.0 open syscall for file libpthread.so.0 open syscall for file /oldhome/oroussel/lib/libpthread.so.0 open syscall for file /lib/tls/libpthread.so.0 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file tls/i686/mmx/libgcc_s.so.1 open syscall for file tls/i686/libgcc_s.so.1 open syscall for file tls/mmx/libgcc_s.so.1 open syscall for file tls/libgcc_s.so.1 open syscall for file i686/mmx/libgcc_s.so.1 open syscall for file i686/libgcc_s.so.1 open syscall for file mmx/libgcc_s.so.1 open syscall for file libgcc_s.so.1 open syscall for file /oldhome/oroussel/lib/libgcc_s.so.1 open syscall for file /lib/libgcc_s.so.1 open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /etc/localtime open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/.OptimizationSolutions/nodelock open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-fpga11_11_sat_pb.cnf.cr.opb [startup+10.0027 s] Raw data (loadavg): 0.93 0.96 0.72 2/57 20844 Raw data (/proc/20844/stat): 20844 (bsolo) R 20843 20844 20602 0 -1 0 2500 0 0 0 948 21 0 0 25 0 1 0 1716914538 13340672 2411 4294967295 134512640 134736556 3221224560 3221223232 134528594 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/20844/statm): 3257 2411 1116 68 0 3189 0 [pid=20844] vsize: 13028 Current children cumulated CPU time (s) 9.69 Current children cumulated vsize (Kb) 13028 [startup+20.0024 s] Raw data (loadavg): 0.94 0.96 0.73 2/57 20844 Raw data (/proc/20844/stat): 20844 (bsolo) R 20843 20844 20602 0 -1 0 3557 0 0 0 1926 30 0 0 25 0 1 0 1716914538 17678336 3468 4294967295 134512640 134736556 3221224560 3221223096 1077378037 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/20844/statm): 4316 3468 1116 68 0 4248 0 [pid=20844] vsize: 17264 Current children cumulated CPU time (s) 19.56 Current children cumulated vsize (Kb) 17264 [startup+30.0031 s] Raw data (loadavg): 0.95 0.96 0.73 2/57 20844 Raw data (/proc/20844/stat): 20844 (bsolo) R 20843 20844 20602 0 -1 0 4439 0 0 0 2907 39 0 0 25 0 1 0 1716914538 21340160 4350 4294967295 134512640 134736556 3221224560 3221223156 134540399 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/20844/statm): 5210 4350 1116 68 0 5142 0 [pid=20844] vsize: 20840 Current children cumulated CPU time (s) 29.46 Current children cumulated vsize (Kb) 20840 [startup+40.0028 s] Raw data (loadavg): 0.96 0.96 0.73 2/57 20844 Raw data (/proc/20844/stat): 20844 (bsolo) R 20843 20844 20602 0 -1 0 5167 0 0 0 3889 49 0 0 25 0 1 0 1716914538 24354816 5078 4294967295 134512640 134736556 3221224560 3221223040 134535737 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/20844/statm): 5946 5078 1116 68 0 5878 0 [pid=20844] vsize: 23784 Current children cumulated CPU time (s) 39.38 Current children cumulated vsize (Kb) 23784 [startup+50.0034 s] Raw data (loadavg): 0.96 0.96 0.73 2/57 20844 Raw data (/proc/20844/stat): 20844 (bsolo) R 20843 20844 20602 0 -1 0 5665 0 0 0 4880 53 0 0 25 0 1 0 1716914538 26402816 5575 4294967295 134512640 134736556 3221224560 3221223272 134694468 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/20844/statm): 6446 5575 1116 68 0 6378 0 [pid=20844] vsize: 25784 Current children cumulated CPU time (s) 49.33 Current children cumulated vsize (Kb) 25784 One traced child (pid=20844) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 58.8113 CPU time (s): 58.0932 CPU user time (s): 57.5223 CPU system time (s): 0.570913 CPU usage (%): 98.779 Max. virtual memory (cumulated for all children) (Kb): 25784
Verifier: OK 0