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-fpga10_8_sat_pb.cnf.cr.opb
MD5SUM	159220fb0573bb17ad11cefe6a440cec
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	11
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.040992
Number of variables	120
Total number of constraints	106
Number of constraints which are clauses	88
Number of constraints which are cardinality constraints (but not clauses)	18
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	5
Maximum length of a constraint	10

Trace number 29025

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-05-25 04:38:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20433 boxname=wulflinc19 idbench=23 idsolver=14 numberseed=0
MD5SUM SOLVER: d29da23ec752be69e0579424c0f0767e  /oldhome/oroussel/solvers/sat4jPseudoBis.jar
MD5SUM BENCH:  159220fb0573bb17ad11cefe6a440cec  /oldhome/oroussel/tmp/wulflinc19/normalized-fpga10_8_sat_pb.cnf.cr.opb
REAL COMMAND:  java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudoBis.jar /oldhome/oroussel/tmp/wulflinc19/normalized-fpga10_8_sat_pb.cnf.cr.opb
IDLAUNCH: 20433
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        656248 kB
Buffers:         27228 kB
Cached:         324460 kB
SwapCached:        416 kB
Active:          32588 kB
Inactive:       321276 kB
HighTotal:      131008 kB
HighFree:          700 kB
LowTotal:       903652 kB
LowFree:        655548 kB
SwapTotal:     2097892 kB
SwapFree:      2096804 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5676 kB
Slab:            18840 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 04:43:19 (client local time) WITH STATUS 10 IN 318.046 SECONDS
stats: 20433 0 318.046 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c SAT4J: a SATisfiability library for Java (c) 2004-2005 Daniel Le Berre
c This is free software under the GNU LGPL licence. See www.sat4j.org for details.
c version Special PB05 Second trial
c --- Begin Solver configuration ---
c org.sat4j.minisat.uip.FirstUIP@1e4cbc4
c org.sat4j.minisat.constraints.PBMinDataStructure@1fdc96c
c org.sat4j.minisat.learning.MiniSATLearning@b2fd8f
c conflictBoundIncFactor=1.5 learntBoundIncFactor=1.1 initLearntBoundConstraintFactor=0.5 initConflictBound=100 
c 
c --- End Solver configuration ---
c solving /oldhome/oroussel/tmp/wulflinc19/normalized-fpga10_8_sat_pb.cnf.cr.opb
c reading problem ... done. Time 0.32 ms.
c #vars     120
c #constraints  106
c starts	: 8
c conflicts	: 4074
c decisions	: 10112
c propagations	: 54698
c inspects	: 1731353
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 4074
c root simplifications	: 8
s SATISFIABLE
v v27 -v105 -v106 -v107 v108 v20 -v117 v118 -v119 -v120 -v13 -v89 -v90 -v91 v92 -v69 -v113 -v114 v115 -v116 -v24 -v93 -v94 -v95 -v96 -v68 -v109 -v110 -v111 -v112 -v15 -v97 -v98 v99 -v100 -v1 -v81 v82 -v83 -v84 -v46 v101 -v102 -v103 -v104 v61 -v29 -v35 -v16 -v63 -v64 -v77 -v39 -v34 -v53 -v49 v79 -v55 -v54 -v65 -v62 -v66 -v67 -v70 -v74 -v2 -v3 -v4 v5 -v6 -v7 -v8 -v9 -v10 -v42 v85 -v86 -v87 -v88 -v40 -v41 -v33 -v31 v32 -v36 -v37 -v38 v56 -v71 -v28 -v72 -v73 -v75 -v76 -v78 -v80 -v12 -v21 -v22 -v23 -v25 -v26 -v30 -v44 -v14 -v51 -v19 -v11 -v58 v43 -v50 -v57 -v59 -v52 -v17 -v18 -v45 -v60 -v48 -v47 
c Total CPU time (ms) : 311.192
#### 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.95 0.98 0.92 2/54 20460
Raw data (stat): 20460 (runsolver) R 20459 10795 10794 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 836050854 1052672 99 4294967295 134512640 135381576 3221224400 3221219620 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.0002 s]
Raw data (loadavg): 1.12 1.02 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18067 0 2 0 733 38 0 0 25 0 11 0 836050854 859103232 19915 4294967295 134512640 134569956 3221224368 3221214680 1131166740 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209742 19915 13086 16 0 209726 0
vsize: 838968
[startup+20.0004 s]
Raw data (loadavg): 1.10 1.02 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18067 0 2 0 1709 38 0 0 25 0 11 0 836050854 858771456 20916 4294967295 134512640 134569956 3221224368 3221214208 1131274592 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 20916 13086 16 0 209645 0
vsize: 838644
[startup+30.0005 s]
Raw data (loadavg): 1.09 1.01 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18067 0 2 0 2676 38 0 0 25 0 11 0 836050854 858771456 21685 4294967295 134512640 134569956 3221224368 3221214064 1131272002 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 21685 13086 16 0 209645 0
vsize: 838644
[startup+40.004 s]
Raw data (loadavg): 1.07 1.01 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18067 0 2 0 3646 38 0 0 25 0 11 0 836050854 858771456 21874 4294967295 134512640 134569956 3221224368 3221214096 1131272008 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 21874 13086 16 0 209645 0
vsize: 838644
[startup+50.0121 s]
Raw data (loadavg): 1.06 1.01 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 4637 38 0 0 25 0 11 0 836050854 858771456 21877 4294967295 134512640 134569956 3221224368 3221214528 1131274561 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 21877 13086 16 0 209645 0
vsize: 838644
[startup+60.0121 s]
Raw data (loadavg): 1.05 1.01 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 5616 38 0 0 25 0 11 0 836050854 858771456 22054 4294967295 134512640 134569956 3221224368 3221214432 1131274641 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 22054 13086 16 0 209645 0
vsize: 838644
[startup+70.0127 s]
Raw data (loadavg): 1.04 1.01 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 6605 38 0 0 25 0 11 0 836050854 858771456 22187 4294967295 134512640 134569956 3221224368 3221214336 1131274698 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 22187 13086 16 0 209645 0
vsize: 838644
[startup+80.0133 s]
Raw data (loadavg): 1.04 1.01 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 7585 38 0 0 25 0 11 0 836050854 858771456 22313 4294967295 134512640 134569956 3221224368 3221214528 1131274616 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 22313 13086 16 0 209645 0
vsize: 838644
[startup+90.0145 s]
Raw data (loadavg): 1.03 1.01 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 8576 38 0 0 25 0 11 0 836050854 858771456 22314 4294967295 134512640 134569956 3221224368 3221214808 1131144153 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 22314 13086 16 0 209645 0
vsize: 838644
[startup+100.015 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 9555 39 0 0 25 0 11 0 836050854 858771456 22390 4294967295 134512640 134569956 3221224368 3221213960 1131274616 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 22390 13086 16 0 209645 0
vsize: 838644
[startup+110.015 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 10532 39 0 0 25 0 11 0 836050854 858771456 22571 4294967295 134512640 134569956 3221224368 3221214528 1131274641 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 22571 13086 16 0 209645 0
vsize: 838644
[startup+120.016 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 11512 39 0 0 25 0 11 0 836050854 858771456 22650 4294967295 134512640 134569956 3221224368 3221214112 1085679762 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 22650 13086 16 0 209645 0
vsize: 838644
[startup+130.016 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 12492 39 0 0 25 0 11 0 836050854 858771456 22665 4294967295 134512640 134569956 3221224368 3221214148 1131271979 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 22665 13086 16 0 209645 0
vsize: 838644
[startup+140.018 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 13481 39 0 0 25 0 11 0 836050854 858771456 22748 4294967295 134512640 134569956 3221224368 3221214292 1131275072 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 22748 13086 16 0 209645 0
vsize: 838644
[startup+150.018 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 14460 39 0 0 25 0 11 0 836050854 858771456 22817 4294967295 134512640 134569956 3221224368 3221214096 1131309273 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 22817 13086 16 0 209645 0
vsize: 838644
[startup+160.018 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 15439 39 0 0 25 0 11 0 836050854 858771456 22919 4294967295 134512640 134569956 3221224368 3221214656 1131167245 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 22919 13086 16 0 209645 0
vsize: 838644
[startup+170.019 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 16418 40 0 0 25 0 11 0 836050854 858771456 22992 4294967295 134512640 134569956 3221224368 3221214192 1131272002 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 22992 13086 16 0 209645 0
vsize: 838644
[startup+180.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 17397 40 0 0 25 0 11 0 836050854 858771456 23043 4294967295 134512640 134569956 3221224368 3221214104 1131271903 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23043 13086 16 0 209645 0
vsize: 838644
[startup+190.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 18376 40 0 0 25 0 11 0 836050854 858771456 23104 4294967295 134512640 134569956 3221224368 3221214432 1131274489 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23104 13086 16 0 209645 0
vsize: 838644
[startup+200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 19365 40 0 0 25 0 11 0 836050854 858771456 23159 4294967295 134512640 134569956 3221224368 3221214656 1131166754 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23159 13086 16 0 209645 0
vsize: 838644
[startup+210.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 20344 40 0 0 25 0 11 0 836050854 858771456 23218 4294967295 134512640 134569956 3221224368 3221214152 1131274641 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23218 13086 16 0 209645 0
vsize: 838644
[startup+220.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 21311 40 0 0 25 0 11 0 836050854 858771456 23318 4294967295 134512640 134569956 3221224368 3221214432 1131274561 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23318 13086 16 0 209645 0
vsize: 838644
[startup+230.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 22290 40 0 0 25 0 11 0 836050854 858771456 23434 4294967295 134512640 134569956 3221224368 3221213912 1131274616 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23434 13086 16 0 209645 0
vsize: 838644
[startup+240.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 23268 40 0 0 25 0 11 0 836050854 858771456 23510 4294967295 134512640 134569956 3221224368 3221214192 1131309410 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23510 13086 16 0 209645 0
vsize: 838644
[startup+250.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 24258 40 0 0 25 0 11 0 836050854 858771456 23544 4294967295 134512640 134569956 3221224368 3221214240 1131274616 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23544 13086 16 0 209645 0
vsize: 838644
[startup+260.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 25236 40 0 0 25 0 11 0 836050854 858771456 23628 4294967295 134512640 134569956 3221224368 3221214240 1131267501 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23628 13086 16 0 209645 0
vsize: 838644
[startup+270.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 26226 40 0 0 25 0 11 0 836050854 858771456 23669 4294967295 134512640 134569956 3221224368 3221214336 1131274668 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23669 13086 16 0 209645 0
vsize: 838644
[startup+280.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 27203 40 0 0 25 0 11 0 836050854 858771456 23706 4294967295 134512640 134569956 3221224368 3221214536 1131259021 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23706 13086 16 0 209645 0
vsize: 838644
[startup+290.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 28181 41 0 0 24 0 11 0 836050854 858771456 23786 4294967295 134512640 134569956 3221224368 3221214528 1131274650 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23786 13086 16 0 209645 0
vsize: 838644
[startup+300.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 29171 41 0 0 25 0 11 0 836050854 858771456 23820 4294967295 134512640 134569956 3221224368 3221213952 1131274564 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23820 13086 16 0 209645 0
vsize: 838644
[startup+310.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 20470
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 30139 41 0 0 25 0 11 0 836050854 858771456 23910 4294967295 134512640 134569956 3221224368 3221214144 1131274641 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23910 13086 16 0 209645 0
vsize: 838644
[startup+312.175 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 20471
Raw data (stat): 20460 (java) R 20459 10795 10794 0 -1 0 18068 0 2 0 30139 41 0 0 25 0 11 0 836050854 858771456 23910 4294967295 134512640 134569956 3221224368 3221214144 1131274641 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209661 23910 13086 16 0 209645 0
vsize: 0

Child status: 10
Real time (s): 312.174
CPU time (s): 318.046
CPU user time (s): 317.413
CPU system time (s): 0.632903
CPU usage (%): 101.881
Max. virtual memory (Kb): 838968
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	0
#### END VERIFIER DATA ####