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/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-my_adder.opb
MD5SUM	fe8f615a95a6852516985b8e3e78bd85
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4561
Optimality of the best value was proved	NO
Number of terms in the objective function	577
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	24510
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	24510
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	577
Total number of constraints	1322
Number of constraints which are clauses	1306
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	16
Minimum length of a constraint	2
Maximum length of a constraint	17

Trace number 42133

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-06-16 00:53:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=25353 boxname=wulflinc5 idbench=255 idsolver=18 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fe8f615a95a6852516985b8e3e78bd85  /oldhome/oroussel/tmp/wulflinc5/normalized-my_adder.opb
REAL COMMAND:  pb2sat-v2 /oldhome/oroussel/tmp/wulflinc5/normalized-my_adder.opb
IDLAUNCH: 25353
/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:        827024 kB
Buffers:         34044 kB
Cached:         150964 kB
SwapCached:        700 kB
Active:          72756 kB
Inactive:       114384 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        826772 kB
SwapTotal:     2097136 kB
SwapFree:      2095508 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5156 kB
Slab:            14724 kB
Committed_AS:    63680 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-16 00:56:42 (client local time) WITH STATUS 1 IN 195.022 SECONDS
stats: 25353 7 195.022 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...
c got solution with objective value: 22983
c big objective detected
c trying from 0 to 511
c trying from 512 to 1023
c trying from 1024 to 1535
c trying from 1536 to 2047

	Unexpected exception :
	St9bad_alloc
#### 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.93 0.98 0.93 1/54 5416
Raw data (stat): 5416 (runsolver) R 5415 7266 7265 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 966594192 884736 94 4294967295 134512640 135332820 3221224480 3221219660 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0007 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 27366 0 0 0 941 58 0 0 25 0 1 0 966594192 85901312 16257 4294967295 134512640 135730672 3221224592 3221000464 135292561 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 20972 16257 301 301 0 20671 0
vsize: 83888
[startup+20.0015 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 49704 0 0 0 1893 105 0 0 25 0 1 0 966594192 151773184 27174 4294967295 134512640 135730672 3221224592 3221222968 134748061 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 37054 27174 301 301 0 36753 0
vsize: 148216
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 60204 0 0 0 2869 129 0 0 25 0 1 0 966594192 176074752 37565 4294967295 134512640 135730672 3221224592 3221147200 134607963 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 42987 37565 301 301 0 42686 0
vsize: 171948
[startup+40.0023 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 96096 0 0 0 3790 207 0 0 25 0 1 0 966594192 293957632 51794 4294967295 134512640 135730672 3221224592 3221049752 134787727 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 71767 51794 301 301 0 71466 0
vsize: 287068
[startup+50.0028 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 108473 0 0 0 4762 236 0 0 25 0 1 0 966594192 316006400 63964 4294967295 134512640 135730672 3221224592 3221088104 135284279 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 77150 63965 301 301 0 76849 0
vsize: 308600
[startup+60.0028 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 122109 0 0 0 5733 265 0 0 25 0 1 0 966594192 338812928 74136 4294967295 134512640 135730672 3221224592 3221222816 134747543 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 82718 74136 301 301 0 82417 0
vsize: 330872
[startup+70.0039 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 132398 0 0 0 6707 291 0 0 25 0 1 0 966594192 380198912 83750 4294967295 134512640 135730672 3221224592 3221222632 135285983 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 92822 83751 301 301 0 92521 0
vsize: 371288
[startup+80.004 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 140713 0 0 0 7688 309 0 0 25 0 1 0 966594192 395743232 91966 4294967295 134512640 135730672 3221224592 3221174068 135282779 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 96617 91966 301 301 0 96316 0
vsize: 386468
[startup+90.0051 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 194118 0 0 0 8588 410 0 0 25 0 1 0 966594192 695275520 126837 4294967295 134512640 135730672 3221224592 3221133776 134788521 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 169745 126841 301 301 0 169444 0
vsize: 678980
[startup+100.006 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 203218 0 0 0 9564 434 0 0 25 0 1 0 966594192 594608128 111152 4294967295 134512640 135730672 3221224592 3221045024 134770712 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 145168 111152 301 301 0 144867 0
vsize: 580672
[startup+110.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 212826 0 0 0 10542 456 0 0 25 0 1 0 966594192 616927232 120567 4294967295 134512640 135730672 3221224592 3221133768 134549480 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 150617 120567 301 301 0 150316 0
vsize: 602468
[startup+120.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 230697 0 0 0 11503 496 0 0 25 0 1 0 966594192 642473984 138230 4294967295 134512640 135730672 3221224592 3221142464 134546483 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 156854 138230 301 301 0 156553 0
vsize: 627416
[startup+130.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 244319 0 0 0 12470 529 0 0 25 0 1 0 966594192 664584192 143827 4294967295 134512640 135730672 3221224592 3221222816 134747592 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 162252 143827 301 301 0 161951 0
vsize: 649008
[startup+140.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 245467 0 0 0 13469 530 0 0 25 0 1 0 966594192 667373568 144393 4294967295 134512640 135730672 3221224592 3221222976 134734769 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 162933 144393 301 301 0 162632 0
vsize: 651732
[startup+150.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 247742 0 0 0 14464 536 0 0 25 0 1 0 966594192 676569088 146668 4294967295 134512640 135730672 3221224592 3221222632 135285983 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 165178 146668 301 301 0 164877 0
vsize: 660712
[startup+160.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 261037 0 0 0 15431 569 0 0 25 0 1 0 966594192 730906624 159963 4294967295 134512640 135730672 3221224592 3221222632 135285983 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 178444 159963 301 301 0 178143 0
vsize: 713776
[startup+170.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 268683 0 0 0 16411 589 0 0 25 0 1 0 966594192 772022272 167538 4294967295 134512640 135730672 3221224592 3221010592 134770027 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 188482 167538 301 301 0 188181 0
vsize: 753928
[startup+180.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 280019 0 0 0 17388 612 0 0 25 0 1 0 966594192 772022272 178672 4294967295 134512640 135730672 3221224592 3221202748 134608033 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 188482 178672 301 301 0 188181 0
vsize: 753928
[startup+190.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 286409 0 0 0 18369 630 0 0 25 0 1 0 966594192 670248960 162591 4294967295 134512640 135730672 3221224592 3221222336 134787193 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 163635 162591 301 301 0 163334 0
vsize: 654540
[startup+195.031 s]
Raw data (loadavg): 0.99 0.98 0.93 1/53 5416
Raw data (stat): 5416 (pb2sat-v2) R 5415 7266 7265 0 -1 0 286409 0 0 0 18369 630 0 0 25 0 1 0 966594192 670248960 162591 4294967295 134512640 135730672 3221224592 3221222336 134787193 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 163635 162591 301 301 0 163334 0
vsize: 0

Child status: 1
Real time (s): 195.031
CPU time (s): 195.022
CPU user time (s): 188.395
CPU system time (s): 6.62699
CPU usage (%): 99.9958
Max. virtual memory (Kb): 753928
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####