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-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-momentum1.opb
MD5SUM	acfea3028edc6266e2157b2d64da7531
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	23392
Biggest coefficient in the objective function	2048000000
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	171547966775
Number of bits of the sum of numbers in the objective function	38
Biggest number in a constraint	524288000000000000000
Number of bits of the biggest number in a constraint	69
Biggest sum of numbers in a constraint	1054942508296556904448
Number of bits of the biggest sum of numbers	70
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.276957
Number of variables	31067
Total number of constraints	47575
Number of constraints which are clauses	24365
Number of constraints which are cardinality constraints (but not clauses)	3166
Number of constraints which are nor clauses,nor cardinality constraints	20044
Minimum length of a constraint	1
Maximum length of a constraint	668

Trace number 29953

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-05-25 13:22:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21377 boxname=wulflinc15 idbench=1365 idsolver=14 numberseed=0
MD5SUM SOLVER: d29da23ec752be69e0579424c0f0767e  /oldhome/oroussel/solvers/sat4jPseudoBis.jar
MD5SUM BENCH:  acfea3028edc6266e2157b2d64da7531  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-momentum1.opb
REAL COMMAND:  java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudoBis.jar /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-momentum1.opb
IDLAUNCH: 21377
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        675664 kB
Buffers:         33728 kB
Cached:         303084 kB
SwapCached:        672 kB
Active:          73792 kB
Inactive:       265096 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        675412 kB
SwapTotal:     2097136 kB
SwapFree:      2095624 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5076 kB
Slab:            14492 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 13:27:34 (client local time) WITH STATUS 20 IN 297.057 SECONDS
stats: 21377 7 297.057 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c SAT4J: a SATisfiability library for Java (c) 2004-2005 Daniel Le Berre
c This is free software under the GNU LGPL licence. See www.sat4j.org for details.
c version Special PB05 Second trial
c --- Begin Solver configuration ---
c org.sat4j.minisat.uip.FirstUIP@1e4cbc4
c org.sat4j.minisat.constraints.PBMinDataStructure@1fdc96c
c org.sat4j.minisat.learning.MiniSATLearning@b2fd8f
c conflictBoundIncFactor=1.5 learntBoundIncFactor=1.1 initLearntBoundConstraintFactor=0.5 initConflictBound=100 
c 
c --- End Solver configuration ---
c solving /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-momentum1.opb
c reading problem ... c (trivial inconsistency)
c starts	: 0
c conflicts	: 0
c decisions	: 0
c propagations	: 0
c inspects	: 0
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 0
s UNSATISFIABLE
c Total CPU time (ms) : 290.546
#### 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): 1.01 1.00 1.00 2/54 8409
Raw data (stat): 8409 (runsolver) R 8408 23514 23513 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 780978677 1052672 99 4294967295 134512640 135381576 3221224400 3221219620 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.0035 s]
Raw data (loadavg): 1.23 1.05 1.02 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18013 0 1 0 871 39 0 0 24 0 10 0 780978677 853635072 19368 4294967295 134512640 134569956 3221224368 3221214344 1079276148 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208407 19368 13086 16 0 208391 0
vsize: 833628
[startup+20.0067 s]
Raw data (loadavg): 1.19 1.05 1.01 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 1767 39 0 0 24 0 10 0 780978677 854061056 19925 4294967295 134512640 134569956 3221224368 3221213672 1073952732 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208511 19925 13086 16 0 208495 0
vsize: 834044
[startup+30.0072 s]
Raw data (loadavg): 1.16 1.04 1.01 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 2667 39 0 0 25 0 10 0 780978677 853635072 20309 4294967295 134512640 134569956 3221224368 3221214464 1077558376 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208407 20309 13086 16 0 208391 0
vsize: 833628
[startup+40.008 s]
Raw data (loadavg): 1.14 1.04 1.01 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 3583 40 0 0 25 0 10 0 780978677 854683648 20892 4294967295 134512640 134569956 3221224368 3221214768 1131234951 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208663 20892 13086 16 0 208647 0
vsize: 834652
[startup+50.0087 s]
Raw data (loadavg): 1.11 1.04 1.01 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 4504 40 0 0 25 0 10 0 780978677 854683648 21054 4294967295 134512640 134569956 3221224368 3221214768 1131234951 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208663 21054 13086 16 0 208647 0
vsize: 834652
[startup+60.0087 s]
Raw data (loadavg): 1.10 1.04 1.01 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 5420 41 0 0 25 0 10 0 780978677 854683648 21188 4294967295 134512640 134569956 3221224368 3221214756 1080204031 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208663 21188 13086 16 0 208647 0
vsize: 834652
[startup+70.0091 s]
Raw data (loadavg): 1.08 1.04 1.01 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 6352 41 0 0 25 0 10 0 780978677 854683648 21305 4294967295 134512640 134569956 3221224368 3221214764 1080204163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208663 21305 13086 16 0 208647 0
vsize: 834652
[startup+80.0104 s]
Raw data (loadavg): 1.07 1.04 1.01 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 7291 41 0 0 25 0 10 0 780978677 854683648 21409 4294967295 134512640 134569956 3221224368 3221214200 1077558376 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208663 21409 13086 16 0 208647 0
vsize: 834652
[startup+90.0102 s]
Raw data (loadavg): 1.06 1.03 1.01 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 8234 42 0 0 25 0 10 0 780978677 854683648 21498 4294967295 134512640 134569956 3221224368 3221214740 1080204031 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208663 21498 13086 16 0 208647 0
vsize: 834652
[startup+100.011 s]
Raw data (loadavg): 1.05 1.03 1.01 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 9174 42 0 0 25 0 10 0 780978677 854683648 21586 4294967295 134512640 134569956 3221224368 3221214644 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208663 21586 13086 16 0 208647 0
vsize: 834652
[startup+110.012 s]
Raw data (loadavg): 1.04 1.03 1.01 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 10115 43 0 0 24 0 10 0 780978677 854683648 21668 4294967295 134512640 134569956 3221224368 3221214216 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208663 21668 13086 16 0 208647 0
vsize: 834652
[startup+120.013 s]
Raw data (loadavg): 1.03 1.03 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 11061 43 0 0 25 0 10 0 780978677 854683648 21741 4294967295 134512640 134569956 3221224368 3221214644 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208663 21741 13086 16 0 208647 0
vsize: 834652
[startup+130.014 s]
Raw data (loadavg): 1.03 1.03 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 12003 44 0 0 25 0 10 0 780978677 854683648 21814 4294967295 134512640 134569956 3221224368 3221214644 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208663 21814 13086 16 0 208647 0
vsize: 834652
[startup+140.017 s]
Raw data (loadavg): 1.02 1.03 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 12949 44 0 0 25 0 10 0 780978677 854683648 21880 4294967295 134512640 134569956 3221224368 3221214748 1080204163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208663 21880 13086 16 0 208647 0
vsize: 834652
[startup+150.021 s]
Raw data (loadavg): 1.02 1.03 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18014 0 1 0 13891 44 0 0 25 0 10 0 780978677 854683648 21947 4294967295 134512640 134569956 3221224368 3221214644 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208663 21947 13086 16 0 208647 0
vsize: 834652
[startup+160.022 s]
Raw data (loadavg): 1.02 1.02 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18027 0 1 0 14730 46 0 0 25 0 10 0 780978677 856113152 22398 4294967295 134512640 134569956 3221224368 3221214264 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209012 22398 13086 16 0 208996 0
vsize: 836048
[startup+170.022 s]
Raw data (loadavg): 1.01 1.02 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18027 0 1 0 15597 46 0 0 25 0 10 0 780978677 856113152 22454 4294967295 134512640 134569956 3221224368 3221214692 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209012 22454 13086 16 0 208996 0
vsize: 836048
[startup+180.023 s]
Raw data (loadavg): 1.01 1.02 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18027 0 1 0 16490 47 0 0 25 0 10 0 780978677 856113152 23133 4294967295 134512640 134569956 3221224368 3221214248 1077558376 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209012 23133 13086 16 0 208996 0
vsize: 836048
[startup+190.024 s]
Raw data (loadavg): 1.01 1.02 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18030 0 1 0 17405 48 0 0 25 0 10 0 780978677 856113152 23862 4294967295 134512640 134569956 3221224368 3221214248 1080019600 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209012 23862 13086 16 0 208996 0
vsize: 836048
[startup+200.024 s]
Raw data (loadavg): 1.01 1.02 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18030 0 1 0 18302 49 0 0 24 0 10 0 780978677 855064576 26405 4294967295 134512640 134569956 3221224368 3221214780 1080204163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208756 26405 13086 16 0 208740 0
vsize: 835024
[startup+210.025 s]
Raw data (loadavg): 1.00 1.02 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18030 0 1 0 19203 50 0 0 25 0 10 0 780978677 855064576 26405 4294967295 134512640 134569956 3221224368 3221214676 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208756 26405 13086 16 0 208740 0
vsize: 835024
[startup+220.025 s]
Raw data (loadavg): 1.00 1.02 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18030 0 1 0 20063 51 0 0 25 0 10 0 780978677 855064576 27084 4294967295 134512640 134569956 3221224368 3221214744 1131154751 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208756 27084 13086 16 0 208740 0
vsize: 835024
[startup+230.026 s]
Raw data (loadavg): 1.00 1.02 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18031 0 1 0 20919 54 0 0 25 0 10 0 780978677 855064576 31086 4294967295 134512640 134569956 3221224368 3221214780 1080204163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208756 31086 13086 16 0 208740 0
vsize: 835024
[startup+240.026 s]
Raw data (loadavg): 1.00 1.02 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18031 0 1 0 21848 54 0 0 25 0 10 0 780978677 855064576 31086 4294967295 134512640 134569956 3221224368 3221214248 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208756 31086 13086 16 0 208740 0
vsize: 835024
[startup+250.027 s]
Raw data (loadavg): 1.00 1.02 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18031 0 1 0 22736 55 0 0 25 0 10 0 780978677 855064576 31123 4294967295 134512640 134569956 3221224368 3221214772 1080204031 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208756 31123 13086 16 0 208740 0
vsize: 835024
[startup+260.027 s]
Raw data (loadavg): 1.00 1.01 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18031 0 1 0 23616 55 0 0 20 0 10 0 780978677 855064576 31353 4294967295 134512640 134569956 3221224368 3221214844 1080204340 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208756 31353 13086 16 0 208740 0
vsize: 835024
[startup+270.027 s]
Raw data (loadavg): 1.00 1.01 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18031 0 1 0 24496 55 0 0 18 0 10 0 780978677 855064576 31592 4294967295 134512640 134569956 3221224368 3221214776 1079677873 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208756 31592 13086 16 0 208740 0
vsize: 835024
[startup+280.028 s]
Raw data (loadavg): 1.00 1.01 1.00 2/63 8418
Raw data (stat): 8409 (java) S 8408 23514 23513 0 -1 0 18031 0 1 0 25386 56 0 0 23 0 10 0 780978677 855064576 31803 4294967295 134512640 134569956 3221224368 3221213488 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208756 31803 13086 16 0 208740 0
vsize: 835024
[startup+290.029 s]
Raw data (loadavg): 1.00 1.01 1.00 2/63 8418
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18031 0 1 0 26279 57 0 0 21 0 10 0 780978677 855064576 31991 4294967295 134512640 134569956 3221224368 3221214772 1080204031 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208756 31991 13086 16 0 208740 0
vsize: 835024
[startup+291.549 s]
Raw data (loadavg): 1.00 1.01 1.00 1/53 8419
Raw data (stat): 8409 (java) R 8408 23514 23513 0 -1 0 18031 0 1 0 26279 57 0 0 21 0 10 0 780978677 855064576 31991 4294967295 134512640 134569956 3221224368 3221214772 1080204031 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208756 31991 13086 16 0 208740 0
vsize: 0

Child status: 20
Real time (s): 291.548
CPU time (s): 297.057
CPU user time (s): 296.039
CPU system time (s): 1.01784
CPU usage (%): 101.889
Max. virtual memory (Kb): 836048
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####