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/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-blp-ar98.opb
MD5SUM	181a05258ae35e5f3b5b834240f1847a
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
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	31
Biggest coefficient in the objective function	1073741824
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	2147483647
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	83886080000000
Number of bits of the biggest number in a constraint	47
Biggest sum of numbers in a constraint	572975239517507
Number of bits of the biggest sum of numbers	50
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.23881
Number of variables	20024
Total number of constraints	17064
Number of constraints which are clauses	1
Number of constraints which are cardinality constraints (but not clauses)	16718
Number of constraints which are nor clauses,nor cardinality constraints	345
Minimum length of a constraint	1
Maximum length of a constraint	15837

Trace number 20367

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-21 20:59:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14961 boxname=wulflinc6 idbench=1151 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  181a05258ae35e5f3b5b834240f1847a  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-blp-ar98.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-blp-ar98.opb /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-blp-ar98.opb
IDLAUNCH: 14961
/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:        257164 kB
Buffers:         28728 kB
Cached:         726916 kB
SwapCached:        516 kB
Active:          95220 kB
Inactive:       662424 kB
HighTotal:      131008 kB
HighFree:          308 kB
LowTotal:       903652 kB
LowFree:        256856 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            14220 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 21:04:33 (client local time) WITH STATUS 1 IN 310.129 SECONDS
stats: 14961 7 310.129 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
PARSE ERROR! [line 32096] Integer overflow. Big numbers not supported yet.
#### 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.90 0.93 0.90 2/54 26349
Raw data (stat): 26349 (runsolver) R 26348 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489925103 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.001 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 26349
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 580 0 0 0 997 2 0 0 25 0 1 0 489925103 4153344 558 4294967295 134512640 134672761 3221224544 3221223836 1075372044 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1014 558 603 41 0 973 0
vsize: 4056
[startup+20.0011 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 26349
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 743 0 0 0 1996 3 0 0 25 0 1 0 489925103 5345280 721 4294967295 134512640 134672761 3221224544 3221223852 1075372060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1305 721 603 41 0 1264 0
vsize: 5220
[startup+30.0012 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 26349
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 833 0 0 0 2996 3 0 0 25 0 1 0 489925103 5517312 811 4294967295 134512640 134672761 3221224544 3221223836 1075372060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1347 811 603 41 0 1306 0
vsize: 5388
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 26349
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 866 0 0 0 3996 4 0 0 25 0 1 0 489925103 5517312 844 4294967295 134512640 134672761 3221224544 3221223872 134586555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1347 844 603 41 0 1306 0
vsize: 5388
[startup+50.0121 s]
Raw data (loadavg): 1.03 0.96 0.91 2/54 26402
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 927 0 0 0 4977 12 0 0 25 0 1 0 489925103 5517312 905 4294967295 134512640 134672761 3221224544 3221223836 1075372055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1347 905 603 41 0 1306 0
vsize: 5388
[startup+60.1148 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 26402
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 972 0 0 0 5987 13 0 0 25 0 1 0 489925103 5648384 950 4294967295 134512640 134672761 3221224544 3221223856 134586646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1379 950 603 41 0 1338 0
vsize: 5516
[startup+70.1147 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 26402
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1198 0 0 0 6987 13 0 0 25 0 1 0 489925103 8015872 1176 4294967295 134512640 134672761 3221224544 3221223856 134586646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1957 1176 603 41 0 1916 0
vsize: 7828
[startup+80.1166 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 26402
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1220 0 0 0 7987 13 0 0 25 0 1 0 489925103 8019968 1198 4294967295 134512640 134672761 3221224544 3221223872 134586518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1958 1198 603 41 0 1917 0
vsize: 7832
[startup+90.117 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 26402
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1240 0 0 0 8987 14 0 0 25 0 1 0 489925103 8019968 1218 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1958 1218 603 41 0 1917 0
vsize: 7832
[startup+100.117 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 26402
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1285 0 0 0 9985 15 0 0 25 0 1 0 489925103 8372224 1263 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2044 1263 603 41 0 2003 0
vsize: 8176
[startup+110.118 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 26402
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1329 0 0 0 10986 15 0 0 25 0 1 0 489925103 8462336 1307 4294967295 134512640 134672761 3221224544 3221223852 1075372044 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2066 1307 603 41 0 2025 0
vsize: 8264
[startup+120.118 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1377 0 0 0 11986 15 0 0 25 0 1 0 489925103 8646656 1355 4294967295 134512640 134672761 3221224544 3221223696 134580257 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2111 1355 603 41 0 2070 0
vsize: 8444
[startup+130.118 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1398 0 0 0 12986 15 0 0 25 0 1 0 489925103 8781824 1376 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2144 1376 603 41 0 2103 0
vsize: 8576
[startup+140.118 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1480 0 0 0 13986 16 0 0 25 0 1 0 489925103 9023488 1444 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1444 603 41 0 2162 0
vsize: 8812
[startup+150.119 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1538 0 0 0 14986 16 0 0 25 0 1 0 489925103 9228288 1491 4294967295 134512640 134672761 3221224544 3221223852 1075372068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2253 1491 603 41 0 2212 0
vsize: 9012
[startup+160.119 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1586 0 0 0 15986 16 0 0 25 0 1 0 489925103 9498624 1539 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2319 1539 603 41 0 2278 0
vsize: 9276
[startup+170.119 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1633 0 0 0 16986 16 0 0 25 0 1 0 489925103 9682944 1586 4294967295 134512640 134672761 3221224544 3221223872 134586518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2364 1586 603 41 0 2323 0
vsize: 9456
[startup+180.121 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1687 0 0 0 17986 17 0 0 25 0 1 0 489925103 9916416 1640 4294967295 134512640 134672761 3221224544 3221223872 134586555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2421 1640 603 41 0 2380 0
vsize: 9684
[startup+190.12 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1754 0 0 0 18986 17 0 0 25 0 1 0 489925103 10252288 1707 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2503 1707 603 41 0 2462 0
vsize: 10012
[startup+200.121 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1796 0 0 0 19986 18 0 0 25 0 1 0 489925103 10354688 1749 4294967295 134512640 134672761 3221224544 3221223872 134586518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2528 1749 603 41 0 2487 0
vsize: 10112
[startup+210.122 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1879 0 0 0 20985 19 0 0 25 0 1 0 489925103 10756096 1832 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2626 1832 603 41 0 2585 0
vsize: 10504
[startup+220.122 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 1989 0 0 0 21985 19 0 0 25 0 1 0 489925103 11169792 1936 4294967295 134512640 134672761 3221224544 3221223852 1075372032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2727 1936 603 41 0 2686 0
vsize: 10908
[startup+230.122 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 2086 0 0 0 22985 20 0 0 25 0 1 0 489925103 11550720 2027 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2820 2027 603 41 0 2779 0
vsize: 11280
[startup+240.123 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 2122 0 0 0 23985 20 0 0 25 0 1 0 489925103 11837440 2063 4294967295 134512640 134672761 3221224544 3221223852 1075372032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2890 2063 603 41 0 2849 0
vsize: 11560
[startup+250.123 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 2217 0 0 0 24984 21 0 0 25 0 1 0 489925103 12337152 2158 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3012 2158 603 41 0 2971 0
vsize: 12048
[startup+260.124 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 2258 0 0 0 25984 21 0 0 25 0 1 0 489925103 12472320 2199 4294967295 134512640 134672761 3221224544 3221223852 1075372032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3045 2199 603 41 0 3004 0
vsize: 12180
[startup+270.124 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 2320 0 0 0 26984 22 0 0 25 0 1 0 489925103 12812288 2261 4294967295 134512640 134672761 3221224544 3221223856 134586537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3128 2261 603 41 0 3087 0
vsize: 12512
[startup+280.124 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 2377 0 0 0 27984 22 0 0 25 0 1 0 489925103 13029376 2318 4294967295 134512640 134672761 3221224544 3221223872 134586545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3181 2318 603 41 0 3140 0
vsize: 12724
[startup+290.124 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 2454 0 0 0 28983 22 0 0 25 0 1 0 489925103 13373440 2395 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3265 2395 603 41 0 3224 0
vsize: 13060
[startup+300.124 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 2513 0 0 0 29983 23 0 0 25 0 1 0 489925103 13611008 2454 4294967295 134512640 134672761 3221224544 3221223852 134516148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3323 2454 603 41 0 3282 0
vsize: 13292
[startup+310.124 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 2598 0 0 0 30983 23 0 0 25 0 1 0 489925103 13975552 2538 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3412 2538 603 41 0 3371 0
vsize: 13648
[startup+310.189 s]
Raw data (loadavg): 1.00 0.97 0.91 1/53 26404
Raw data (stat): 26349 (minisat+) R 26348 29653 29652 0 -1 0 2598 0 0 0 30983 23 0 0 25 0 1 0 489925103 13975552 2538 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3412 2538 603 41 0 3371 0
vsize: 0

Child status: 1
Real time (s): 310.188
CPU time (s): 310.129
CPU user time (s): 309.887
CPU system time (s): 0.241963
CPU usage (%): 99.9808
Max. virtual memory (Kb): 13648
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####