70 lines
4.2 KiB
Plaintext
70 lines
4.2 KiB
Plaintext
c
|
|
c Mallob -- a parallel and distributed platform for job scheduling, load balancing, and SAT solving
|
|
c Designed by P. Sanders and D. Schreiber 2018-2022
|
|
c Developed by D. Schreiber 2019-2022
|
|
c
|
|
c 0.000 0 Program options: -0o=1 -J=1 -T=0 -ajpc=0 -ans=0 -appmode=fork -ba=4 -bicg=4 -c=1 -cbbs=1500 -cbdf=1 -cfci=500 -cg=1 -ch=0 -chaf=5 -checksums=0 -chstms=10 -cmp=0 -colors=0 -dc=0 -ddd=0 -delaymonkey=0 -derandomize=1 -evu=0 -fapii=0 -g=0 -gclls=0 -h=0 -hbbfs=10 -hubfs=9999999 -huca=-1 -interface-fs=0 -interface-ipc=0 -isp=0 -jc=4 -jcl=0 -jcup=0 -jjp=0 -jwl=0 -l=1 -latencymonkey=0 -ljpc=32 -mbfsd=4 -mbt=1000000 -mcips=10 -md=0 -mid=0 -mjps=0 -mlbdps=2 -mlpt=50000000 -mmpi=0 -mono=/rundir/experiment/test.cnf -nce=20 -os=0 -p=0.01 -phasediv=1 -pls=0 -pph=0 -q=0 -qcll=8 -qlbdl=2 -ril=0 -rpa=1 -rs=1 -rto=0 -s=1 -satsolver=k -scll=20 -seed=0 -sjd=0 -slbdl=30 -sleep=1000 -t=4 -trace-dir=competition -v=3 -w=-1 -wam=10000 -warmup=0 -watchdog=1 -wr=0 -y=1 -yield=0
|
|
c 0.000 0 Mallob rls pid=18 on host d6efa65e5077
|
|
c 0.000 0 8 workers, 1 clients
|
|
c 0.126 0 Created client communicator
|
|
c 0.225 0 Created worker communicator
|
|
c 0.225 0 My bounce alternatives: 5 7 6 2
|
|
c 0.225 0 Set up API at src/interface/api/api_connector.hpp
|
|
c 0.225 0 <Janitor> tid=79
|
|
c 0.235 0 <Reader> Starting
|
|
c 0.297 0 Machine color 0 with 4 total workers (my rank: 0)
|
|
c 0.297 0 I Mapping job "admin.mono-job.json" to internal ID #1
|
|
c 0.297 0 <Reader> [T] Reading job #1 rev. 0 {/rundir/experiment/test.cnf} ...
|
|
c 0.297 0 <Reader> [T] Initialized job #1 {/rundir/experiment/test.cnf} in 0.000s: 7 lits w/ separators, 0 assumptions
|
|
c 0.298 0 Introducing job #1 rev. 0 : r.#1:0 rev. 0 <- [0] born=0.298 hops=0 epoch=-1 => [1]
|
|
c 0.301 0 Scheduling r.#1:0 rev. 0 <- [0] born=0.298 hops=1 epoch=-1 on [3] (latency: 0.00327s)
|
|
c 0.312 0 ADOPT r.#1:2 rev. 0 <- [3] born=0.336 hops=0 epoch=2 mode=1 <= [3]
|
|
c 0.312 0 COMMIT #1 -> #1:2
|
|
c 0.313 0 #1:2 growing: r.#1:5 rev. 0 <- [0] born=0.313 hops=0 epoch=2 => [6]
|
|
c 0.313 0 #1:2 growing: r.#1:6 rev. 0 <- [0] born=0.313 hops=0 epoch=2 => [4]
|
|
c 0.314 0 UNCOMMIT #1:2
|
|
c 0.314 0 LOAD 1 (+#1:2)
|
|
c 0.314 0 EXECUTE #1:2 <= [3]
|
|
c 0.326 0 <#1> Mallob SAT engine rls pid=94
|
|
c 0.326 0 <#1> S8.0 Diversifying 8
|
|
c 0.326 0 <#1> S8.0 found result SAT for rev. 0
|
|
c 0.326 0 <#1> S9.0 Diversifying 9
|
|
c 0.326 0 <#1> S9.0 found result SAT for rev. 0
|
|
c 0.326 0 <#1> S10.0 Diversifying 10
|
|
c 0.327 0 <#1> S11.0 Diversifying 11
|
|
c 0.327 0 <#1> S11.0 found result SAT for rev. 0
|
|
c 0.327 0 <#1> S10.0 found result SAT for rev. 0
|
|
c 0.337 0 LOAD 0 (-#1:2)
|
|
c 0.337 0 #1:2 desires fulfilled=0.0000 latency={num:0 min:0.00000 med:0.00000 avg:0.00000 max:0.00000}
|
|
c 0.337 0 <#1> END S8 pps:3 dcs:2 cfs:0 rst:0 prod:0 (flt:0 adm:0 drp:0) recv:0 (flt:0 digd:0 drp:0) + intim:0/0
|
|
c 0.337 0 <#1> END S8 clenhist prod total:0 0
|
|
c 0.337 0 <#1> END S8 clenhist digd total:0 0
|
|
c 0.337 0 <#1> END S9 pps:3 dcs:2 cfs:0 rst:0 prod:0 (flt:0 adm:0 drp:0) recv:0 (flt:0 digd:0 drp:0) + intim:0/0
|
|
c 0.337 0 <#1> END S9 clenhist prod total:0 0
|
|
c 0.337 0 <#1> END S9 clenhist digd total:0 0
|
|
c 0.337 0 <#1> END S10 pps:3 dcs:2 cfs:0 rst:0 prod:0 (flt:0 adm:0 drp:0) recv:0 (flt:0 digd:0 drp:0) + intim:0/0
|
|
c 0.337 0 <#1> END S10 clenhist prod total:0 0
|
|
c 0.337 0 <#1> END S10 clenhist digd total:0 0
|
|
c 0.337 0 <#1> END S11 pps:3 dcs:2 cfs:0 rst:0 prod:0 (flt:0 adm:0 drp:0) recv:0 (flt:0 digd:0 drp:0) + intim:0/0
|
|
c 0.337 0 <#1> END S11 clenhist prod total:0 0
|
|
c 0.337 0 <#1> END S11 clenhist digd total:0 0
|
|
c 0.337 0 <#1> END pps:12 dcs:8 cfs:0 rst:0 prod:0 (flt:0 adm:0 drp:0) recv:0 (flt:0 digd:0 drp:0) + intim:0/0
|
|
c 0.337 0 <#1> END exp:0/0 drp:0(0.000000) pflt:0 sflt:0
|
|
c 0.337 0 <#1> clenhist prod total:0 0
|
|
c 0.337 0 <#1> clenhist flfl total:0 0
|
|
c 0.337 0 <#1> clenhist admt total:0 0
|
|
c 0.337 0 <#1> clenhist drpd total:0 0
|
|
c 0.337 0 <#1> clenhist dltd total:0 0
|
|
c 0.337 0 <#1> clenhist retd total:0 0
|
|
c 0.348 0 RESPONSE_TIME #1 0.049750 rev. 0
|
|
c 0.348 0 SOLUTION #1 SAT rev. 0
|
|
s SATISFIABLE
|
|
v 1 2 3 0
|
|
c 0.349 0 Received exit signal <= [0]
|
|
c 0.349 0 Terminating.
|
|
c 0.444 0 busytime=0.023
|
|
c 0.544 0 STATS treegrowth_latencies num:0 min:0.000000 max:0.000000 med:0.000000 mean:0.000000
|
|
c 0.545 0 STATS balancing_latencies num:0 min:0.000000 max:0.000000 med:0.000000 mean:0.000000
|
|
c 0.545 0 <Reader> Stopping
|
|
c 0.794 0 Exiting happily
|