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-ooo.unbounded.all.ucl.opb
MD5SUM	e8f0ca38acbe8c57203147fb9147be3a
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	129
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	510
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	487.167
Number of variables	84836
Total number of constraints	245062
Number of constraints which are clauses	233598
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	11464
Minimum length of a constraint	1
Maximum length of a constraint	15

Trace number 24658

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-11 16:26:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2729 boxname=wulflinc31 idbench=304 idsolver=2 numberseed=0
MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7  /oldhome/oroussel/solvers/bsolo_lpr_cuts
MD5SUM BENCH:  e8f0ca38acbe8c57203147fb9147be3a  /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.unbounded.all.ucl.opb
REAL COMMAND:  bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.unbounded.all.ucl.opb
IDLAUNCH: 2729
/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:        919000 kB
Buffers:          3016 kB
Cached:          90752 kB
SwapCached:       1908 kB
Active:          68256 kB
Inactive:        28716 kB
HighTotal:      131008 kB
HighFree:        39424 kB
LowTotal:       903652 kB
LowFree:        879576 kB
SwapTotal:     2097892 kB
SwapFree:      2095160 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5364 kB
Slab:            12780 kB
Committed_AS:    63860 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-11 16:30:02 (client local time) WITH STATUS 0 IN 232.872 SECONDS
stats: 2729 7 232.872 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 84836 variables and 245062 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.97 0.99 2/55 31646
Raw data (stat): 31646 (runsolver) R 31645 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 719313329 1056768 100 4294967295 134512640 135381576 3221221664 3221216880 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 21435 0 0 0 945 50 0 0 25 0 1 0 719313329 44015616 7444 4294967295 134512640 134714508 3221221776 3221220020 1077313968 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 10746 7444 1111 63 0 10683 0
vsize: 42984
[startup+20.001 s]
Raw data (loadavg): 0.94 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 108296 0 0 0 1788 207 0 0 25 0 1 0 719313329 61571072 11735 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 15032 11742 1111 63 0 14969 0
vsize: 60128
[startup+30.001 s]
Raw data (loadavg): 0.95 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 328731 0 0 0 2396 599 0 0 25 0 1 0 719313329 72544256 14336 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17711 14343 1111 63 0 17648 0
vsize: 70844
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 548893 0 0 0 3006 990 0 0 25 0 1 0 719313329 81510400 16578 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 19856 16536 1111 63 0 19793 0
vsize: 79600
[startup+50.0018 s]
Raw data (loadavg): 0.96 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 769081 0 0 0 3612 1384 0 0 25 0 1 0 719313329 89325568 18497 4294967295 134512640 134714508 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 21841 18498 1111 63 0 21778 0
vsize: 87232
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 985189 0 0 0 4228 1768 0 0 25 0 1 0 719313329 96727040 20295 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 23615 20301 1111 63 0 23552 0
vsize: 94460
[startup+70.0027 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 1203421 0 0 0 4822 2174 0 0 25 0 1 0 719313329 104161280 22128 4294967295 134512640 134714508 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 25430 22128 1111 63 0 25367 0
vsize: 101720
[startup+80.0036 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 1414781 0 0 0 5425 2571 0 0 25 0 1 0 719313329 110505984 23650 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 26979 23655 1111 63 0 26916 0
vsize: 107916
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 1623884 0 0 0 6039 2957 0 0 25 0 1 0 719313329 116342784 25061 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 28404 25067 1111 63 0 28341 0
vsize: 113616
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 1833233 0 0 0 6641 3356 0 0 25 0 1 0 719313329 122544128 26403 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 29918 26408 1111 63 0 29855 0
vsize: 119672
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 2040282 0 0 0 7249 3748 0 0 25 0 1 0 719313329 127840256 27696 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 31211 27702 1111 63 0 31148 0
vsize: 124844
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 2242138 0 0 0 7861 4136 0 0 25 0 1 0 719313329 132726784 28930 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 32332 28861 1111 63 0 32269 0
vsize: 129616
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 2444847 0 0 0 8471 4527 0 0 25 0 1 0 719313329 137039872 30006 4294967295 134512640 134714508 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 33457 30006 1111 63 0 33394 0
vsize: 133828
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 2647574 0 0 0 9086 4911 0 0 25 0 1 0 719313329 141832192 31136 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 34627 31141 1111 63 0 34564 0
vsize: 138508
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 2846120 0 0 0 9706 5292 0 0 25 0 1 0 719313329 146173952 32224 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 35687 32229 1111 63 0 35624 0
vsize: 142748
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 3044237 0 0 0 10317 5681 0 0 25 0 1 0 719313329 150245376 33187 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 36681 33192 1111 63 0 36618 0
vsize: 146724
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 3138255 0 0 0 11130 5868 0 0 25 0 1 0 719313329 177938432 41955 4294967295 134512640 134714508 3221221776 3221220584 1077378037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 43442 41959 1111 63 0 43379 0
vsize: 173768
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 3308213 0 0 0 11731 6268 0 0 25 0 1 0 719313329 321167360 76955 4294967295 134512640 134714508 3221221776 3221220520 134630805 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 78410 76955 1111 63 0 78347 0
vsize: 313640
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 3520662 0 0 0 12216 6782 0 0 25 0 1 0 719313329 598716416 144486 4294967295 134512640 134714508 3221221776 3221220416 134606468 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 146171 144493 1111 63 0 146108 0
vsize: 584684
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 3653379 0 0 0 12882 7116 0 0 25 0 1 0 719313329 464224256 111867 4294967295 134512640 134714508 3221221776 3221220240 134542300 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 113336 111867 1111 63 0 113273 0
vsize: 453344
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 3777387 0 0 0 13588 7411 0 0 25 0 1 0 719313329 445865984 107391 4294967295 134512640 134714508 3221221776 3221220528 134630792 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 108854 107391 1111 63 0 108791 0
vsize: 435416
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 3892845 0 0 0 14311 7688 0 0 25 0 1 0 719313329 457084928 110052 4294967295 134512640 134714508 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 111593 110058 1111 63 0 111530 0
vsize: 446372
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 4076520 0 0 0 14865 8135 0 0 25 0 1 0 719313329 683638784 165243 4294967295 134512640 134714508 3221221776 3221220416 134606479 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 166904 165250 1111 63 0 166841 0
vsize: 667616
[startup+232.887 s]
Raw data (loadavg): 0.99 0.97 0.99 1/54 31646
Raw data (stat): 31646 (bsolo_lpr_cuts) R 31645 7876 7672 0 -1 0 4076520 0 0 0 14865 8135 0 0 25 0 1 0 719313329 683638784 165243 4294967295 134512640 134714508 3221221776 3221220416 134606479 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 166904 165250 1111 63 0 166841 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 232.887
CPU time (s): 232.872
CPU user time (s): 149.607
CPU system time (s): 83.2643
CPU usage (%): 99.9935
Max. virtual memory (Kb): 667616
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####