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/web/uclid_pb_benchmarks/normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb
MD5SUM	6bfe4c2dce1e5dbe61cc34b52b1b387f
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
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	130
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	512
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	45.816
Number of variables	87751
Total number of constraints	254772
Number of constraints which are clauses	247060
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	7712
Minimum length of a constraint	1
Maximum length of a constraint	15

Trace number 24539

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-10 22:05:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2514 boxname=wulflinc31 idbench=280 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  6bfe4c2dce1e5dbe61cc34b52b1b387f  /oldhome/oroussel/tmp/wulflinc31/normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc31/normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb
IDLAUNCH: 2514
/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:        918988 kB
Buffers:         27452 kB
Cached:          63372 kB
SwapCached:       1588 kB
Active:          52308 kB
Inactive:        41276 kB
HighTotal:      131008 kB
HighFree:        70252 kB
LowTotal:       903652 kB
LowFree:        848736 kB
SwapTotal:     2097892 kB
SwapFree:      2095268 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4812 kB
Slab:            16280 kB
Committed_AS:    63648 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-10 22:09:23 (client local time) WITH STATUS 0 IN 226.292 SECONDS
stats: 2514 7 226.292 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: No cost function. Find solution and finish.
c Initial problem consists of 87751 variables and 254772 constraints.
#### 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 19518
Raw data (stat): 19518 (runsolver) R 19517 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 712709318 1056768 100 4294967295 134512640 135381576 3221221664 3221216884 135158418 0 2147483391 1 90112 0 0 0 17 1 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 18033 0 0 0 952 44 0 0 25 0 1 0 712709318 45531136 7709 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11073 7698 1111 63 0 11010 0
vsize: 44464
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 104462 0 0 0 1807 189 0 0 25 0 1 0 712709318 64114688 12276 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 15653 12276 1111 63 0 15590 0
vsize: 62612
[startup+30.002 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 327370 0 0 0 2413 583 0 0 25 0 1 0 712709318 75227136 14901 4294967295 134512640 134714540 3221221760 3221220064 134568032 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18366 14901 1111 63 0 18303 0
vsize: 73464
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 551815 0 0 0 3006 990 0 0 25 0 1 0 712709318 84463616 17172 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20621 17172 1111 63 0 20558 0
vsize: 82484
[startup+50.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 770666 0 0 0 3612 1385 0 0 25 0 1 0 712709318 92147712 19111 4294967295 134512640 134714540 3221221760 3221219960 1077799185 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 22497 19112 1111 63 0 22434 0
vsize: 89988
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 984387 0 0 0 4223 1774 0 0 25 0 1 0 712709318 99409920 20880 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 24270 20886 1111 63 0 24207 0
vsize: 97080
[startup+70.0025 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 1194838 0 0 0 4835 2162 0 0 25 0 1 0 712709318 106856448 22650 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 26088 22656 1111 63 0 26025 0
vsize: 104352
[startup+80.0034 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 1403556 0 0 0 5452 2545 0 0 25 0 1 0 712709318 112836608 24124 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 27548 24130 1111 63 0 27485 0
vsize: 110192
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 1616606 0 0 0 6051 2946 0 0 25 0 1 0 712709318 118673408 25545 4294967295 134512640 134714540 3221221760 3221219804 1077387418 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 28973 25545 1111 63 0 28910 0
vsize: 115892
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 1822849 0 0 0 6658 3339 0 0 25 0 1 0 712709318 124600320 26861 4294967295 134512640 134714540 3221221760 3221219960 1077799185 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 30420 26862 1111 63 0 30357 0
vsize: 121680
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 2026027 0 0 0 7273 3724 0 0 25 0 1 0 712709318 129765376 28121 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 31681 28126 1111 63 0 31618 0
vsize: 126724
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 2226045 0 0 0 7890 4107 0 0 25 0 1 0 712709318 134664192 29294 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 32877 29299 1111 63 0 32814 0
vsize: 131508
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 2428895 0 0 0 8501 4497 0 0 25 0 1 0 712709318 139284480 30433 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 34005 30433 1111 63 0 33942 0
vsize: 136020
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 2628303 0 0 0 9116 4882 0 0 25 0 1 0 712709318 143626240 31498 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 35065 31504 1111 63 0 35002 0
vsize: 140260
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 2827363 0 0 0 9720 5278 0 0 25 0 1 0 712709318 147984384 32556 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 36129 32561 1111 63 0 36066 0
vsize: 144516
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 3024243 0 0 0 10338 5660 0 0 25 0 1 0 712709318 151924736 33526 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 37091 33531 1111 63 0 37028 0
vsize: 148364
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 3222163 0 0 0 10956 6042 0 0 25 0 1 0 712709318 155996160 34563 4294967295 134512640 134714540 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 38085 34568 1111 63 0 38022 0
vsize: 152340
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 3376916 0 0 0 11650 6349 0 0 25 0 1 0 712709318 164585472 36679 4294967295 134512640 134714540 3221221760 3221218236 1077206765 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 40182 36679 1111 63 0 40119 0
vsize: 160728
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 3556126 0 0 0 12218 6780 0 0 25 0 1 0 712709318 419168256 100561 4294967295 134512640 134714540 3221221760 3221220400 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 102336 100568 1111 63 0 102273 0
vsize: 409344
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 3742220 0 0 0 12771 7227 0 0 25 0 1 0 712709318 497369088 119729 4294967295 134512640 134714540 3221221760 3221220400 134606468 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 121428 119736 1111 63 0 121365 0
vsize: 485712
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 3933198 0 0 0 13311 7687 0 0 25 0 1 0 712709318 472137728 113595 4294967295 134512640 134714540 3221221760 3221220400 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 115268 113601 1111 63 0 115205 0
vsize: 461072
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 4093177 0 0 0 13916 8083 0 0 25 0 1 0 712709318 398299136 95554 4294967295 134512640 134714540 3221221760 3221220400 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 97241 95560 1111 63 0 97178 0
vsize: 388964
[startup+226.306 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 19518
Raw data (stat): 19518 (bsolo_mis) R 19517 7876 7672 0 -1 0 4093177 0 0 0 13916 8083 0 0 25 0 1 0 712709318 398299136 95554 4294967295 134512640 134714540 3221221760 3221220400 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 97241 95560 1111 63 0 97178 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 226.306
CPU time (s): 226.292
CPU user time (s): 141.639
CPU system time (s): 84.6521
CPU usage (%): 99.9938
Max. virtual memory (Kb): 485712
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####