PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:

LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga11_10_sat_pb.cnf.cr.opb
MD5SUM	e95696bbb09fe4b39809de76f67becbf
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.042992
Number of variables	165
Total number of constraints	141
Number of constraints which are clauses	120
Number of constraints which are cardinality constraints (but not clauses)	21
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	5
Maximum length of a constraint	11

Trace number 23264

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-02 00:14:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=219 boxname=wulflinc31 idbench=25 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  e95696bbb09fe4b39809de76f67becbf  /oldhome/oroussel/tmp/wulflinc31/normalized-fpga11_10_sat_pb.cnf.cr.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc31/normalized-fpga11_10_sat_pb.cnf.cr.opb
IDLAUNCH: 219
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        929372 kB
Buffers:         37092 kB
Cached:          46296 kB
SwapCached:        864 kB
Active:          71404 kB
Inactive:        14328 kB
HighTotal:      131008 kB
HighFree:        83776 kB
LowTotal:       903652 kB
LowFree:        845596 kB
SwapTotal:     2097892 kB
SwapFree:      2096432 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5504 kB
Slab:            13896 kB
Committed_AS:    63656 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-02 00:19:16 (client local time) WITH STATUS 10 IN 263.907 SECONDS
stats: 219 0 263.907 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: No cost function. Find solution and finish.
c Initial problem consists of 165 variables and 141 constraints.
c After prepocess the problem consists of 165 variables and 141 constraints.
c preprocess terminated 0.063 s
c Not use computed LB before first solution.
c NEW SOLUTION FOUND: 0 @ 263.853
s SATISFIABLE
v -v108 v151 -v152 -v153 -v154 -v155 -v27 -v131 -v132 -v133 v134 -v135 v75 -v72 -v136 -v137 -v138 -v139 -v140 -v1 -v2 -v3 v4 -v5 -v6 -v7 -v8 -v9 -v10 -v11 -v69 -v121 -v122 v123 -v124 -v125 -v66 -v161 v162 -v163 -v164 -v165 -v18 -v141 -v142 -v143 v144 -v145 -v58 -v78 -v79 -v80 -v81 -v82 -v83 -v84 v85 -v86 -v87 -v88 -v59 -v126 -v127 -v128 -v129 v130 v40 -v51 -v15 -v14 -v19 -v146 -v147 -v148 -v149 v150 -v70 -v50 -v62 -v63 v23 -v111 v112 -v113 -v114 -v115 -v102 -v95 -v101 v116 -v117 -v118 -v119 -v120 -v46 -v71 -v76 -v156 -v157 v158 -v159 -v160 -v74 -v34 -v105 -v67 -v68 -v73 -v77 -v21 -v24 -v89 -v45 -v91 -v41 -v104 -v25 -v90 -v92 -v93 -v94 -v96 -v97 -v98 v99 -v35 -v28 -v26 -v29 -v30 -v31 -v32 -v33 -v107 -v17 -v61 -v52 -v38 v109 v13 -v103 -v49 -v22 -v110 -v100 -v106 -v53 -v65 -v42 -v12 -v16 -v20 -v43 -v57 -v39 -v56 v60 -v64 -v44 -v48 -v54 v47 -v55 -v37 -v36 
c Exit Code: 10
c Total time: 263.856 s
#### 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.90 2/54 17052
Raw data (stat): 17052 (runsolver) R 17051 7876 7672 0 -1 64 3 0 0 0 0 0 0 0 19 0 1 0 635716067 1056768 98 4294967295 134512640 135381576 3221221680 3221217048 135024953 0 0 1 90112 0 0 0 17 0 0 0
Raw data (statm): 258 98 215 215 0 43 0
vsize: 1032
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 2282 0 0 0 987 9 0 0 25 0 1 0 635716067 13029376 2257 4294967295 134512640 134714540 3221221776 3221220512 134535750 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 3181 2257 1111 63 0 3118 0
vsize: 12724
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 3160 0 0 0 1982 14 0 0 25 0 1 0 635716067 16547840 3135 4294967295 134512640 134714540 3221221776 3221220512 134535750 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 4040 3135 1111 63 0 3977 0
vsize: 16160
[startup+30.0006 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 3847 0 0 0 2979 17 0 0 25 0 1 0 635716067 19410944 3821 4294967295 134512640 134714540 3221221776 3221220700 1077781665 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 4739 3821 1111 63 0 4676 0
vsize: 18956
[startup+40.0007 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 4341 0 0 0 3977 20 0 0 25 0 1 0 635716067 21438464 4315 4294967295 134512640 134714540 3221221776 3221220408 134552681 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5234 4315 1111 63 0 5171 0
vsize: 20936
[startup+50.0005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 4960 0 0 0 4974 23 0 0 25 0 1 0 635716067 24010752 4934 4294967295 134512640 134714540 3221221776 3221220332 134535664 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 5862 4934 1111 63 0 5799 0
vsize: 23448
[startup+60.0008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 5695 0 0 0 5970 26 0 0 25 0 1 0 635716067 27127808 5669 4294967295 134512640 134714540 3221221776 3221220560 134529410 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 6623 5669 1111 63 0 6560 0
vsize: 26492
[startup+70.0014 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 6299 0 0 0 6968 29 0 0 25 0 1 0 635716067 29581312 6271 4294967295 134512640 134714540 3221221776 3221220428 134536828 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 7222 6271 1111 63 0 7159 0
vsize: 28888
[startup+80.0013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 6779 0 0 0 7964 33 0 0 25 0 1 0 635716067 31629312 6749 4294967295 134512640 134714540 3221221776 3221220364 134535956 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 7722 6749 1111 63 0 7659 0
vsize: 30888
[startup+90.0012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 7134 0 0 0 8962 35 0 0 25 0 1 0 635716067 33140736 7103 4294967295 134512640 134714540 3221221776 3221220512 134535745 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 8091 7103 1111 63 0 8028 0
vsize: 32364
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 7388 0 0 0 9960 37 0 0 25 0 1 0 635716067 34107392 7355 4294967295 134512640 134714540 3221221776 3221220332 134535967 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 8327 7355 1111 63 0 8264 0
vsize: 33308
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 7649 0 0 0 10958 39 0 0 25 0 1 0 635716067 35209216 7616 4294967295 134512640 134714540 3221221776 3221220364 134535891 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 8596 7616 1111 63 0 8533 0
vsize: 34384
[startup+120.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 7908 0 0 0 11957 41 0 0 25 0 1 0 635716067 36331520 7875 4294967295 134512640 134714540 3221221776 3221220544 134529376 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 8870 7875 1111 63 0 8807 0
vsize: 35480
[startup+130.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 8154 0 0 0 12955 42 0 0 25 0 1 0 635716067 37281792 8121 4294967295 134512640 134714540 3221221776 3221220368 134549689 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9102 8121 1111 63 0 9039 0
vsize: 36408
[startup+140.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 8423 0 0 0 13953 45 0 0 25 0 1 0 635716067 38498304 8390 4294967295 134512640 134714540 3221221776 3221220544 134584759 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9399 8390 1111 63 0 9336 0
vsize: 37596
[startup+150.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 8741 0 0 0 14951 46 0 0 25 0 1 0 635716067 39886848 8708 4294967295 134512640 134714540 3221221776 3221220544 134592104 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9738 8708 1111 63 0 9675 0
vsize: 38952
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 9150 0 0 0 15950 48 0 0 25 0 1 0 635716067 41541632 9117 4294967295 134512640 134714540 3221221776 3221220408 134552681 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10142 9117 1111 63 0 10079 0
vsize: 40568
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 9962 0 0 0 16947 51 0 0 25 0 1 0 635716067 44785664 9929 4294967295 134512640 134714540 3221221776 3221220448 134551963 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10934 9929 1111 63 0 10871 0
vsize: 43736
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 10627 0 0 0 17944 54 0 0 25 0 1 0 635716067 47489024 10594 4294967295 134512640 134714540 3221221776 3221220344 1077378037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11594 10594 1111 63 0 11531 0
vsize: 46376
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 11091 0 0 0 18941 57 0 0 25 0 1 0 635716067 49389568 11057 4294967295 134512640 134714540 3221221776 3221220332 134535649 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 12058 11057 1111 63 0 11995 0
vsize: 48232
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 11415 0 0 0 19940 58 0 0 25 0 1 0 635716067 50765824 11381 4294967295 134512640 134714540 3221221776 3221220416 134543110 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 12394 11381 1111 63 0 12331 0
vsize: 49576
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 11773 0 0 0 20939 59 0 0 25 0 1 0 635716067 52252672 11739 4294967295 134512640 134714540 3221221776 3221220344 1077378037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 12757 11739 1111 63 0 12694 0
vsize: 51028
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 12073 0 0 0 21939 60 0 0 25 0 1 0 635716067 53477376 12039 4294967295 134512640 134714540 3221221776 3221220560 134529259 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13056 12039 1111 63 0 12993 0
vsize: 52224
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 12330 0 0 0 22937 62 0 0 25 0 1 0 635716067 54558720 12296 4294967295 134512640 134714540 3221221776 3221220428 134536817 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13320 12296 1111 63 0 13257 0
vsize: 53280
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 12582 0 0 0 23936 63 0 0 25 0 1 0 635716067 55504896 12548 4294967295 134512640 134714540 3221221776 3221220368 134549541 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13551 12548 1111 63 0 13488 0
vsize: 54204
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 12801 0 0 0 24935 64 0 0 25 0 1 0 635716067 56451072 12767 4294967295 134512640 134714540 3221221776 3221220452 134551958 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13782 12767 1111 63 0 13719 0
vsize: 55128
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 13028 0 0 0 25934 65 0 0 25 0 1 0 635716067 57421824 12994 4294967295 134512640 134714540 3221221776 3221220560 134529368 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14019 12994 1111 63 0 13956 0
vsize: 56076
[startup+263.909 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 17052
Raw data (stat): 17052 (bsolo_mis) R 17051 7876 7672 0 -1 0 13028 0 0 0 25934 65 0 0 25 0 1 0 635716067 57421824 12994 4294967295 134512640 134714540 3221221776 3221220560 134529368 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14019 12994 1111 63 0 13956 0
vsize: 0

Child status: 10
Real time (s): 263.908
CPU time (s): 263.907
CPU user time (s): 263.222
CPU system time (s): 0.684895
CPU usage (%): 99.9995
Max. virtual memory (Kb): 56076
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	0
#### END VERIFIER DATA ####