From 07a2c5cc72a6eaf5f27ab9eaf1153e45f5ddff39 Mon Sep 17 00:00:00 2001 From: YuhangQ Date: Fri, 21 Apr 2023 16:24:52 +0800 Subject: [PATCH] =?UTF-8?q?=E4=BF=AE=E5=A4=8D=20RS=20=E7=9A=84=20BUG?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- kissat-inc/src/bump.c | 5 +- run.sh | 19 +- src/sharer.cpp | 2 + test.log | 545 ++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 560 insertions(+), 11 deletions(-) create mode 100644 test.log diff --git a/kissat-inc/src/bump.c b/kissat-inc/src/bump.c index d0df120..fc2a0e3 100644 --- a/kissat-inc/src/bump.c +++ b/kissat-inc/src/bump.c @@ -76,12 +76,13 @@ void kissat_init_shuffle(kissat * solver, int maxvar) { } int block_size = maxvar / number; - int cursor = index * block_size; + int cursor = index * block_size + 1; + for(int i=cursor; i<=maxvar; i++) { kissat_activate_literal(solver, kissat_import_literal(solver, id[i])); } - for (int i = 1; i < cursor ; i++) { + for (int i = 1; i < cursor && i <= maxvar ; i++) { kissat_activate_literal(solver, kissat_import_literal(solver, id[i])); } diff --git a/run.sh b/run.sh index d16adc0..bebe45b 100755 --- a/run.sh +++ b/run.sh @@ -21,21 +21,22 @@ # 3d2a6e5c2f8f58dee79fd50444009625-cfi-rigid-z2-0088-03-or_2_shuffle_all.cnf -# 这个存在问题 -DIR=/pub/data/chenzh/data/sat2022 -INSTANCE=04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf - -# make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 - - # cd kissat-inc # make clean # ./configure # make -j 64 # cd .. - # make clean -make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i ./data/WS_500_16_70_10.apx_0.cnf --share=1 --threads=16 --times=3600 +# 这个存在问题 +DIR=/pub/data/chenzh/data/sat2022 +INSTANCE=d87714e099c66f0034fb95727fa47ccc-Wallace_Bits_Fast_2.cnf.cnf + +make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --shuffle=1 --share=1 --threads=16 --times=3600 --share_method=0 + + + + +# make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i ./data/WS_500_16_70_10.apx_0.cnf --share=1 --threads=16 --times=3600 #./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 diff --git a/src/sharer.cpp b/src/sharer.cpp index b57d619..35dbbf4 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -358,6 +358,8 @@ void sharer::init_tree_transmission(std::vector> &sharing_group } } + MPI_Barrier(MPI_COMM_WORLD); + } void sharer::init_circular_transmission(std::vector> &sharing_groups) { diff --git a/test.log b/test.log new file mode 100644 index 0000000..ccdf39d --- /dev/null +++ b/test.log @@ -0,0 +1,545 @@ +make: 'light' is up to date. +c ------------------- Paras list ------------------- +c Name Type Now Default Comment +c DPS int 0 0 DPS/NPS +c DPS_period int 10000 10000 DPS sharing period +c margin int 0 0 DPS margin +c pakis int 1 1 Use pakis diversity +c reset int 0 0 Dynamically reseting +c reset_time int 10 10 Reseting base interval (seconds) +c share int 1 1 Sharing learnt clauses +c share_intv int 500000 500000 Sharing interval (microseconds) +c share_lits int 1500 1500 Sharing lits (per every #share_intv seconds) +c share_method int 1 1 0 for Circle Propagate/ 1 for Tree Broadcast +c shuffle int 1 1 Use random shuffle +c simplify int 1 1 Use Simplify (only preprocess) +c threads int 16 32 Thread number +c times double 3600.000000 5000 Cutoff time +c unique int 1 1 Whether perform unique checking when receiving clauses from other nodes +c config string "" Config file +c instance string /pub/data/chenzh/data/sat2022/d87714e099c66f0034fb95727fa47ccc-Wallace_Bits_Fast_2.cnf.cnf "" CNF format instance +c -------------------------------------------------- +c [leader] preprocess(simplify) input data +c [GE] XORs: 2879 (time: 0.00) +c [GE] VAR SCC: 1009 +c [GE] XOR SCCs: 66 (time: 0.00) +c [GE] unary xor: 0, bin xor: 0, bin added +c After preprocess: vars: 5892 -> 5825 , clauses: 23367 -> 23165 , +c [CE] almost one cons: 133 +c len 0 +c sz 2 +c turns: 4 +c After preprocess: vars: 5825 -> 5675 , clauses: 23165 -> 22697 , +c [leader] hand out length of cnf instance to all nodes +c [leader] hand out cnf instance to all nodes +c [leader] hand out done! +c index:5 number:16 seed:8 +c index:4 number:16 seed:8 +c index:0 number:16 seed:8 +c index:3 number:16 seed:8 +c index:1 number:16 seed:8 +c index:2 number:16 seed:8 +c index:10 number:16 seed:8 +c index:6 number:16 seed:8 +c index:15 number:16 seed:8 +c index:8 number:16 seed:8 +c index:15 number:16 seed:3 +c index:1 number:16 seed:3 +c index:7 number:16 seed:8 +c index:0 number:16 seed:3 +c index:2 number:16 seed:7 +c index:9 number:16 seed:3 +c index:5 number:16 seed:3 +c index:2 number:16 seed:5 +c index:7 number:16 seed:5 +c index:13 number:16 seed:5 +c index:4 number:16 seed:3 +c index:7 number:16 seed:3 +c index:0 number:16 seed:5 +c index:6 number:16 seed:5 +c index:3 number:16 seed:5 +c index:11 number:16 seed:5 +c index:14 number:16 seed:8 +c index:12 number:16 seed:8 +c index:9 number:16 seed:8 +c index:13 number:16 seed:8 +c index:11 number:16 seed:8 +c index:0 number:16 seed:4 +c index:10 number:16 seed:5 +c index:10 number:16 seed:6 +c index:0 number:16 seed:6 +c index:4 number:16 seed:5 +c index:12 number:16 seed:5 +c index:15 number:16 seed:5 +c index:1 number:16 seed:5 +c index:8 number:16 seed:5 +c index:9 number:16 seed:5 +c index:5 number:16 seed:5 +c index:14 number:16 seed:5 +c index:5 number:16 seed:4 +c index:7 number:16 seed:6 +c index:5 number:16 seed:6 +c index:1 number:16 seed:6 +c index:3 number:16 seed:6 +c index:3 number:16 seed:4 +c index:13 number:16 seed:4 +c index:14 number:16 seed:4 +c index:8 number:16 seed:4 +c index:10 number:16 seed:4 +c index:2 number:16 seed:4 +c index:14 number:16 seed:6 +c index:6 number:16 seed:6 +c index:13 number:16 seed:6 +c index:15 number:16 seed:6 +c index:9 number:16 seed:6 +c index:2 number:16 seed:6 +c index:3 number:16 seed:3 +c index:14 number:16 seed:3 +c index:2 number:16 seed:3 +c index:11 number:16 seed:4 +c index:12 number:16 seed:3 +c index:13 number:16 seed:3 +c index:12 number:16 seed:4 +c index:8 number:16 seed:3 +c index:1 number:16 seed:1 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:0 number:16 seed:1 +c index:12 number:16 seed:1 +c index:5 number:16 seed:1 +c index:12 number:16 seed:6 +c index:6 number:16 seed:4 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:13 number:16 seed:1 +c index:7 number:16 seed:4 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:15 number:16 seed:4 +c index:9 number:16 seed:4 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:7 number:16 seed:1 +c index:-1 number:-1 seed:-1 +c index:4 number:16 seed:4 +c index:-1 number:-1 seed:-1 +c index:1 number:16 seed:4 +c index:10 number:16 seed:1 +c index:15 number:16 seed:1 +c index:9 number:16 seed:1 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] +c =========build tree========= +c son[1][1][0]=-1 son[1][1][1]=-1 +c son[2][2][0]=-1 son[2][2][1]=-1 +c son[3][3][0]=6 son[3][3][1]=8 +c index:11 number:16 seed:6 +c son[3][6][0]=4 son[3][6][1]=5 +c son[3][8][0]=7 son[3][8][1]=-1 +c son[3][4][0]=-1 son[3][4][1]=-1 +c son[3][5][0]=-1 son[3][5][1]=-1 +c son[3][7][0]=-1 son[3][7][1]=-1 +c son[4][4][0]=7 son[4][4][1]=3 +c son[4][7][0]=8 son[4][7][1]=5 +c son[4][3][0]=6 son[4][3][1]=-1 +c son[4][8][0]=-1 son[4][8][1]=-1 +c son[4][5][0]=-1 son[4][5][1]=-1 +c son[4][6][0]=-1 son[4][6][1]=-1 +c son[5][5][0]=4 son[5][5][1]=6 +c son[5][4][0]=7 son[5][4][1]=8 +c son[5][6][0]=3 son[5][6][1]=-1 +c son[5][7][0]=-1 son[5][7][1]=-1 +c son[5][8][0]=-1 son[5][8][1]=-1 +c son[5][3][0]=-1 son[5][3][1]=-1 +c son[6][6][0]=8 son[6][6][1]=7 +c son[6][8][0]=5 son[6][8][1]=3 +c son[6][7][0]=4 son[6][7][1]=-1 +c son[6][5][0]=-1 son[6][5][1]=-1 +c son[6][3][0]=-1 son[6][3][1]=-1 +c son[6][4][0]=-1 son[6][4][1]=-1 +c son[7][7][0]=8 son[7][7][1]=4 +c son[7][8][0]=6 son[7][8][1]=3 +c son[7][4][0]=5 son[7][4][1]=-1 +c son[7][6][0]=-1 son[7][6][1]=-1 +c son[7][3][0]=-1 son[7][3][1]=-1 +c son[7][5][0]=-1 son[7][5][1]=-1 +c son[8][8][0]=7 son[8][8][1]=4 +c son[8][7][0]=6 son[8][7][1]=5 +c son[8][4][0]=3 son[8][4][1]=-1 +c son[8][6][0]=-1 son[8][6][1]=-1 +c son[8][5][0]=-1 son[8][5][1]=-1 +c son[8][3][0]=-1 son[8][3][1]=-1 +c index:4 number:16 seed:6 +c index:0 number:16 seed:7 +c index:1 number:16 seed:7 +c index:10 number:16 seed:3 +c index:4 number:16 seed:1 +c index:6 number:16 seed:1 +c index:3 number:16 seed:1 +c index:8 number:16 seed:1 +c index:14 number:16 seed:1 +c index:11 number:16 seed:1 +c index:6 number:16 seed:3 +c index:13 number:16 seed:7 +c index:15 number:16 seed:7 +c index:7 number:16 seed:7 +c index:5 number:16 seed:7 +c index:14 number:16 seed:7 +c index:8 number:16 seed:7 +c index:2 number:16 seed:1 +c index:8 number:16 seed:6 +c index:9 number:16 seed:7 +c index:3 number:16 seed:7 +c index:12 number:16 seed:7 +c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] +c =========build tree========= +c son[1][1][0]=-1 son[1][1][1]=-1 +c son[2][2][0]=-1 son[2][2][1]=-1 +c son[3][3][0]=6 son[3][3][1]=8 +c son[3][6][0]=4 son[3][6][1]=5 +c son[3][8][0]=7 son[3][8][1]=-1 +c son[3][4][0]=-1 son[3][4][1]=-1 +c son[3][5][0]=-1 son[3][5][1]=-1 +c son[3][7][0]=-1 son[3][7][1]=-1 +c son[4][4][0]=7 son[4][4][1]=3 +c son[4][7][0]=8 son[4][7][1]=5 +c son[4][3][0]=6 son[4][3][1]=-1 +c son[4][8][0]=-1 son[4][8][1]=-1 +c son[4][5][0]=-1 son[4][5][1]=-1 +c son[4][6][0]=-1 son[4][6][1]=-1 +c son[5][5][0]=4 son[5][5][1]=6 +c son[5][4][0]=7 son[5][4][1]=8 +c son[5][6][0]=3 son[5][6][1]=-1 +c son[5][7][0]=-1 son[5][7][1]=-1 +c son[5][8][0]=-1 son[5][8][1]=-1 +c son[5][3][0]=-1 son[5][3][1]=-1 +c son[6][6][0]=8 son[6][6][1]=7 +c son[6][8][0]=5 son[6][8][1]=3 +c son[6][7][0]=4 son[6][7][1]=-1 +c son[6][5][0]=-1 son[6][5][1]=-1 +c son[6][3][0]=-1 son[6][3][1]=-1 +c son[6][4][0]=-1 son[6][4][1]=-1 +c son[7][7][0]=8 son[7][7][1]=4 +c son[7][8][0]=6 son[7][8][1]=3 +c son[7][4][0]=5 son[7][4][1]=-1 +c son[7][6][0]=-1 son[7][6][1]=-1 +c son[7][3][0]=-1 son[7][3][1]=-1 +c son[7][5][0]=-1 son[7][5][1]=-1 +c son[8][8][0]=7 son[8][8][1]=4 +c son[8][7][0]=6 son[8][7][1]=5 +c son[8][4][0]=3 son[8][4][1]=-1 +c son[8][6][0]=-1 son[8][6][1]=-1 +c son[8][5][0]=-1 son[8][5][1]=-1 +c son[8][3][0]=-1 son[8][3][1]=-1 +c index:10 number:16 seed:7 +c index:6 number:16 seed:7 +c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] +c =========build tree========= +c son[1][1][0]=-1 son[1][1][1]=-1 +c son[2][2][0]=-1 son[2][2][1]=-1 +c son[3][3][0]=6 son[3][3][1]=8 +c son[3][6][0]=4 son[3][6][1]=5 +c son[3][8][0]=7 son[3][8][1]=-1 +c son[3][4][0]=-1 son[3][4][1]=-1 +c son[3][5][0]=-1 son[3][5][1]=-1 +c son[3][7][0]=-1 son[3][7][1]=-1 +c son[4][4][0]=7 son[4][4][1]=3 +c son[4][7][0]=8 son[4][7][1]=5 +c son[4][3][0]=6 son[4][3][1]=-1 +c son[4][8][0]=-1 son[4][8][1]=-1 +c son[4][5][0]=-1 son[4][5][1]=-1 +c son[4][6][0]=-1 son[4][6][1]=-1 +c son[5][5][0]=4 son[5][5][1]=6 +c son[5][4][0]=7 son[5][4][1]=8 +c son[5][6][0]=3 son[5][6][1]=-1 +c son[5][7][0]=-1 son[5][7][1]=-1 +c son[5][8][0]=-1 son[5][8][1]=-1 +c son[5][3][0]=-1 son[5][3][1]=-1 +c son[6][6][0]=8 son[6][6][1]=7 +c son[6][8][0]=5 son[6][8][1]=3 +c son[6][7][0]=4 son[6][7][1]=-1 +c son[6][5][0]=-1 son[6][5][1]=-1 +c son[6][3][0]=-1 son[6][3][1]=-1 +c son[6][4][0]=-1 son[6][4][1]=-1 +c son[7][7][0]=8 son[7][7][1]=4 +c son[7][8][0]=6 son[7][8][1]=3 +c son[7][4][0]=5 son[7][4][1]=-1 +c son[7][6][0]=-1 son[7][6][1]=-1 +c son[7][3][0]=-1 son[7][3][1]=-1 +c son[7][5][0]=-1 son[7][5][1]=-1 +c son[8][8][0]=7 son[8][8][1]=4 +c son[8][7][0]=6 son[8][7][1]=5 +c son[8][4][0]=3 son[8][4][1]=-1 +c son[8][6][0]=-1 son[8][6][1]=-1 +c son[8][5][0]=-1 son[8][5][1]=-1 +c son[8][3][0]=-1 son[8][3][1]=-1 +c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] +c =========build tree========= +c son[1][1][0]=-1 son[1][1][1]=-1 +c son[2][2][0]=-1 son[2][2][1]=-1 +c son[3][3][0]=6 son[3][3][1]=8 +c son[3][6][0]=4 son[3][6][1]=5 +c son[3][8][0]=7 son[3][8][1]=-1 +c son[3][4][0]=-1 son[3][4][1]=-1 +c son[3][5][0]=-1 son[3][5][1]=-1 +c son[3][7][0]=-1 son[3][7][1]=-1 +c son[4][4][0]=7 son[4][4][1]=3 +c son[4][7][0]=8 son[4][7][1]=5 +c son[4][3][0]=6 son[4][3][1]=-1 +c son[4][8][0]=-1 son[4][8][1]=-1 +c son[4][5][0]=-1 son[4][5][1]=-1 +c son[4][6][0]=-1 son[4][6][1]=-1 +c son[5][5][0]=4 son[5][5][1]=6 +c son[5][4][0]=7 son[5][4][1]=8 +c son[5][6][0]=3 son[5][6][1]=-1 +c son[5][7][0]=-1 son[5][7][1]=-1 +c son[5][8][0]=-1 son[5][8][1]=-1 +c son[5][3][0]=-1 son[5][3][1]=-1 +c son[6][6][0]=8 son[6][6][1]=7 +c son[6][8][0]=5 son[6][8][1]=3 +c son[6][7][0]=4 son[6][7][1]=-1 +c son[6][5][0]=-1 son[6][5][1]=-1 +c son[6][3][0]=-1 son[6][3][1]=-1 +c son[6][4][0]=-1 son[6][4][1]=-1 +c son[7][7][0]=8 son[7][7][1]=4 +c son[7][8][0]=6 son[7][8][1]=3 +c son[7][4][0]=5 son[7][4][1]=-1 +c son[7][6][0]=-1 son[7][6][1]=-1 +c son[7][3][0]=-1 son[7][3][1]=-1 +c son[7][5][0]=-1 son[7][5][1]=-1 +c son[8][8][0]=7 son[8][8][1]=4 +c son[8][7][0]=6 son[8][7][1]=5 +c son[8][4][0]=3 son[8][4][1]=-1 +c son[8][6][0]=-1 son[8][6][1]=-1 +c son[8][5][0]=-1 son[8][5][1]=-1 +c son[8][3][0]=-1 son[8][3][1]=-1 +c index:11 number:16 seed:3 +c index:4 number:16 seed:7 +c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] +c =========build tree========= +c son[1][1][0]=-1 son[1][1][1]=-1 +c son[2][2][0]=-1 son[2][2][1]=-1 +c son[3][3][0]=6 son[3][3][1]=8 +c son[3][6][0]=4 son[3][6][1]=5 +c son[3][8][0]=7 son[3][8][1]=-1 +c son[3][4][0]=-1 son[3][4][1]=-1 +c son[3][5][0]=-1 son[3][5][1]=-1 +c son[3][7][0]=-1 son[3][7][1]=-1 +c son[4][4][0]=7 son[4][4][1]=3 +c son[4][7][0]=8 son[4][7][1]=5 +c son[4][3][0]=6 son[4][3][1]=-1 +c son[4][8][0]=-1 son[4][8][1]=-1 +c son[4][5][0]=-1 son[4][5][1]=-1 +c son[4][6][0]=-1 son[4][6][1]=-1 +c son[5][5][0]=4 son[5][5][1]=6 +c son[5][4][0]=7 son[5][4][1]=8 +c son[5][6][0]=3 son[5][6][1]=-1 +c son[5][7][0]=-1 son[5][7][1]=-1 +c son[5][8][0]=-1 son[5][8][1]=-1 +c son[5][3][0]=-1 son[5][3][1]=-1 +c son[6][6][0]=8 son[6][6][1]=7 +c son[6][8][0]=5 son[6][8][1]=3 +c son[6][7][0]=4 son[6][7][1]=-1 +c son[6][5][0]=-1 son[6][5][1]=-1 +c son[6][3][0]=-1 son[6][3][1]=-1 +c son[6][4][0]=-1 son[6][4][1]=-1 +c son[7][7][0]=8 son[7][7][1]=4 +c son[7][8][0]=6 son[7][8][1]=3 +c son[7][4][0]=5 son[7][4][1]=-1 +c son[7][6][0]=-1 son[7][6][1]=-1 +c son[7][3][0]=-1 son[7][3][1]=-1 +c son[7][5][0]=-1 son[7][5][1]=-1 +c son[8][8][0]=7 son[8][8][1]=4 +c son[8][7][0]=6 son[8][7][1]=5 +c son[8][4][0]=3 son[8][4][1]=-1 +c son[8][6][0]=-1 son[8][6][1]=-1 +c son[8][5][0]=-1 son[8][5][1]=-1 +c son[8][3][0]=-1 son[8][3][1]=-1 +c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] +c =========build tree========= +c son[1][1][0]=-1 son[1][1][1]=-1 +c son[2][2][0]=-1 son[2][2][1]=-1 +c son[3][3][0]=6 son[3][3][1]=8 +c son[3][6][0]=4 son[3][6][1]=5 +c son[3][8][0]=7 son[3][8][1]=-1 +c son[3][4][0]=-1 son[3][4][1]=-1 +c son[3][5][0]=-1 son[3][5][1]=-1 +c son[3][7][0]=-1 son[3][7][1]=-1 +c son[4][4][0]=7 son[4][4][1]=3 +c son[4][7][0]=8 son[4][7][1]=5 +c son[4][3][0]=6 son[4][3][1]=-1 +c son[4][8][0]=-1 son[4][8][1]=-1 +c son[4][5][0]=-1 son[4][5][1]=-1 +c son[4][6][0]=-1 son[4][6][1]=-1 +c son[5][5][0]=4 son[5][5][1]=6 +c son[5][4][0]=7 son[5][4][1]=8 +c son[5][6][0]=3 son[5][6][1]=-1 +c son[5][7][0]=-1 son[5][7][1]=-1 +c son[5][8][0]=-1 son[5][8][1]=-1 +c son[5][3][0]=-1 son[5][3][1]=-1 +c son[6][6][0]=8 son[6][6][1]=7 +c son[6][8][0]=5 son[6][8][1]=3 +c son[6][7][0]=4 son[6][7][1]=-1 +c son[6][5][0]=-1 son[6][5][1]=-1 +c son[6][3][0]=-1 son[6][3][1]=-1 +c son[6][4][0]=-1 son[6][4][1]=-1 +c son[7][7][0]=8 son[7][7][1]=4 +c son[7][8][0]=6 son[7][8][1]=3 +c son[7][4][0]=5 son[7][4][1]=-1 +c son[7][6][0]=-1 son[7][6][1]=-1 +c son[7][3][0]=-1 son[7][3][1]=-1 +c son[7][5][0]=-1 son[7][5][1]=-1 +c son[8][8][0]=7 son[8][8][1]=4 +c son[8][7][0]=6 son[8][7][1]=5 +c son[8][4][0]=3 son[8][4][1]=-1 +c son[8][6][0]=-1 son[8][6][1]=-1 +c son[8][5][0]=-1 son[8][5][1]=-1 +c son[8][3][0]=-1 son[8][3][1]=-1 +c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] +c =========build tree========= +c son[1][1][0]=-1 son[1][1][1]=-1 +c son[2][2][0]=-1 son[2][2][1]=-1 +c son[3][3][0]=6 son[3][3][1]=8 +c son[3][6][0]=4 son[3][6][1]=5 +c son[3][8][0]=7 son[3][8][1]=-1 +c son[3][4][0]=-1 son[3][4][1]=-1 +c son[3][5][0]=-1 son[3][5][1]=-1 +c son[3][7][0]=-1 son[3][7][1]=-1 +c son[4][4][0]=7 son[4][4][1]=3 +c son[4][7][0]=8 son[4][7][1]=5 +c son[4][3][0]=6 son[4][3][1]=-1 +c son[4][8][0]=-1 son[4][8][1]=-1 +c son[4][5][0]=-1 son[4][5][1]=-1 +c son[4][6][0]=-1 son[4][6][1]=-1 +c son[5][5][0]=4 son[5][5][1]=6 +c son[5][4][0]=7 son[5][4][1]=8 +c son[5][6][0]=3 son[5][6][1]=-1 +c son[5][7][0]=-1 son[5][7][1]=-1 +c son[5][8][0]=-1 son[5][8][1]=-1 +c son[5][3][0]=-1 son[5][3][1]=-1 +c son[6][6][0]=8 son[6][6][1]=7 +c son[6][8][0]=5 son[6][8][1]=3 +c son[6][7][0]=4 son[6][7][1]=-1 +c son[6][5][0]=-1 son[6][5][1]=-1 +c son[6][3][0]=-1 son[6][3][1]=-1 +c son[6][4][0]=-1 son[6][4][1]=-1 +c son[7][7][0]=8 son[7][7][1]=4 +c son[7][8][0]=6 son[7][8][1]=3 +c son[7][4][0]=5 son[7][4][1]=-1 +c son[7][6][0]=-1 son[7][6][1]=-1 +c son[7][3][0]=-1 son[7][3][1]=-1 +c son[7][5][0]=-1 son[7][5][1]=-1 +c son[8][8][0]=7 son[8][8][1]=4 +c son[8][7][0]=6 son[8][7][1]=5 +c son[8][4][0]=3 son[8][4][1]=-1 +c son[8][6][0]=-1 son[8][6][1]=-1 +c son[8][5][0]=-1 son[8][5][1]=-1 +c son[8][3][0]=-1 son[8][3][1]=-1 +c index:11 number:16 seed:7 +c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] +c =========build tree========= +c son[1][1][0]=-1 son[1][1][1]=-1 +c son[2][2][0]=-1 son[2][2][1]=-1 +c son[3][3][0]=6 son[3][3][1]=8 +c son[3][6][0]=4 son[3][6][1]=5 +c son[3][8][0]=7 son[3][8][1]=-1 +c son[3][4][0]=-1 son[3][4][1]=-1 +c son[3][5][0]=-1 son[3][5][1]=-1 +c son[3][7][0]=-1 son[3][7][1]=-1 +c son[4][4][0]=7 son[4][4][1]=3 +c son[4][7][0]=8 son[4][7][1]=5 +c son[4][3][0]=6 son[4][3][1]=-1 +c son[4][8][0]=-1 son[4][8][1]=-1 +c son[4][5][0]=-1 son[4][5][1]=-1 +c son[4][6][0]=-1 son[4][6][1]=-1 +c son[5][5][0]=4 son[5][5][1]=6 +c son[5][4][0]=7 son[5][4][1]=8 +c son[5][6][0]=3 son[5][6][1]=-1 +c son[5][7][0]=-1 son[5][7][1]=-1 +c son[5][8][0]=-1 son[5][8][1]=-1 +c son[5][3][0]=-1 son[5][3][1]=-1 +c son[6][6][0]=8 son[6][6][1]=7 +c son[6][8][0]=5 son[6][8][1]=3 +c son[6][7][0]=4 son[6][7][1]=-1 +c son[6][5][0]=-1 son[6][5][1]=-1 +c son[6][3][0]=-1 son[6][3][1]=-1 +c son[6][4][0]=-1 son[6][4][1]=-1 +c son[7][7][0]=8 son[7][7][1]=4 +c son[7][8][0]=6 son[7][8][1]=3 +c son[7][4][0]=5 son[7][4][1]=-1 +c son[7][6][0]=-1 son[7][6][1]=-1 +c son[7][3][0]=-1 son[7][3][1]=-1 +c son[7][5][0]=-1 son[7][5][1]=-1 +c son[8][8][0]=7 son[8][8][1]=4 +c son[8][7][0]=6 son[8][7][1]=5 +c son[8][4][0]=3 son[8][4][1]=-1 +c son[8][6][0]=-1 son[8][6][1]=-1 +c son[8][5][0]=-1 son[8][5][1]=-1 +c son[8][3][0]=-1 son[8][3][1]=-1 +c node4(2)round 1, time: 0.0 +c node4(2) get 6835 exported lits from network +c node4 sharing nums: 1 +c sharing time: 0.00 +c node4 sharing received_num_by_network: 1997 +c node4 sharing skip_num_by_network: 0 +c node4 sharing unique reduce percentage: 0.00% +c [worker4] kissat exit with result: 0 +c node2(1)round 1, time: 0.0 +c node2(1) get 0 exported lits from network +c node2 sharing nums: 1 +c sharing time: 0.00 +c node2 sharing received_num_by_network: 0 +c node2 sharing skip_num_by_network: 0 +c node2 sharing unique reduce percentage: -nan% +c [worker2] kissat exit with result: 10 +c [worker2] getting terminate signal +c node1(0)round 1, time: 0.0 +c node1(0) get 0 exported lits from network +c node1 sharing nums: 1 +c sharing time: 0.00 +c node1 sharing received_num_by_network: 0 +c node1 sharing skip_num_by_network: 0 +c node1 sharing unique reduce percentage: -nan% +c [worker1] kissat exit with result: 10 +c [worker1] getting terminate signal +c node3(2)round 1, time: 0.0 +c node3(2) get 20985 exported lits from network +c node3 sharing nums: 1 +c sharing time: 0.00 +c node3 sharing received_num_by_network: 5906 +c node3 sharing skip_num_by_network: 0 +c node3 sharing unique reduce percentage: 0.00% +c [worker3] kissat exit with result: 10 +c [worker3] getting terminate signal +c node7(2)round 1, time: 0.0 +c node7(2) get 34928 exported lits from network +c node7 sharing nums: 1 +c sharing time: 0.01 +c node7 sharing received_num_by_network: 10690 +c node7 sharing skip_num_by_network: 1147 +c node7 sharing unique reduce percentage: 10.73% +c [worker7] kissat exit with result: 10 +c [worker7] getting terminate signal +c node8(2)round 1, time: 0.0 +c node8(2) get 0 exported lits from network +c node8 sharing nums: 1 +c sharing time: 0.00 +c node8 sharing received_num_by_network: 0 +c node8 sharing skip_num_by_network: 0 +c node8 sharing unique reduce percentage: -nan% +c [worker8] kissat exit with result: 10 +c [worker8] getting send model signal +c node6(2)round 1, time: 0.0 +c node6(2) get 0 exported lits from network +c node6 sharing nums: 1 +c sharing time: 0.00 +c node6 sharing received_num_by_network: 0 +c node6 sharing skip_num_by_network: 0 +c node6 sharing unique reduce percentage: -nan% +c [worker6] kissat exit with result: 0 +c [leader] received model size: 5675