diff --git a/experiment/cal.py b/experiment/cal.py index 57b93f5..02893bf 100755 --- a/experiment/cal.py +++ b/experiment/cal.py @@ -274,8 +274,12 @@ def gen_samples(dir): if __name__ == "__main__": solvers = [] # solvers.append(solver_SAT_standard_gnomon("/pub/netdisk1/qianyh/aws-batch-comp-infrastructure-sample/docker/runner/exp-result","mallob")) - solvers.append(solver_SAT_standard_gnomon("./light-3m-new-tree","light-3m-new-tree")) - solvers.append(solver_SAT_standard_gnomon("./light-3m-new-circle","light-3m-new-circle")) + solvers.append(solver_SAT_standard_gnomon("./light-3m-v3-tree","light-3m-v3-tree")) + solvers.append(solver_SAT_standard_gnomon("./light-3m-v3-circle","light-3m-v3-circle")) + solvers.append(solver_SAT_standard_gnomon("./light-3m-v2-tree","light-3m-v2-tree")) + solvers.append(solver_SAT_standard_gnomon("./light-3m-v2-circle","light-3m-v2-circle")) + # solvers.append(solver_SAT_standard_gnomon("./light-3m-new-tree","light-3m-new-tree")) + # solvers.append(solver_SAT_standard_gnomon("./light-3m-new-circle","light-3m-new-circle")) solvers.append(solver_SAT_standard_gnomon("./light-3m-no-pre","light-3m-no-pre")) solvers.append(solver_SAT_standard_gnomon("./light-3m","light-3m")) solvers.append(solver_SAT_standard_gnomon("./light-no-bug","light-no-bug")) diff --git a/hard1_dy_lbd.log b/hard1_dy_lbd.log new file mode 100644 index 0000000..d202624 --- /dev/null +++ b/hard1_dy_lbd.log @@ -0,0 +1,857 @@ +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 10.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 ./data/hard1.cnf "" CNF format instance +c -------------------------------------------------- +c [leader] preprocess(simplify) input data +c [GE] XORs: 2484 (time: 0.00) +c [GE] VAR SCC: 459 +c [GE] XOR SCCs: 23 (time: 0.00) +c [GE] unary xor: 0, bin xor: 0, bin added +c After preprocess: vars: 5034 -> 5031 , clauses: 21066 -> 21062 , +c [CE] almost one cons: 2550 +c len 0 +c sz 2 +c turns: 2 +c After preprocess: vars: 5031 -> 5024 , clauses: 21062 -> 21048 , +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:1 number:16 seed:7 +c index:1 number:16 seed:1 +c index:4 number:16 seed:1 +c index:13 number:16 seed:4 +c index:0 number:16 seed:7 +c index:2 number:16 seed:7 +c index:0 number:16 seed:6 +c index:12 number:16 seed:8 +c index:5 number:16 seed:7 +c index:4 number:16 seed:7 +c index:7 number:16 seed:7 +c index:13 number:16 seed:7 +c index:2 number:16 seed:4 +c index:9 number:16 seed:7 +c index:-1 number:-1 seed:-1 +c index:6 number:16 seed:8 +c index:2 number:16 seed:8 +c index:1 number:16 seed:8 +c index:3 number:16 seed:4 +c index:5 number:16 seed:8 +c index:3 number:16 seed:8 +c index:9 number:16 seed:8 +c index:14 number:16 seed:8 +c index:6 number:16 seed:7 +c index:3 number:16 seed:7 +c index:-1 number:-1 seed:-1 +c index:14 number:16 seed:7 +c index:8 number:16 seed:7 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:15 number:16 seed:7 +c index:7 number:16 seed:8 +c index:-1 number:-1 seed:-1 +c index:8 number:16 seed:8 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:1 number:16 seed:6 +c index:13 number:16 seed:8 +c index:5 number:16 seed:6 +c index:3 number:16 seed:5 +c index:0 number:16 seed:8 +c index:0 number:16 seed:5 +c index:1 number:16 seed:5 +c index:12 number:16 seed:7 +c index:10 number:16 seed:8 +c index:6 number:16 seed:4 +c index:8 number:16 seed:6 +c index:8 number:16 seed:5 +c index:15 number:16 seed:6 +c index:2 number:16 seed:6 +c index:9 number:16 seed:5 +c index:5 number:16 seed:5 +c index:7 number:16 seed:6 +c index:11 number:16 seed:8 +c index:2 number:16 seed:5 +c index:3 number:16 seed:6 +c index:6 number:16 seed:6 +c index:11 number:16 seed:6 +c index:15 number:16 seed:4 +c index:12 number:16 seed:6 +c index:14 number:16 seed:4 +c index:10 number:16 seed:6 +c index:4 number:16 seed:6 +c index:2 number:16 seed:1 +c index:0 number:16 seed:4 +c index:0 number:16 seed:1 +c index:8 number:16 seed:4 +c index:15 number:16 seed:1 +c index:1 number:16 seed:3 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:11 number:16 seed:4 +c index:11 number:16 seed:7 +c index:1 number:16 seed:4 +c index:-1 number:-1 seed:-1 +c index:15 number:16 seed:8 +c index:12 number:16 seed:3 +c index:4 number:16 seed:8 +c index:10 number:16 seed:3 +c index:4 number:16 seed:4 +c index:0 number:16 seed:3 +c index:11 number:16 seed:1 +c index:5 number:16 seed:1 +c index:5 number:16 seed:3 +c index:10 number:16 seed:1 +c index:12 number:16 seed:1 +c index:3 number:16 seed:1 +c index:13 number:16 seed:3 +c index:9 number:16 seed:4 +c index:12 number:16 seed:4 +c index:8 number:16 seed:1 +c index:6 number:16 seed:3 +c index:3 number:16 seed:3 +c index:13 number:16 seed:6 +c index:14 number:16 seed:6 +c index:9 number:16 seed:6 +c index:8 number:16 seed:3 +c index:4 number:16 seed:5 +c index:13 number:16 seed:1 +c index:2 number:16 seed:3 +c index:9 number:16 seed:3 +c index:7 number:16 seed:3 +c index:-1 number:-1 seed:-1 +c index:11 number:16 seed:3 +c index:4 number:16 seed:3 +c index:15 number:16 seed:3 +==============run1============ +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 +==============run2============ +c index:14 number:16 seed:3 +c index:10 number:16 seed:7 +c index:6 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:10 number:16 seed:4 +c index:5 number:16 seed:4 +==============run1============ +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 +==============run2============ +c index:10 number:16 seed:5 +c index:9 number:16 seed:1 +c index:7 number:16 seed:5 +c index:-1 number:-1 seed:-1 +c index:11 number:16 seed:5 +c index:12 number:16 seed:5 +c index:15 number:16 seed:5 +c index:7 number:16 seed:4 +c index:6 number:16 seed:5 +c index:14 number:16 seed:5 +c index:14 number:16 seed:1 +==============run1============ +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 +==============run2============ +c index:13 number:16 seed:5 +==============run1============ +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 +==============run2============ +==============run1============ +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 +==============run2============ +==============run1============ +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 +==============run2============ +c index:7 number:16 seed:1 +==============run1============ +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 +==============run2============ +==============run1============ +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 +==============run2============ +c node8(2)round 1, time: 0.0 +c node8(2) get 0 exported lits from network +c node6(2)round 1, time: 0.0 +c node6(2) get 0 exported lits from network +c node7(2)round 1, time: 0.0 +c node5(2)round 1, time: 0.0 +c node5(2) get 23647 exported lits from network +c node4(2)round 1, time: 0.0 +c node2(1)round 1, time: 0.0 +c node2(1) get 0 exported lits from network +c node1(0)round 1, time: 0.0 +c node1(0) get 0 exported lits from network +c node4(2) get 125788 exported lits from network +c node3(2)round 1, time: 0.0 +c node3(2) get 81158 exported lits from network +c node7(2) get 170616 exported lits from network +c node8(2)round 2, time: 0.506 +c node6(2)round 2, time: 0.506 +c node2(1)round 2, time: 0.505 +c node2(1) get 0 exported lits from network +c node5(2)round 2, time: 0.510 +c node5(2) get 90952 exported lits from network +c node1(0)round 2, time: 0.505 +c node1(0) get 0 exported lits from network +c node4(2)round 2, time: 0.529 +c node8(2) get 183670 exported lits from network +c node3(2)round 2, time: 0.518 +c node7(2)round 2, time: 0.567 +c node4(2) get 121277 exported lits from network +c node3(2) get 184066 exported lits from network +c node7(2) get 121393 exported lits from network +c node6(2) get 302903 exported lits from network +c node5(2)round 3, time: 1.29 +c node2(1)round 3, time: 1.31 +c node2(1) get 0 exported lits from network +c node1(0)round 3, time: 1.10 +c node1(0) get 0 exported lits from network +c node8(2)round 3, time: 1.52 +c node5(2) get 170959 exported lits from network +c node4(2)round 3, time: 1.67 +c node8(2) get 157957 exported lits from network +c node4(2) get 125299 exported lits from network +c node7(2)round 3, time: 1.110 +c node3(2)round 3, time: 1.81 +c node7(2) get 130818 exported lits from network +c node3(2) get 124419 exported lits from network +c node6(2)round 3, time: 1.160 +c node6(2) get 124140 exported lits from network +c node1(0)round 4, time: 1.514 +c node1(0) get 0 exported lits from network +c node2(1)round 4, time: 1.540 +c node2(1) get 0 exported lits from network +c node5(2)round 4, time: 1.572 +c node5(2) get 99768 exported lits from network +c node8(2)round 4, time: 1.604 +c node4(2)round 4, time: 1.604 +c node8(2) get 105248 exported lits from network +c node4(2) get 100991 exported lits from network +c node3(2)round 4, time: 1.608 +c node7(2)round 4, time: 1.650 +c node7(2) get 80139 exported lits from network +c node6(2)round 4, time: 1.693 +c node3(2) get 97617 exported lits from network +c node6(2) get 64480 exported lits from network +c node1(0)round 5, time: 2.18 +c node1(0) get 0 exported lits from network +c node2(1)round 5, time: 2.47 +c node2(1) get 0 exported lits from network +c node5(2)round 5, time: 2.95 +c node5(2) get 69823 exported lits from network +c node8(2)round 5, time: 2.132 +c node8(2) get 56914 exported lits from network +c node4(2)round 5, time: 2.134 +c node4(2) get 58001 exported lits from network +c node7(2)round 5, time: 2.177 +c node7(2) get 55128 exported lits from network +c node6(2)round 5, time: 2.209 +c node3(2)round 5, time: 2.171 +c node6(2) get 50992 exported lits from network +c node3(2) get 66346 exported lits from network +c node1(0)round 6, time: 2.522 +c node1(0) get 0 exported lits from network +c node2(1)round 6, time: 2.555 +c node2(1) get 0 exported lits from network +c node5(2)round 6, time: 2.608 +c node5(2) get 57021 exported lits from network +c node8(2)round 6, time: 2.647 +c node8(2) get 59128 exported lits from network +c node4(2)round 6, time: 2.648 +c node4(2) get 57336 exported lits from network +c node7(2)round 6, time: 2.694 +c node7(2) get 60415 exported lits from network +c node6(2)round 6, time: 2.724 +c node6(2) get 60425 exported lits from network +c node3(2)round 6, time: 2.697 +c node3(2) get 60149 exported lits from network +c node1(0)round 7, time: 3.26 +c node1(0) get 0 exported lits from network +c node2(1)round 7, time: 3.62 +c node2(1) get 0 exported lits from network +c node5(2)round 7, time: 3.120 +c node5(2) get 60983 exported lits from network +c node8(2)round 7, time: 3.162 +c node8(2) get 59112 exported lits from network +c node4(2)round 7, time: 3.162 +c node4(2) get 61378 exported lits from network +c node7(2)round 7, time: 3.225 +c node6(2)round 7, time: 3.240 +c node7(2) get 70546 exported lits from network +c node6(2) get 62989 exported lits from network +c node3(2)round 7, time: 3.211 +c node3(2) get 69145 exported lits from network +c node1(0)round 8, time: 3.529 +c node1(0) get 0 exported lits from network +c node2(1)round 8, time: 3.568 +c node2(1) get 0 exported lits from network +c node5(2)round 8, time: 3.632 +c node5(2) get 66160 exported lits from network +c node8(2)round 8, time: 3.677 +c node8(2) get 77893 exported lits from network +c node4(2)round 8, time: 3.693 +c node4(2) get 69165 exported lits from network +c node7(2)round 8, time: 3.751 +c node6(2)round 8, time: 3.771 +c node7(2) get 68901 exported lits from network +c node3(2)round 8, time: 3.742 +c node3(2) get 76025 exported lits from network +c node6(2) get 97320 exported lits from network +c node1(0)round 9, time: 4.32 +c node1(0) get 0 exported lits from network +c node2(1)round 9, time: 4.74 +c node2(1) get 0 exported lits from network +c node5(2)round 9, time: 4.144 +c node5(2) get 77913 exported lits from network +c node8(2)round 9, time: 4.197 +c node8(2) get 76651 exported lits from network +c node4(2)round 9, time: 4.230 +c node4(2) get 64357 exported lits from network +c node7(2)round 9, time: 4.274 +c node6(2)round 9, time: 4.308 +c node7(2) get 69597 exported lits from network +c node6(2) get 52530 exported lits from network +c node3(2)round 9, time: 4.275 +c node3(2) get 66816 exported lits from network +c node1(0)round 10, time: 4.535 +c node1(0) get 0 exported lits from network +c node2(1)round 10, time: 4.579 +c node2(1) get 0 exported lits from network +c node5(2)round 10, time: 4.658 +c node5(2) get 71087 exported lits from network +c node8(2)round 10, time: 4.726 +c node8(2) get 61109 exported lits from network +c node4(2)round 10, time: 4.744 +c node4(2) get 66448 exported lits from network +c node7(2)round 10, time: 4.810 +c node6(2)round 10, time: 4.822 +c node6(2) get 52011 exported lits from network +c node7(2) get 72677 exported lits from network +c node3(2)round 10, time: 4.804 +c node3(2) get 63557 exported lits from network +c node1(0)round 11, time: 5.38 +c node1(0) get 0 exported lits from network +c node2(1)round 11, time: 5.84 +c node2(1) get 0 exported lits from network +c node5(2)round 11, time: 5.170 +c node5(2) get 64559 exported lits from network +c node8(2)round 11, time: 5.255 +c node8(2) get 61146 exported lits from network +c node4(2)round 11, time: 5.256 +c node4(2) get 65257 exported lits from network +c node7(2)round 11, time: 5.335 +c node6(2)round 11, time: 5.343 +c node7(2) get 36174 exported lits from network +c node6(2) get 57534 exported lits from network +c node3(2)round 11, time: 5.317 +c node3(2) get 49360 exported lits from network +c node1(0)round 12, time: 5.543 +c node1(0) get 0 exported lits from network +c node2(1)round 12, time: 5.590 +c node2(1) get 0 exported lits from network +c node5(2)round 12, time: 5.681 +c node5(2) get 54516 exported lits from network +c node8(2)round 12, time: 5.766 +c node8(2) get 39853 exported lits from network +c node4(2)round 12, time: 5.788 +c node4(2) get 38566 exported lits from network +c node7(2)round 12, time: 5.845 +c node6(2)round 12, time: 5.855 +c node6(2) get 38435 exported lits from network +c node3(2)round 12, time: 5.826 +c node7(2) get 47685 exported lits from network +c node3(2) get 41254 exported lits from network +c node1(0)round 13, time: 6.46 +c node1(0) get 0 exported lits from network +c node2(1)round 13, time: 6.97 +c node2(1) get 0 exported lits from network +c node5(2)round 13, time: 6.191 +c node5(2) get 40988 exported lits from network +c node8(2)round 13, time: 6.275 +c node8(2) get 45536 exported lits from network +c node4(2)round 13, time: 6.298 +c node4(2) get 51903 exported lits from network +c node7(2)round 13, time: 6.369 +c node7(2) get 42424 exported lits from network +c node3(2)round 13, time: 6.367 +c node3(2) get 38582 exported lits from network +c node6(2)round 13, time: 6.427 +c node6(2) get 68472 exported lits from network +c node1(0)round 14, time: 6.548 +c node1(0) get 0 exported lits from network +c node2(1)round 14, time: 6.602 +c node2(1) get 0 exported lits from network +c node5(2)round 14, time: 6.730 +c node5(2) get 56336 exported lits from network +c node8(2)round 14, time: 6.802 +c node8(2) get 50387 exported lits from network +c node4(2)round 14, time: 6.838 +c node4(2) get 51384 exported lits from network +c node7(2)round 14, time: 6.877 +c node7(2) get 53386 exported lits from network +c node3(2)round 14, time: 6.874 +c node3(2) get 52883 exported lits from network +c node6(2)round 14, time: 6.946 +c node6(2) get 55719 exported lits from network +c node1(0)round 15, time: 7.50 +c node1(0) get 0 exported lits from network +c node2(1)round 15, time: 7.107 +c node2(1) get 0 exported lits from network +c node5(2)round 15, time: 7.239 +c node5(2) get 53943 exported lits from network +c node8(2)round 15, time: 7.312 +c node8(2) get 59520 exported lits from network +c node4(2)round 15, time: 7.351 +c node4(2) get 58256 exported lits from network +c node7(2)round 15, time: 7.387 +c node7(2) get 60736 exported lits from network +c node3(2)round 15, time: 7.382 +c node3(2) get 58897 exported lits from network +c node6(2)round 15, time: 7.458 +c node6(2) get 64902 exported lits from network +c node1(0)round 16, time: 7.552 +c node1(0) get 0 exported lits from network +c node2(1)round 16, time: 7.616 +c node2(1) get 0 exported lits from network +c node5(2)round 16, time: 7.748 +c node5(2) get 61246 exported lits from network +c node8(2)round 16, time: 7.824 +c node8(2) get 66458 exported lits from network +c node4(2)round 16, time: 7.864 +c node4(2) get 66008 exported lits from network +c node7(2)round 16, time: 7.900 +c node7(2) get 65606 exported lits from network +c node3(2)round 16, time: 7.893 +c node3(2) get 63397 exported lits from network +c node6(2)round 16, time: 7.968 +c node6(2) get 67693 exported lits from network +c node1(0)round 17, time: 8.55 +c node1(0) get 0 exported lits from network +c node2(1)round 17, time: 8.122 +c node2(1) get 0 exported lits from network +c node5(2)round 17, time: 8.259 +c node5(2) get 62600 exported lits from network +c node8(2)round 17, time: 8.335 +c node8(2) get 65095 exported lits from network +c node4(2)round 17, time: 8.376 +c node4(2) get 58597 exported lits from network +c node7(2)round 17, time: 8.412 +c node7(2) get 57192 exported lits from network +c node3(2)round 17, time: 8.403 +c node3(2) get 60927 exported lits from network +c node6(2)round 17, time: 8.481 +c node6(2) get 58259 exported lits from network +c node1(0)round 18, time: 8.557 +c node1(0) get 0 exported lits from network +c node2(1)round 18, time: 8.625 +c node2(1) get 0 exported lits from network +c node5(2)round 18, time: 8.768 +c node5(2) get 57514 exported lits from network +c node8(2)round 18, time: 8.849 +c node8(2) get 57738 exported lits from network +c node4(2)round 18, time: 8.889 +c node4(2) get 55550 exported lits from network +c node7(2)round 18, time: 8.941 +c node7(2) get 51244 exported lits from network +c node3(2)round 18, time: 8.914 +c node3(2) get 54898 exported lits from network +c node6(2)round 18, time: 8.992 +c node6(2) get 52403 exported lits from network +c node1(0)round 19, time: 9.59 +c node1(0) get 0 exported lits from network +c node2(1)round 19, time: 9.130 +c node2(1) get 0 exported lits from network +c node5(2)round 19, time: 9.279 +c node5(2) get 52782 exported lits from network +c node5 sharing nums: 19 +c sharing time: 0.28 +c node5 sharing received_num_by_network: 182928 +c node5 sharing skip_num_by_network: 2714 +c node5 sharing unique reduce percentage: 1.48% +c [worker5] kissat exit with result: 0 +c node8(2)round 19, time: 9.360 +c node8(2) get 49807 exported lits from network +c node8 sharing nums: 19 +c sharing time: 0.36 +c node8 sharing received_num_by_network: 197227 +c node8 sharing skip_num_by_network: 11663 +c node8 sharing unique reduce percentage: 5.91% +c [worker8] kissat exit with result: 0 +c [leader] solve time out +c node4(2)round 19, time: 9.401 +c node4(2) get 50577 exported lits from network +c node4 sharing nums: 19 +c sharing time: 0.40 +c node4 sharing received_num_by_network: 200493 +c node4 sharing skip_num_by_network: 9428 +c node4 sharing unique reduce percentage: 4.70% +c [worker4] kissat exit with result: 0 +c node7(2)round 19, time: 9.451 +c node7(2) get 48949 exported lits from network +c node7 sharing nums: 19 +c sharing time: 0.45 +c node7 sharing received_num_by_network: 204320 +c node7 sharing skip_num_by_network: 10788 +c node7 sharing unique reduce percentage: 5.28% +c [worker7] kissat exit with result: 0 +c node3(2)round 19, time: 9.423 +c node3(2) get 49984 exported lits from network +c node3 sharing nums: 19 +c sharing time: 0.42 +c node3 sharing received_num_by_network: 193513 +c node3 sharing skip_num_by_network: 2745 +c node3 sharing unique reduce percentage: 1.42% +c [worker3] kissat exit with result: 0 +c node6(2)round 19, time: 9.504 +c node6(2) get 49917 exported lits from network +c node6 sharing nums: 19 +c sharing time: 0.50 +c node6 sharing received_num_by_network: 202730 +c node6 sharing skip_num_by_network: 10499 +c node6 sharing unique reduce percentage: 5.18% +c [worker6] kissat exit with result: 0 +c node1(0)round 20, time: 9.561 +c node1(0) get 0 exported lits from network +c node1 sharing nums: 20 +c sharing time: 0.05 +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: 0 +c node2(1)round 20, time: 9.635 +c node2(1) get 0 exported lits from network +c node2 sharing nums: 20 +c sharing time: 0.13 +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: 0 +s UNKNOWN diff --git a/hard1_lbd2.log b/hard1_lbd2.log new file mode 100644 index 0000000..34b0696 --- /dev/null +++ b/hard1_lbd2.log @@ -0,0 +1,858 @@ +mpicxx -std=c++17 -O3 -Wall -Wextra -MMD -MP -march=native -mtune=native -g -c src/sharer.cpp -o build/./src/sharer.cpp.o -Wl,-Bstatic -lkissat -L kissat-inc/build -I kissat-inc/ -lm4ri -L m4ri-20140914/.libs -I m4ri-20140914/ -pthread -lz -lm -lboost_thread -lboost_date_time -lboost_system -Wl,-Bdynamic -lmpi_cxx -lmpi +mpicxx -std=c++17 -O3 -Wall -Wextra -MMD -MP -march=native -mtune=native -g build/./src/utils/parse.cpp.o build/./src/utils/hashmap.cpp.o build/./src/paras.cpp.o build/./src/main.cpp.o build/./src/preprocess/card.cpp.o build/./src/preprocess/preprocess.cpp.o build/./src/preprocess/resolution.cpp.o build/./src/preprocess/propagation.cpp.o build/./src/preprocess/gauss.cpp.o build/./src/preprocess/binary.cpp.o build/./src/solve.cpp.o build/./src/solver_api/basekissat.cpp.o build/./src/solver_api/basesolver.cpp.o build/./src/light.cpp.o build/./src/sharer.cpp.o -o light -Wl,-Bstatic -lkissat -L kissat-inc/build -I kissat-inc/ -lm4ri -L m4ri-20140914/.libs -I m4ri-20140914/ -pthread -lz -lm -lboost_thread -lboost_date_time -lboost_system -Wl,-Bdynamic -lmpi_cxx -lmpi +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 10.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 ./data/hard1.cnf "" CNF format instance +c -------------------------------------------------- +c [leader] preprocess(simplify) input data +c [GE] XORs: 2484 (time: 0.00) +c [GE] VAR SCC: 459 +c [GE] XOR SCCs: 23 (time: 0.00) +c [GE] unary xor: 0, bin xor: 0, bin added +c After preprocess: vars: 5034 -> 5031 , clauses: 21066 -> 21062 , +c [CE] almost one cons: 2550 +c len 0 +c sz 2 +c turns: 2 +c After preprocess: vars: 5031 -> 5024 , clauses: 21062 -> 21048 , +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:-1 number:-1 seed:-1 +c index:0 number:16 seed:7 +c index:10 number:16 seed:3 +c index:14 number:16 seed:3 +c index:0 number:16 seed:8 +c index:2 number:16 seed:7 +c index:-1 number:-1 seed:-1 +c index:1 number:16 seed:1 +c index:0 number:16 seed:1 +c index:1 number:16 seed:8 +c index:5 number:16 seed:8 +c index:2 number:16 seed:5 +c index:7 number:16 seed:5 +c index:0 number:16 seed:5 +c index:6 number:16 seed:7 +c index:9 number:16 seed:5 +c index:12 number:16 seed:7 +c index:8 number:16 seed:7 +c index:11 number:16 seed:7 +c index:13 number:16 seed:7 +c index:9 number:16 seed:7 +c index:3 number:16 seed:1 +c index:15 number:16 seed:8 +c index:9 number:16 seed:8 +c index:6 number:16 seed:1 +c index:7 number:16 seed:1 +c index:4 number:16 seed:8 +c index:13 number:16 seed:8 +c index:8 number:16 seed:8 +c index:1 number:16 seed:4 +c index:14 number:16 seed:1 +c index:10 number:16 seed:8 +c index:6 number:16 seed:8 +c index:2 number:16 seed:8 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:13 number:16 seed:1 +c index:4 number:16 seed:4 +c index:6 number:16 seed:4 +c index:9 number:16 seed:1 +c index:7 number:16 seed:4 +c index:3 number:16 seed:4 +c index:11 number:16 seed:4 +c index:10 number:16 seed:4 +c index:2 number:16 seed:4 +c index:15 number:16 seed:1 +c index:11 number:16 seed:8 +c index:3 number:16 seed:8 +c index:0 number:16 seed:4 +c index:1 number:16 seed:5 +c index:3 number:16 seed:7 +c index:-1 number:-1 seed:-1 +c index:15 number:16 seed:4 +c index:12 number:16 seed:4 +c index:14 number:16 seed:4 +c index:5 number:16 seed:5 +c index:3 number:16 seed:5 +c index:5 number:16 seed:1 +c index:5 number:16 seed:7 +c index:4 number:16 seed:7 +c index:7 number:16 seed:7 +c index:7 number:16 seed:8 +c index:2 number:16 seed:1 +c index:11 number:16 seed:1 +c index:9 number:16 seed:6 +c index:11 number:16 seed:5 +c index:6 number:16 seed:6 +c index:15 number:16 seed:6 +c index:12 number:16 seed:6 +c index:12 number:16 seed:8 +c index:10 number:16 seed:1 +c index:-1 number:-1 seed:-1 +c index:14 number:16 seed:8 +c index:1 number:16 seed:7 +c index:12 number:16 seed:1 +c index:6 number:16 seed:5 +c index:3 number:16 seed:3 +c index:0 number:16 seed:3 +c index:5 number:16 seed:3 +c index:15 number:16 seed:5 +c index:1 number:16 seed:6 +c index:3 number:16 seed:6 +c index:7 number:16 seed:6 +c index:8 number:16 seed:1 +c index:10 number:16 seed:7 +c index:7 number:16 seed:3 +c index:-1 number:-1 seed:-1 +c index:8 number:16 seed:4 +c index:15 number:16 seed:7 +c index:4 number:16 seed:1 +c index:5 number:16 seed:4 +c index:9 number:16 seed:4 +c index:5 number:16 seed:6 +c index:10 number:16 seed:6 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:8 number:16 seed:5 +c index:13 number:16 seed:5 +c index:0 number:16 seed:6 +c index:4 number:16 seed:5 +c index:2 number:16 seed:6 +c index:-1 number:-1 seed:-1 +c index:8 number:16 seed:6 +c index:2 number:16 seed:3 +c index:14 number:16 seed:7 +c index:13 number:16 seed:4 +c index:14 number:16 seed:5 +c index:4 number:16 seed:3 +c index:1 number:16 seed:3 +c index:12 number:16 seed:3 +c index:13 number:16 seed:3 +c index:9 number:16 seed:3 +c index:4 number:16 seed:6 +c index:13 number:16 seed:6 +==============run1============ +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]=8c index:-1 number:-1 seed:-1 + 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]=-1c index:-1 number:-1 seed:-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 +==============run2============ +c index:6 number:16 seed:3 +c index:8 number:16 seed:3 +c index:15 number:16 seed:3 +c index:11 number:16 seed:3 +==============run1============ +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 index:12 number:16 seed:5 +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 +==============run2============ +==============run1============ +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 +==============run2============ +c index:10 number:16 seed:5 +c index:11 number:16 seed:6 +c index:14 number:16 seed:6 +==============run1============ +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 +==============run2============ +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +c index:-1 number:-1 seed:-1 +==============run1============ +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 +==============run2============ +==============run1============ +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 +==============run2============ +==============run1============ +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 +==============run2============ +==============run1============ +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 +==============run2============ +c node8(2)round 1, time: 0.0 +c node8(2) get 0 exported lits from network +c node1(0)round 1, time: 0.0 +c node1(0) get 0 exported lits from network +c node7(2)round 1, time: 0.0 +c node4(2)round 1, time: 0.0 +c node5(2)round 1, time: 0.0 +c node3(2)round 1, time: 0.0 +c node2(1)round 1, time: 0.0 +c node2(1) get 0 exported lits from network +c node7(2) get 61475 exported lits from network +c node3(2) get 57542 exported lits from network +c node5(2) get 70894 exported lits from network +c node6(2)round 1, time: 0.0 +c node4(2) get 169407 exported lits from network +c node6(2) get 146781 exported lits from network +c node1(0)round 2, time: 0.505 +c node1(0) get 0 exported lits from network +c node8(2)round 2, time: 0.507 +c node2(1)round 2, time: 0.508 +c node2(1) get 0 exported lits from network +c node7(2)round 2, time: 0.522 +c node5(2)round 2, time: 0.520 +c node5(2) get 96220 exported lits from network +c node3(2)round 2, time: 0.539 +c node8(2) get 158779 exported lits from network +c node7(2) get 180201 exported lits from network +c node4(2)round 2, time: 0.570 +c node3(2) get 167960 exported lits from network +c node6(2)round 2, time: 0.568 +c node4(2) get 147417 exported lits from network +c node6(2) get 169923 exported lits from network +c node1(0)round 3, time: 1.10 +c node1(0) get 0 exported lits from network +c node2(1)round 3, time: 1.25 +c node2(1) get 0 exported lits from network +c node5(2)round 3, time: 1.58 +c node8(2)round 3, time: 1.68 +c node7(2)round 3, time: 1.90 +c node5(2) get 151592 exported lits from network +c node3(2)round 3, time: 1.96 +c node8(2) get 160986 exported lits from network +c node4(2)round 3, time: 1.123 +c node7(2) get 132887 exported lits from network +c node3(2) get 146068 exported lits from network +c node6(2)round 3, time: 1.124 +c node4(2) get 121030 exported lits from network +c node6(2) get 121107 exported lits from network +c node1(0)round 4, time: 1.516 +c node1(0) get 0 exported lits from network +c node2(1)round 4, time: 1.531 +c node2(1) get 0 exported lits from network +c node5(2)round 4, time: 1.600 +c node8(2)round 4, time: 1.626 +c node7(2)round 4, time: 1.632 +c node5(2) get 96047 exported lits from network +c node3(2)round 4, time: 1.640 +c node7(2) get 92408 exported lits from network +c node8(2) get 135708 exported lits from network +c node3(2) get 113665 exported lits from network +c node4(2)round 4, time: 1.694 +c node4(2) get 75871 exported lits from network +c node6(2)round 4, time: 1.696 +c node6(2) get 78695 exported lits from network +c node1(0)round 5, time: 2.19 +c node1(0) get 0 exported lits from network +c node2(1)round 5, time: 2.38 +c node2(1) get 0 exported lits from network +c node5(2)round 5, time: 2.133 +c node5(2) get 63142 exported lits from network +c node7(2)round 5, time: 2.168 +c node7(2) get 51839 exported lits from network +c node8(2)round 5, time: 2.178 +c node3(2)round 5, time: 2.174 +c node8(2) get 62574 exported lits from network +c node3(2) get 61814 exported lits from network +c node4(2)round 5, time: 2.217 +c node4(2) get 63967 exported lits from network +c node6(2)round 5, time: 2.223 +c node6(2) get 65534 exported lits from network +c node1(0)round 6, time: 2.523 +c node1(0) get 0 exported lits from network +c node2(1)round 6, time: 2.544 +c node2(1) get 0 exported lits from network +c node5(2)round 6, time: 2.647 +c node5(2) get 65327 exported lits from network +c node7(2)round 6, time: 2.679 +c node7(2) get 61918 exported lits from network +c node8(2)round 6, time: 2.710 +c node3(2)round 6, time: 2.711 +c node3(2) get 61493 exported lits from network +c node8(2) get 68462 exported lits from network +c node4(2)round 6, time: 2.736 +c node4(2) get 65870 exported lits from network +c node6(2)round 6, time: 2.738 +c node6(2) get 67926 exported lits from network +c node1(0)round 7, time: 3.26 +c node1(0) get 0 exported lits from network +c node2(1)round 7, time: 3.48 +c node2(1) get 0 exported lits from network +c node5(2)round 7, time: 3.174 +c node5(2) get 60817 exported lits from network +c node7(2)round 7, time: 3.201 +c node7(2) get 67941 exported lits from network +c node8(2)round 7, time: 3.241 +c node3(2)round 7, time: 3.235 +c node4(2)round 7, time: 3.254 +c node3(2) get 52426 exported lits from network +c node4(2) get 56851 exported lits from network +c node8(2) get 102288 exported lits from network +c node6(2)round 7, time: 3.272 +c node6(2) get 72854 exported lits from network +c node1(0)round 8, time: 3.528 +c node1(0) get 0 exported lits from network +c node2(1)round 8, time: 3.553 +c node2(1) get 0 exported lits from network +c node5(2)round 8, time: 3.707 +c node7(2)round 8, time: 3.717 +c node7(2) get 94910 exported lits from network +c node5(2) get 103849 exported lits from network +c node3(2)round 8, time: 3.760 +c node3(2) get 53356 exported lits from network +c node4(2)round 8, time: 3.786 +c node8(2)round 8, time: 3.797 +c node8(2) get 79186 exported lits from network +c node4(2) get 90767 exported lits from network +c node6(2)round 8, time: 3.800 +c node6(2) get 80368 exported lits from network +c node1(0)round 9, time: 4.31 +c node1(0) get 0 exported lits from network +c node2(1)round 9, time: 4.57 +c node2(1) get 0 exported lits from network +c node7(2)round 9, time: 4.254 +c node5(2)round 9, time: 4.248 +c node7(2) get 71819 exported lits from network +c node5(2) get 77702 exported lits from network +c node3(2)round 9, time: 4.302 +c node8(2)round 9, time: 4.319 +c node4(2)round 9, time: 4.326 +c node8(2) get 51759 exported lits from network +c node4(2) get 59968 exported lits from network +c node6(2)round 9, time: 4.320 +c node3(2) get 145316 exported lits from network +c node6(2) get 75791 exported lits from network +c node1(0)round 10, time: 4.533 +c node1(0) get 0 exported lits from network +c node2(1)round 10, time: 4.561 +c node2(1) get 0 exported lits from network +c node7(2)round 10, time: 4.775 +c node5(2)round 10, time: 4.769 +c node7(2) get 45341 exported lits from network +c node5(2) get 64543 exported lits from network +c node8(2)round 10, time: 4.842 +c node4(2)round 10, time: 4.844 +c node8(2) get 53761 exported lits from network +c node4(2) get 55729 exported lits from network +c node3(2)round 10, time: 4.862 +c node6(2)round 10, time: 4.838 +c node6(2) get 36639 exported lits from network +c node3(2) get 63265 exported lits from network +c node1(0)round 11, time: 5.36 +c node1(0) get 0 exported lits from network +c node2(1)round 11, time: 5.65 +c node2(1) get 0 exported lits from network +c node7(2)round 11, time: 5.287 +c node5(2)round 11, time: 5.282 +c node7(2) get 52782 exported lits from network +c node5(2) get 46506 exported lits from network +c node8(2)round 11, time: 5.353 +c node4(2)round 11, time: 5.357 +c node8(2) get 50676 exported lits from network +c node4(2) get 31544 exported lits from network +c node6(2)round 11, time: 5.345 +c node6(2) get 42762 exported lits from network +c node3(2)round 11, time: 5.387 +c node3(2) get 40729 exported lits from network +c node1(0)round 12, time: 5.540 +c node1(0) get 0 exported lits from network +c node2(1)round 12, time: 5.569 +c node2(1) get 0 exported lits from network +c node7(2)round 12, time: 5.798 +c node5(2)round 12, time: 5.793 +c node7(2) get 45529 exported lits from network +c node5(2) get 44821 exported lits from network +c node8(2)round 12, time: 5.866 +c node4(2)round 12, time: 5.866 +c node6(2)round 12, time: 5.855 +c node3(2)round 12, time: 5.897 +c node8(2) get 50559 exported lits from network +c node3(2) get 28134 exported lits from network +c node4(2) get 44377 exported lits from network +c node6(2) get 49071 exported lits from network +c node1(0)round 13, time: 6.42 +c node1(0) get 0 exported lits from network +c node2(1)round 13, time: 6.72 +c node2(1) get 0 exported lits from network +c node7(2)round 13, time: 6.308 +c node5(2)round 13, time: 6.305 +c node7(2) get 44523 exported lits from network +c node5(2) get 50818 exported lits from network +c node3(2)round 13, time: 6.418 +c node4(2)round 13, time: 6.425 +c node8(2)round 13, time: 6.433 +c node3(2) get 14873 exported lits from network +c node4(2) get 45590 exported lits from network +c node8(2) get 55860 exported lits from network +c node6(2)round 13, time: 6.423 +c node6(2) get 46575 exported lits from network +c node1(0)round 14, time: 6.545 +c node1(0) get 0 exported lits from network +c node2(1)round 14, time: 6.575 +c node2(1) get 0 exported lits from network +c node7(2)round 14, time: 6.833 +c node7(2) get 58604 exported lits from network +c node5(2)round 14, time: 6.877 +c node5(2) get 49441 exported lits from network +c node3(2)round 14, time: 6.924 +c node4(2)round 14, time: 6.935 +c node3(2) get 38068 exported lits from network +c node8(2)round 14, time: 6.944 +c node4(2) get 56345 exported lits from network +c node8(2) get 60247 exported lits from network +c node6(2)round 14, time: 6.934 +c node6(2) get 60786 exported lits from network +c node1(0)round 15, time: 7.47 +c node1(0) get 0 exported lits from network +c node2(1)round 15, time: 7.78 +c node2(1) get 0 exported lits from network +c node7(2)round 15, time: 7.352 +c node7(2) get 66476 exported lits from network +c node5(2)round 15, time: 7.389 +c node5(2) get 61963 exported lits from network +c node3(2)round 15, time: 7.433 +c node3(2) get 58654 exported lits from network +c node4(2)round 15, time: 7.448 +c node8(2)round 15, time: 7.455 +c node8(2) get 60684 exported lits from network +c node4(2) get 77573 exported lits from network +c node6(2)round 15, time: 7.446 +c node6(2) get 62870 exported lits from network +c node1(0)round 16, time: 7.549 +c node1(0) get 0 exported lits from network +c node2(1)round 16, time: 7.581 +c node2(1) get 0 exported lits from network +c node7(2)round 16, time: 7.862 +c node7(2) get 63902 exported lits from network +c node5(2)round 16, time: 7.915 +c node5(2) get 62018 exported lits from network +c node3(2)round 16, time: 7.944 +c node3(2) get 75642 exported lits from network +c node8(2)round 16, time: 7.968 +c node8(2) get 46504 exported lits from network +c node4(2)round 16, time: 7.978 +c node4(2) get 58550 exported lits from network +c node6(2)round 16, time: 7.959 +c node6(2) get 65241 exported lits from network +c node1(0)round 17, time: 8.51 +c node1(0) get 0 exported lits from network +c node2(1)round 17, time: 8.84 +c node2(1) get 0 exported lits from network +c node7(2)round 17, time: 8.377 +c node7(2) get 57430 exported lits from network +c node5(2)round 17, time: 8.429 +c node5(2) get 58363 exported lits from network +c node3(2)round 17, time: 8.456 +c node3(2) get 60027 exported lits from network +c node8(2)round 17, time: 8.480 +c node8(2) get 59134 exported lits from network +c node6(2)round 17, time: 8.472 +c node4(2)round 17, time: 8.509 +c node6(2) get 62654 exported lits from network +c node4(2) get 70297 exported lits from network +c node1(0)round 18, time: 8.553 +c node1(0) get 0 exported lits from network +c node2(1)round 18, time: 8.586 +c node2(1) get 0 exported lits from network +c node7(2)round 18, time: 8.888 +c node7(2) get 55080 exported lits from network +c node5(2)round 18, time: 8.942 +c node5(2) get 60046 exported lits from network +c node8(2)round 18, time: 8.991 +c node3(2)round 18, time: 8.981 +c node8(2) get 46316 exported lits from network +c node3(2) get 82408 exported lits from network +c node6(2)round 18, time: 8.985 +c node6(2) get 56658 exported lits from network +c node4(2)round 18, time: 9.40 +c node4(2) get 54840 exported lits from network +c node1(0)round 19, time: 9.55 +c node1(0) get 0 exported lits from network +c node2(1)round 19, time: 9.89 +c node2(1) get 0 exported lits from network +c node7(2)round 19, time: 9.400 +c node7(2) get 40907 exported lits from network +c [leader] solve time out +c node7 sharing nums: 19 +c sharing time: 0.40 +c node7 sharing received_num_by_network: 194696 +c node7 sharing skip_num_by_network: 5216 +c node7 sharing unique reduce percentage: 2.68% +c [worker7] kissat exit with result: 0 +c node5(2)round 19, time: 9.454 +c node5(2) get 55197 exported lits from network +c node5 sharing nums: 19 +c sharing time: 0.45 +c node5 sharing received_num_by_network: 191266 +c node5 sharing skip_num_by_network: 3130 +c node5 sharing unique reduce percentage: 1.64% +c [worker5] kissat exit with result: 0 +c node8(2)round 19, time: 9.504 +c node3(2)round 19, time: 9.498 +c node8(2) get 48048 exported lits from network +c node8 sharing nums: 19 +c sharing time: 0.50 +c node8 sharing received_num_by_network: 190352 +c node8 sharing skip_num_by_network: 4089 +c node8 sharing unique reduce percentage: 2.15% +c [worker8] kissat exit with result: 0 +c node3(2) get 46609 exported lits from network +c node3 sharing nums: 19 +c sharing time: 0.50 +c node3 sharing received_num_by_network: 194710 +c node3 sharing skip_num_by_network: 2648 +c node3 sharing unique reduce percentage: 1.36% +c [worker3] kissat exit with result: 0 +c node6(2)round 19, time: 9.494 +c node6(2) get 46507 exported lits from network +c node6 sharing nums: 19 +c sharing time: 0.49 +c node6 sharing received_num_by_network: 202626 +c node6 sharing skip_num_by_network: 3727 +c node6 sharing unique reduce percentage: 1.84% +c [worker6] kissat exit with result: 0 +c node1(0)round 20, time: 9.556 +c node1(0) get 0 exported lits from network +c node4(2)round 19, time: 9.553 +c node1 sharing nums: 20 +c sharing time: 0.05 +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: 0 +c node4(2) get 44810 exported lits from network +c node4 sharing nums: 19 +c sharing time: 0.55 +c node4 sharing received_num_by_network: 203364 +c node4 sharing skip_num_by_network: 6532 +c node4 sharing unique reduce percentage: 3.21% +c [worker4] kissat exit with result: 0 +c node2(1)round 20, time: 9.592 +c node2(1) get 0 exported lits from network +c node2 sharing nums: 20 +c sharing time: 0.08 +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: 0 +s UNKNOWN diff --git a/run.sh b/run.sh index 3939a75..fd90dde 100755 --- a/run.sh +++ b/run.sh @@ -32,11 +32,8 @@ DIR=/pub/data/chenzh/data/sat2022 INSTANCE=3d2a6e5c2f8f58dee79fd50444009625-cfi-rigid-z2-0088-03-or_2_shuffle_all.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=1 +# 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=1 - - - -# 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 +make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i ./data/hard1.cnf --share=1 --threads=16 --times=10 #./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 diff --git a/src/sharer.cpp b/src/sharer.cpp index bc426cb..d974aad 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -235,7 +235,7 @@ void sharer::do_clause_sharing() { // 增加 lits 限制 int percent = sort_clauses(i); - if(S->worker_type == light::UNSAT) { + if(S->worker_type != light::SAT) { if (percent < 75) { producers[i]->broaden_export_limit(); }