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.Ic22arity.ucl.opb
MD5SUM	6bfe4c2dce1e5dbe61cc34b52b1b387f
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	130
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	512
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	45.816
Number of variables	87751
Total number of constraints	254772
Number of constraints which are clauses	247060
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	7712
Minimum length of a constraint	1
Maximum length of a constraint	15

Trace number 7834

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-17 16:45:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2517 boxname=wulflinc8 idbench=280 idsolver=6 numberseed=0
MD5SUM SOLVER: 2225cba0d9b2c30e235f6cafc823d7ac  /oldhome/oroussel/solvers/PBS4
MD5SUM BENCH:  6bfe4c2dce1e5dbe61cc34b52b1b387f  /oldhome/oroussel/tmp/wulflinc8/normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb
REAL COMMAND:  PBS4 /oldhome/oroussel/tmp/wulflinc8/normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb
IDLAUNCH: 2517
/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:        826728 kB
Buffers:         38668 kB
Cached:         145612 kB
SwapCached:          0 kB
Active:          98020 kB
Inactive:        90960 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        826476 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            13356 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-17 16:50:48 (client local time) WITH STATUS 20 IN 334.472 SECONDS
stats: 2517 7 334.472 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c PBS v4 by Bashar Al-Rawi & Fadi Aloul
c Solving /oldhome/oroussel/tmp/wulflinc8/normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb ......
s UNSATISFIABLE
c Done, CPU Time=322.478
#### 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.65 0.86 0.87 2/54 19013
Raw data (stat): 19013 (runsolver) R 19012 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 440271224 1052672 99 4294967295 134512640 135381576 3221224512 3221219760 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.0011 s]
Raw data (loadavg): 0.70 0.86 0.87 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 9022 0 0 0 974 25 0 0 25 0 1 0 440271224 34377728 7427 4294967295 134512640 135450300 3221224624 3221157344 134523738 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8393 7427 231 231 0 8162 0
vsize: 33572
[startup+20.0014 s]
Raw data (loadavg): 0.75 0.87 0.87 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 10886 0 0 0 1968 31 0 0 25 0 1 0 440271224 40878080 9066 4294967295 134512640 135450300 3221224624 3221223360 134538069 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 9980 9066 231 231 0 9749 0
vsize: 39920
[startup+30.0015 s]
Raw data (loadavg): 0.78 0.87 0.88 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 11340 0 0 0 2967 32 0 0 25 0 1 0 440271224 42160128 9348 4294967295 134512640 135450300 3221224624 3221223360 134538672 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10293 9348 231 231 0 10062 0
vsize: 41172
[startup+40.0091 s]
Raw data (loadavg): 0.82 0.87 0.88 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 11814 0 0 0 3966 34 0 0 25 0 1 0 440271224 43630592 9650 4294967295 134512640 135450300 3221224624 3221223360 134538443 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10652 9650 231 231 0 10421 0
vsize: 42608
[startup+50.0188 s]
Raw data (loadavg): 0.84 0.88 0.88 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 12045 0 0 0 4967 35 0 0 25 0 1 0 440271224 43765760 9709 4294967295 134512640 135450300 3221224624 3221223360 134538463 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10685 9709 231 231 0 10454 0
vsize: 42740
[startup+60.0189 s]
Raw data (loadavg): 0.87 0.88 0.88 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 12088 0 0 0 5967 35 0 0 25 0 1 0 440271224 43900928 9752 4294967295 134512640 135450300 3221224624 3221223020 134533046 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10718 9752 231 231 0 10487 0
vsize: 42872
[startup+70.0187 s]
Raw data (loadavg): 0.89 0.88 0.88 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 12132 0 0 0 6966 36 0 0 25 0 1 0 440271224 44036096 9796 4294967295 134512640 135450300 3221224624 3221223500 135126769 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10751 9796 231 231 0 10520 0
vsize: 43004
[startup+80.0191 s]
Raw data (loadavg): 0.90 0.89 0.88 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 12269 0 0 0 7966 36 0 0 25 0 1 0 440271224 44437504 9900 4294967295 134512640 135450300 3221224624 3221223552 134539619 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10849 9900 231 231 0 10618 0
vsize: 43396
[startup+90.0192 s]
Raw data (loadavg): 0.92 0.89 0.88 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 12322 0 0 0 8965 37 0 0 25 0 1 0 440271224 44572672 9953 4294967295 134512640 135450300 3221224624 3221223488 134539158 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10882 9953 231 231 0 10651 0
vsize: 43528
[startup+100.019 s]
Raw data (loadavg): 0.93 0.89 0.88 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 12530 0 0 0 9964 38 0 0 25 0 1 0 440271224 44707840 9989 4294967295 134512640 135450300 3221224624 3221223360 134538945 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10915 9989 231 231 0 10684 0
vsize: 43660
[startup+110.02 s]
Raw data (loadavg): 0.94 0.90 0.88 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 12595 0 0 0 10964 39 0 0 25 0 1 0 440271224 44978176 10054 4294967295 134512640 135450300 3221224624 3221223036 134533356 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10981 10054 231 231 0 10750 0
vsize: 43924
[startup+120.02 s]
Raw data (loadavg): 0.95 0.90 0.88 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 12638 0 0 0 11963 39 0 0 25 0 1 0 440271224 45113344 10097 4294967295 134512640 135450300 3221224624 3221223500 135126769 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11014 10097 231 231 0 10783 0
vsize: 44056
[startup+130.02 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 12656 0 0 0 12963 40 0 0 25 0 1 0 440271224 45113344 10115 4294967295 134512640 135450300 3221224624 3221223360 134538459 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11014 10115 231 231 0 10783 0
vsize: 44056
[startup+140.02 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 12694 0 0 0 13962 41 0 0 25 0 1 0 440271224 45113344 10153 4294967295 134512640 135450300 3221224624 3221223360 134538672 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11014 10153 231 231 0 10783 0
vsize: 44056
[startup+150.02 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 12964 0 0 0 14961 42 0 0 25 0 1 0 440271224 45514752 10251 4294967295 134512640 135450300 3221224624 3221223500 135126769 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11112 10251 231 231 0 10881 0
vsize: 44448
[startup+160.021 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 12987 0 0 0 15961 42 0 0 25 0 1 0 440271224 45514752 10274 4294967295 134512640 135450300 3221224624 3221223360 134538487 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11112 10274 231 231 0 10881 0
vsize: 44448
[startup+170.02 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 13033 0 0 0 16960 43 0 0 25 0 1 0 440271224 45514752 10320 4294967295 134512640 135450300 3221224624 3221223360 134537876 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11112 10320 231 231 0 10881 0
vsize: 44448
[startup+180.021 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 13490 0 0 0 17960 44 0 0 25 0 1 0 440271224 47726592 10777 4294967295 134512640 135450300 3221224624 3221223564 134530372 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11652 10777 231 231 0 11421 0
vsize: 46608
[startup+190.022 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 13879 0 0 0 18959 45 0 0 25 0 1 0 440271224 49328128 11133 4294967295 134512640 135450300 3221224624 3221223360 134538459 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 12043 11133 231 231 0 11812 0
vsize: 48172
[startup+200.022 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 13988 0 0 0 19959 45 0 0 25 0 1 0 440271224 49856512 11242 4294967295 134512640 135450300 3221224624 3221223360 134538672 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 12172 11242 231 231 0 11941 0
vsize: 48688
[startup+210.022 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 14250 0 0 0 20958 46 0 0 25 0 1 0 440271224 50925568 11504 4294967295 134512640 135450300 3221224624 3221223508 134539108 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 12433 11504 231 231 0 12202 0
vsize: 49732
[startup+220.022 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 14329 0 0 0 21957 47 0 0 25 0 1 0 440271224 51195904 11583 4294967295 134512640 135450300 3221224624 3221223360 134538549 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 12499 11583 231 231 0 12268 0
vsize: 49996
[startup+230.023 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 14356 0 0 0 22956 48 0 0 25 0 1 0 440271224 51195904 11610 4294967295 134512640 135450300 3221224624 3221223360 134538549 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 12499 11610 231 231 0 12268 0
vsize: 49996
[startup+240.023 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 14499 0 0 0 23955 49 0 0 25 0 1 0 440271224 51871744 11753 4294967295 134512640 135450300 3221224624 3221223360 134538435 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 12664 11753 231 231 0 12433 0
vsize: 50656
[startup+250.023 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 14634 0 0 0 24955 50 0 0 25 0 1 0 440271224 52404224 11855 4294967295 134512640 135450300 3221224624 3221223232 134537582 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 12794 11855 231 231 0 12563 0
vsize: 51176
[startup+260.023 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 14657 0 0 0 25954 51 0 0 25 0 1 0 440271224 60792832 11878 4294967295 134512640 135450300 3221224624 3221223360 134538549 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 14842 11878 231 231 0 14611 0
vsize: 59368
[startup+270.023 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 14706 0 0 0 26954 51 0 0 25 0 1 0 440271224 60928000 11927 4294967295 134512640 135450300 3221224624 3221223360 134538512 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 14875 11927 231 231 0 14644 0
vsize: 59500
[startup+280.024 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 15033 0 0 0 27953 52 0 0 25 0 1 0 440271224 61329408 12049 4294967295 134512640 135450300 3221224624 3221223500 135126769 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 14973 12049 231 231 0 14742 0
vsize: 59892
[startup+290.025 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 15037 0 0 0 28953 53 0 0 25 0 1 0 440271224 61329408 12053 4294967295 134512640 135450300 3221224624 3221223360 134538549 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 14973 12053 231 231 0 14742 0
vsize: 59892
[startup+300.025 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 15044 0 0 0 29952 54 0 0 25 0 1 0 440271224 61329408 12060 4294967295 134512640 135450300 3221224624 3221223360 134538654 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 14973 12060 231 231 0 14742 0
vsize: 59892
[startup+310.026 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 15117 0 0 0 30952 54 0 0 25 0 1 0 440271224 61460480 12100 4294967295 134512640 135450300 3221224624 3221223456 134549362 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 15005 12100 231 231 0 14774 0
vsize: 60020
[startup+320.026 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 15152 0 0 0 31952 55 0 0 25 0 1 0 440271224 61460480 12135 4294967295 134512640 135450300 3221224624 3221223360 134538435 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 15005 12135 231 231 0 14774 0
vsize: 60020
[startup+330.027 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 15184 0 0 0 32952 55 0 0 25 0 1 0 440271224 61460480 12167 4294967295 134512640 135450300 3221224624 3221223360 134538604 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 15005 12167 231 231 0 14774 0
vsize: 60020
[startup+334.424 s]
Raw data (loadavg): 0.99 0.94 0.91 1/53 19013
Raw data (stat): 19013 (PBS4) R 19012 26667 26666 0 -1 0 15184 0 0 0 32952 55 0 0 25 0 1 0 440271224 61460480 12167 4294967295 134512640 135450300 3221224624 3221223360 134538604 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 15005 12167 231 231 0 14774 0
vsize: 0

Child status: 20
Real time (s): 334.423
CPU time (s): 334.472
CPU user time (s): 333.886
CPU system time (s): 0.58591
CPU usage (%): 100.015
Max. virtual memory (Kb): 60020
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####