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.Ih2arity.ucl.opb
MD5SUM	10884ebaf21c192c8c7003372b35d2fc
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	131
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	513
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	12.0522
Number of variables	76091
Total number of constraints	218262
Number of constraints which are clauses	207610
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	10652
Minimum length of a constraint	2
Maximum length of a constraint	15

Trace number 40829

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-06-08 22:52:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=28897 boxname=wulflinc5 idbench=283 idsolver=21 numberseed=0
MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb  /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2
MD5SUM BENCH:  10884ebaf21c192c8c7003372b35d2fc  /oldhome/oroussel/tmp/wulflinc5/normalized-cache-ibm-q-unbounded.Ih2arity.ucl.opb
REAL COMMAND:  bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc5/normalized-cache-ibm-q-unbounded.Ih2arity.ucl.opb
IDLAUNCH: 28897
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        894760 kB
Buffers:          4188 kB
Cached:         110008 kB
SwapCached:       3852 kB
Active:          26684 kB
Inactive:        92784 kB
HighTotal:      131008 kB
HighFree:        19544 kB
LowTotal:       903652 kB
LowFree:        875216 kB
SwapTotal:     2097136 kB
SwapFree:      2092324 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5076 kB
Slab:            14536 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-08 22:55:19 (client local time) WITH STATUS 0 IN 193.053 SECONDS
stats: 28897 7 193.053 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c INFO: No cost function. Find solution and finish.
c Initial problem consists of 76091 variables and 218262 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
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.91 0.94 0.90 2/54 23707
Raw data (stat): 23707 (runsolver) R 23706 7266 7265 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 905377859 884736 94 4294967295 134512640 135332820 3221224432 3221219612 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0012 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 19323 0 0 0 953 43 0 0 25 0 1 0 905377859 43651072 7309 4294967295 134512640 134716908 3221224544 3221222588 1077386340 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10657 7316 1111 63 0 10594 0
vsize: 42628
[startup+20.002 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 91507 0 0 0 1811 186 0 0 25 0 1 0 905377859 60477440 11448 4294967295 134512640 134716908 3221224544 3221223400 1076602885 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 14765 11448 1111 63 0 14702 0
vsize: 59060
[startup+30.0027 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 304910 0 0 0 2435 561 0 0 25 0 1 0 905377859 71565312 14079 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17472 14079 1111 63 0 17409 0
vsize: 69888
[startup+40.0035 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 528087 0 0 0 3047 950 0 0 25 0 1 0 905377859 80809984 16352 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19729 16352 1111 63 0 19666 0
vsize: 78916
[startup+50.0041 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 755537 0 0 0 3654 1343 0 0 25 0 1 0 905377859 89026560 18394 4294967295 134512640 134716908 3221224544 3221221420 1077253896 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21783 18399 1111 63 0 21720 0
vsize: 86940
[startup+60.0048 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 977731 0 0 0 4249 1749 0 0 25 0 1 0 905377859 96698368 20232 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 23608 20239 1111 63 0 23545 0
vsize: 94432
[startup+70.0045 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 1198702 0 0 0 4851 2147 0 0 25 0 1 0 905377859 104288256 22131 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 25461 22136 1111 63 0 25398 0
vsize: 101844
[startup+80.0053 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 1415956 0 0 0 5454 2543 0 0 25 0 1 0 905377859 110665728 23679 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 27018 23686 1111 63 0 26955 0
vsize: 108072
[startup+90.0051 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 1629465 0 0 0 6058 2939 0 0 25 0 1 0 905377859 116375552 25088 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 28412 25094 1111 63 0 28349 0
vsize: 113648
[startup+100.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 1841674 0 0 0 6665 3332 0 0 25 0 1 0 905377859 122720256 26413 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 29961 26419 1111 63 0 29898 0
vsize: 119844
[startup+110.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 2051635 0 0 0 7274 3724 0 0 25 0 1 0 905377859 127885312 27721 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 31222 27726 1111 63 0 31159 0
vsize: 124888
[startup+120.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 2258348 0 0 0 7890 4108 0 0 25 0 1 0 905377859 132775936 28936 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 32416 28942 1111 63 0 32353 0
vsize: 129664
[startup+130.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 2434672 0 0 0 8557 4441 0 0 25 0 1 0 905377859 140595200 30889 4294967295 134512640 134716908 3221224544 3221221308 1077191450 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 34325 30889 1111 63 0 34262 0
vsize: 137300
[startup+140.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 2559474 0 0 0 9264 4734 0 0 25 0 1 0 905377859 366723072 87964 4294967295 134512640 134716908 3221224544 3221223184 134606504 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 89532 87971 1111 63 0 89469 0
vsize: 358128
[startup+150.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 2743333 0 0 0 9821 5178 0 0 25 0 1 0 905377859 390955008 93848 4294967295 134512640 134716908 3221224544 3221223184 134606504 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 95448 93854 1111 63 0 95385 0
vsize: 381792
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 2844981 0 0 0 10579 5419 0 0 25 0 1 0 905377859 339345408 81421 4294967295 134512640 134716908 3221224544 3221223184 134594970 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 82848 81421 1111 63 0 82785 0
vsize: 331392
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 2881008 0 0 0 11498 5501 0 0 25 0 1 0 905377859 339480576 81448 4294967295 134512640 134716908 3221224544 3221223024 134536638 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 82881 81448 1111 63 0 82818 0
vsize: 331524
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 2973957 0 0 0 12276 5722 0 0 25 0 1 0 905377859 380166144 91372 4294967295 134512640 134716908 3221224544 3221223096 134542829 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 92814 91372 1111 63 0 92751 0
vsize: 371256
[startup+190.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 3079404 0 0 0 13037 5962 0 0 25 0 1 0 905377859 717606912 173644 4294967295 134512640 134716908 3221224544 3221223072 134554866 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 175197 173650 1111 63 0 175134 0
vsize: 700788
[startup+193.164 s]
Raw data (loadavg): 0.99 0.96 0.91 1/53 23707
Raw data (stat): 23707 (bsolo_lpr_cuts-) R 23706 7266 7265 0 -1 0 3079404 0 0 0 13037 5962 0 0 25 0 1 0 905377859 717606912 173644 4294967295 134512640 134716908 3221224544 3221223072 134554866 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 175197 173650 1111 63 0 175134 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 193.164
CPU time (s): 193.053
CPU user time (s): 131.336
CPU system time (s): 61.7166
CPU usage (%): 99.9423
Max. virtual memory (Kb): 700788
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####