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-full.all.ucl.opb
MD5SUM	b8424149645ffb0af409a9e7aef74685
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable
(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	68
Number of bits of the biggest number in a constraint	7
Biggest sum of numbers in a constraint	257
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	81558
Total number of constraints	240469
Number of constraints which are clauses	235865
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	4604
Minimum length of a constraint	1
Maximum length of a constraint	13

Trace number 39653

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-06-07 15:45:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=27713 boxname=wulflinc6 idbench=271 idsolver=20 numberseed=0
MD5SUM SOLVER: f6aa7fb267fa9710116626be7e6d3048  /oldhome/oroussel/solvers/bsolo_lpr-v2
MD5SUM BENCH:  b8424149645ffb0af409a9e7aef74685  /oldhome/oroussel/tmp/wulflinc6/normalized-cache-ibm-q-full.all.ucl.opb
REAL COMMAND:  bsolo_lpr-v2 /oldhome/oroussel/tmp/wulflinc6/normalized-cache-ibm-q-full.all.ucl.opb
IDLAUNCH: 27713
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        818156 kB
Buffers:         33880 kB
Cached:         159920 kB
SwapCached:       1020 kB
Active:          55676 kB
Inactive:       140256 kB
HighTotal:      131008 kB
HighFree:        77504 kB
LowTotal:       903652 kB
LowFree:        740652 kB
SwapTotal:     2097136 kB
SwapFree:      2095192 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5036 kB
Slab:            14784 kB
Committed_AS:    63736 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-07 15:50:45 (client local time) WITH STATUS 0 IN 292.546 SECONDS
stats: 27713 7 292.546 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 81558 variables and 240469 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.92 0.95 0.93 2/54 15850
Raw data (stat): 15850 (runsolver) R 15849 25568 25567 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 894178087 884736 94 4294967295 134512640 135332820 3221224448 3221219628 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.0004 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 15693 0 0 0 955 42 0 0 25 0 1 0 894178087 47595520 8287 4294967295 134512640 134716908 3221224560 3221221324 1077195911 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11620 8287 1111 63 0 11557 0
vsize: 46480
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 94650 0 0 0 1809 188 0 0 25 0 1 0 894178087 67006464 13047 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16359 13047 1111 63 0 16296 0
vsize: 65436
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 318087 0 0 0 2411 587 0 0 25 0 1 0 894178087 78393344 15758 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 19139 15758 1111 63 0 19076 0
vsize: 76556
[startup+40.0026 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 546043 0 0 0 3006 992 0 0 25 0 1 0 894178087 87445504 18013 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21349 18013 1111 63 0 21286 0
vsize: 85396
[startup+50.0033 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 772493 0 0 0 3607 1391 0 0 25 0 1 0 894178087 95776768 20052 4294967295 134512640 134716908 3221224560 3221222864 134568040 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 23383 20052 1111 63 0 23320 0
vsize: 93532
[startup+60.0041 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 992744 0 0 0 4201 1797 0 0 25 0 1 0 894178087 103985152 22038 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 25387 22038 1111 63 0 25324 0
vsize: 101548
[startup+70.0042 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 1209171 0 0 0 4800 2198 0 0 25 0 1 0 894178087 110641152 23667 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 27012 23667 1111 63 0 26949 0
vsize: 108048
[startup+80.0054 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 1421262 0 0 0 5409 2590 0 0 25 0 1 0 894178087 116621312 25131 4294967295 134512640 134716908 3221224560 3221222864 134568044 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 28472 25131 1111 63 0 28409 0
vsize: 113888
[startup+90.0055 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 1631906 0 0 0 6012 2987 0 0 25 0 1 0 894178087 122466304 26527 4294967295 134512640 134716908 3221224560 3221222584 1077799011 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29899 26527 1111 63 0 29836 0
vsize: 119596
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 1824255 0 0 0 6635 3364 0 0 25 0 1 0 894178087 128110592 27816 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 31277 27816 1111 63 0 31214 0
vsize: 125108
[startup+110.007 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 2029133 0 0 0 7248 3751 0 0 25 0 1 0 894178087 133271552 29048 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 32537 29048 1111 63 0 32474 0
vsize: 130148
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 2231686 0 0 0 7862 4137 0 0 25 0 1 0 894178087 138027008 30253 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 33626 30184 1111 63 0 33563 0
vsize: 134792
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 2434639 0 0 0 8470 4530 0 0 25 0 1 0 894178087 142786560 31342 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 34860 31348 1111 63 0 34797 0
vsize: 139440
[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 2632157 0 0 0 9083 4918 0 0 25 0 1 0 894178087 147128320 32465 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 35920 32471 1111 63 0 35857 0
vsize: 143680
[startup+150.116 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 2832448 0 0 0 9691 5320 0 0 25 0 1 0 894178087 151343104 33470 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 36949 33475 1111 63 0 36886 0
vsize: 147796
[startup+160.116 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 2972077 0 0 0 10367 5644 0 0 25 0 1 0 894178087 281694208 67257 4294967295 134512640 134716908 3221224560 3221223200 134606504 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 68773 67263 1111 63 0 68710 0
vsize: 275092
[startup+170.117 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 3174256 0 0 0 10883 6129 0 0 25 0 1 0 894178087 554979328 133836 4294967295 134512640 134716908 3221224560 3221223200 134606504 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 135493 133842 1111 63 0 135430 0
vsize: 541972
[startup+180.117 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 3334548 0 0 0 11488 6524 0 0 25 0 1 0 894178087 501895168 121088 4294967295 134512640 134716908 3221224560 3221222944 134542303 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 122533 121088 1111 63 0 122470 0
vsize: 490132
[startup+190.118 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 3465113 0 0 0 12167 6846 0 0 25 0 1 0 894178087 525619200 126853 4294967295 134512640 134716908 3221224560 3221223188 134594953 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 128325 126853 1111 63 0 128262 0
vsize: 513300
[startup+200.118 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 3580329 0 0 0 12883 7129 0 0 25 0 1 0 894178087 502026240 121109 4294967295 134512640 134716908 3221224560 3221222992 134523171 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 122565 121109 1111 63 0 122502 0
vsize: 490260
[startup+210.118 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 3675134 0 0 0 13653 7360 0 0 25 0 1 0 894178087 508907520 122794 4294967295 134512640 134716908 3221224560 3221223164 134543540 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 124245 122794 1111 63 0 124182 0
vsize: 496980
[startup+220.119 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 3796340 0 0 0 14366 7648 0 0 25 0 1 0 894178087 516771840 124720 4294967295 134512640 134716908 3221224560 3221223164 134543553 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 126165 124720 1111 63 0 126102 0
vsize: 504660
[startup+230.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 3917065 0 0 0 15070 7944 0 0 25 0 1 0 894178087 502157312 121125 4294967295 134512640 134716908 3221224560 3221223312 134630838 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 122597 121125 1111 63 0 122534 0
vsize: 490388
[startup+240.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 4051956 0 0 0 15743 8271 0 0 25 0 1 0 894178087 502157312 121136 4294967295 134512640 134716908 3221224560 3221222944 134542701 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 122597 121136 1111 63 0 122534 0
vsize: 490388
[startup+250.122 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 4175085 0 0 0 16445 8570 0 0 25 0 1 0 894178087 502157312 121145 4294967295 134512640 134716908 3221224560 3221222968 134543600 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 122597 121145 1111 63 0 122534 0
vsize: 490388
[startup+260.125 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 4277501 0 0 0 17197 8819 0 0 25 0 1 0 894178087 503140352 121321 4294967295 134512640 134716908 3221224560 3221223200 134606504 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 122837 121328 1111 63 0 122774 0
vsize: 491348
[startup+270.125 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 4391936 0 0 0 17924 9092 0 0 25 0 1 0 894178087 520970240 125596 4294967295 134512640 134716908 3221224560 3221223200 134606495 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 127190 125603 1111 63 0 127127 0
vsize: 508760
[startup+280.125 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 4519641 0 0 0 18616 9400 0 0 25 0 1 0 894178087 647782400 156581 4294967295 134512640 134716908 3221224560 3221223200 134606504 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 158150 156588 1111 63 0 158087 0
vsize: 632600
[startup+290.127 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 4736096 0 0 0 19089 9928 0 0 25 0 1 0 894178087 756051968 182956 4294967295 134512640 134716908 3221224560 3221223200 134606484 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 184583 182964 1111 63 0 184520 0
vsize: 738332
[startup+292.537 s]
Raw data (loadavg): 0.99 0.97 0.93 1/53 15850
Raw data (stat): 15850 (bsolo_lpr-v2) R 15849 25568 25567 0 -1 0 4736096 0 0 0 19089 9928 0 0 25 0 1 0 894178087 756051968 182956 4294967295 134512640 134716908 3221224560 3221223200 134606484 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 184583 182964 1111 63 0 184520 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 292.537
CPU time (s): 292.546
CPU user time (s): 191.607
CPU system time (s): 100.939
CPU usage (%): 100.003
Max. virtual memory (Kb): 738332
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####