fixed another bug
This commit is contained in:
ihan-o
parent
064c4be71c
commit
ae0516eb9c
@ -941,21 +941,21 @@ bool SimpSolver::gaussElim() { assert(decisionLevel() == 0);
|
||||
Stopwatch timer;
|
||||
|
||||
xors_found = searchXors(xors);
|
||||
printf("c [GE] XORs: %d (time: %.2f)\n", xors.size(), timer.tick());
|
||||
// printf("c [GE] XORs: %d (time: %.2f)\n", xors.size(), timer.tick());
|
||||
|
||||
int upper_limit = computeVarSccs(v2scc_id, var_sccs, xors);
|
||||
computeXorSccs(xor_sccs, xors, v2scc_id, var_sccs, upper_limit);
|
||||
printf("c [GE] XOR SCCs: %d (time: %.2f)\n", xor_sccs.size(), timer.tick());
|
||||
// printf("c [GE] XOR SCCs: %d (time: %.2f)\n", xor_sccs.size(), timer.tick());
|
||||
|
||||
ok = performGaussElim(xor_sccs);
|
||||
|
||||
for (int i = 0; i < xors.size(); i++) delete xors[i];
|
||||
for (int i = 0; i < xor_sccs.size(); i++) delete xor_sccs[i];
|
||||
|
||||
printf("c [GE] matrices: %d, unary xor: %d, bin xor: %d, bin added: %d (time: %.2f)\n",
|
||||
stat_gauss, stat_gauss_case1, stat_gauss_case2, stat_gauss_bin_added, timer.tick());
|
||||
// printf("c [GE] matrices: %d, unary xor: %d, bin xor: %d, bin added: %d (time: %.2f)\n",
|
||||
// stat_gauss, stat_gauss_case1, stat_gauss_case2, stat_gauss_bin_added, timer.tick());
|
||||
stat_gauss_time += timer.total();
|
||||
if (!ok) printf("c [GE] UNSAT\n");
|
||||
// if (!ok) printf("c [GE] UNSAT\n");
|
||||
|
||||
return ok;
|
||||
}
|
||||
|
||||
@ -1,341 +0,0 @@
|
||||
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 0 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 0 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/f1afd5e8d4b842c15c6a2c420b2b2dba-pj2018_k10.cnf "" CNF format instance
|
||||
c --------------------------------------------------
|
||||
c [leader] preprocess(simplify) input data
|
||||
c After preprocess: vars: 578145 -> 573298 , clauses: 1588617 -> 1569477 ,
|
||||
c len 5203
|
||||
c After preprocess: vars: 573298 -> 565733 , clauses: 1569477 -> 1561473 ,
|
||||
c [leader] length of cnf (bytes): 29837411
|
||||
c [leader] hand out length of cnf instance to all nodes
|
||||
c [leader] hand out cnf instance to all nodes
|
||||
c [worker4] threads per worker were set 16 by default : 0
|
||||
c [worker5] threads per worker were set 16 by default : 0
|
||||
c id is 0
|
||||
c id is 1
|
||||
c [worker6] threads per worker were set 16 by default : 0
|
||||
c id is 0
|
||||
c id is 1
|
||||
c [worker7] threads per worker were set 16 by default : 0
|
||||
c [worker8] threads per worker were set 16 by default : 0
|
||||
c id is 0
|
||||
c [leader] hand out done!
|
||||
c [worker1] threads per worker were set 16 by default : 0
|
||||
c id is 0
|
||||
c [worker2] threads per worker were set 16 by default : 0
|
||||
c id is 0
|
||||
c [worker3] threads per worker were set 16 by default : 0
|
||||
c id is 0
|
||||
c id is 1
|
||||
c id is 1
|
||||
c id is 1
|
||||
c id is 0
|
||||
c id is 1
|
||||
c id is 2
|
||||
c id is 3
|
||||
c id is 4
|
||||
c id is 2
|
||||
c id is 3
|
||||
c id is 4
|
||||
c id is 0
|
||||
c id is 1
|
||||
c id is 1
|
||||
c id is 2
|
||||
c id is 2
|
||||
c id is 3
|
||||
c id is 2
|
||||
c id is 3
|
||||
c id is 4
|
||||
c id is 5
|
||||
c id is 2
|
||||
c id is 3
|
||||
c id is 4
|
||||
c id is 2
|
||||
c id is 3
|
||||
c id is 4
|
||||
c id is 2
|
||||
c id is 3
|
||||
c id is 5
|
||||
c id is 6
|
||||
c id is 7
|
||||
c id is 8
|
||||
c id is 5
|
||||
c id is 6
|
||||
c id is 7
|
||||
c id is 8
|
||||
c id is 9
|
||||
c id is 3
|
||||
c id is 4
|
||||
c id is 10
|
||||
c id is 11
|
||||
c id is 4
|
||||
c id is 5
|
||||
c id is 6
|
||||
c id is 7
|
||||
c id is 8
|
||||
c id is 5
|
||||
c id is 6
|
||||
c id is 5
|
||||
c id is 6
|
||||
c id is 4
|
||||
c id is 5
|
||||
c id is 6
|
||||
c id is 9
|
||||
c id is 10
|
||||
c id is 11
|
||||
c id is 12
|
||||
c id is 5
|
||||
c id is 6
|
||||
c id is 9
|
||||
c id is 7
|
||||
c id is 8
|
||||
c id is 7
|
||||
c id is 8
|
||||
c id is 7
|
||||
c id is 8
|
||||
c id is 7
|
||||
c id is 8
|
||||
c id is 13
|
||||
c id is 14
|
||||
c id is 12
|
||||
c id is 13
|
||||
c id is 14
|
||||
c id is 15
|
||||
c maple configure 0
|
||||
c maple configure 1
|
||||
c maple configure 2
|
||||
c maple configure 3
|
||||
c maple configure 4
|
||||
c maple configure 5
|
||||
c maple configure 6
|
||||
c maple configure 7
|
||||
c id is 6
|
||||
c id is 7
|
||||
c id is 8
|
||||
c id is 9
|
||||
c id is 9
|
||||
c id is 15
|
||||
c maple configure 0
|
||||
c maple configure 1
|
||||
c maple configure 2
|
||||
c maple configure 3
|
||||
c maple configure 4
|
||||
c maple configure 5
|
||||
c maple configure 6
|
||||
c maple configure 7
|
||||
c maple configure 8
|
||||
c maple configure 8
|
||||
c maple configure 9
|
||||
c maple configure 10
|
||||
c maple configure 11
|
||||
c maple configure 12
|
||||
c maple configure 13
|
||||
c maple configure 14
|
||||
c maple configure 15
|
||||
c id is 9
|
||||
c id is 10
|
||||
c id is 10
|
||||
c id is 11
|
||||
c id is 12
|
||||
c id is 9
|
||||
c id is 10
|
||||
c id is 11
|
||||
c id is 9
|
||||
c id is 10
|
||||
c id is 11
|
||||
c id is 11
|
||||
c id is 12
|
||||
c id is 13
|
||||
c id is 13
|
||||
c id is 14
|
||||
c id is 15
|
||||
c id is 12
|
||||
c id is 13
|
||||
c id is 12
|
||||
c id is 13
|
||||
c id is 10
|
||||
c id is 11
|
||||
c id is 12
|
||||
c id is 10
|
||||
c id is 11
|
||||
c id is 12
|
||||
c id is 13
|
||||
c maple configure 9
|
||||
c maple configure 10
|
||||
c maple configure 11
|
||||
c maple configure 12
|
||||
c maple configure 13
|
||||
c maple configure 14
|
||||
c maple configure 15
|
||||
c id is 14
|
||||
c maple configure 0
|
||||
c maple configure 1
|
||||
c maple configure 2
|
||||
c maple configure 3
|
||||
c maple configure 4
|
||||
c maple configure 5
|
||||
c maple configure 6
|
||||
c maple configure 7
|
||||
c maple configure 8
|
||||
c maple configure 9
|
||||
c maple configure 10
|
||||
c maple configure 11
|
||||
c maple configure 12
|
||||
c maple configure 13
|
||||
c maple configure 14
|
||||
c maple configure 15
|
||||
c id is 14
|
||||
c id is 13
|
||||
c id is 14
|
||||
c id is 14
|
||||
c id is 15
|
||||
c id is 14
|
||||
c id is 15
|
||||
c maple configure 0
|
||||
c maple configure 1
|
||||
c id is 15
|
||||
c maple configure 0
|
||||
c maple configure 1
|
||||
c maple configure 2
|
||||
c maple configure 3
|
||||
c maple configure 4
|
||||
c maple configure 5
|
||||
c maple configure 6
|
||||
c maple configure 7
|
||||
c maple configure 8
|
||||
c maple configure 9
|
||||
c maple configure 10
|
||||
c maple configure 11
|
||||
c maple configure 12
|
||||
c maple configure 13
|
||||
c maple configure 14
|
||||
c maple configure 15
|
||||
c id is 15
|
||||
c maple configure 0
|
||||
c maple configure 1
|
||||
c maple configure 2
|
||||
c maple configure 3
|
||||
c maple configure 4
|
||||
c maple configure 5
|
||||
c maple configure 6
|
||||
c maple configure 7
|
||||
c maple configure 8
|
||||
c maple configure 9
|
||||
c maple configure 10
|
||||
c maple configure 11
|
||||
c maple configure 12
|
||||
c maple configure 13
|
||||
c maple configure 14
|
||||
c id is 15
|
||||
c maple configure 0
|
||||
c maple configure 1
|
||||
c maple configure 2
|
||||
c maple configure 3
|
||||
c maple configure 4
|
||||
c maple configure 5
|
||||
c maple configure 6
|
||||
c maple configure 7
|
||||
c maple configure 8
|
||||
c maple configure 9
|
||||
c maple configure 10
|
||||
c maple configure 11
|
||||
c maple configure 2
|
||||
c maple configure 3
|
||||
c maple configure 4
|
||||
c maple configure 5
|
||||
c maple configure 6
|
||||
c maple configure 7
|
||||
c maple configure 8
|
||||
c maple configure 9
|
||||
c maple configure 10
|
||||
c maple configure 11
|
||||
c maple configure 12
|
||||
c maple configure 13
|
||||
c maple configure 14
|
||||
c maple configure 15
|
||||
c maple configure 12
|
||||
c maple configure 13
|
||||
c maple configure 14
|
||||
c maple configure 15
|
||||
c maple configure 0
|
||||
c maple configure 1
|
||||
c maple configure 2
|
||||
c maple configure 3
|
||||
c maple configure 4
|
||||
c maple configure 5
|
||||
c maple configure 6
|
||||
c maple configure 7
|
||||
c maple configure 8
|
||||
c maple configure 9
|
||||
c maple configure 10
|
||||
c maple configure 11
|
||||
c maple configure 12
|
||||
c maple configure 13
|
||||
c maple configure 14
|
||||
c maple configure 15
|
||||
c maple configure 15
|
||||
c [GE] XORs: 0 (time: 0.71)
|
||||
c [GE] XOR SCCs: 0 (time: 0.00)
|
||||
c [GE] matrices: 0, unary xor: 0, bin xor: 0, bin added: 0 (time: 0.00)
|
||||
c [GE] XORs: 0 (time: 0.78)
|
||||
c [GE] XOR SCCs: 0 (time: 0.00)
|
||||
c [GE] matrices: 0, unary xor: 0, bin xor: 0, bin added: 0 (time: 0.00)
|
||||
c [GE] XORs: 0 (time: 0.68)
|
||||
c [GE] XOR SCCs: 0 (time: 0.00)
|
||||
c [GE] matrices: 0, unary xor: 0, bin xor: 0, bin added: 0 (time: 0.00)
|
||||
c [GE] XORs: 0 (time: 0.77)
|
||||
c [GE] XOR SCCs: 0 (time: 0.00)
|
||||
c [GE] matrices: 0, unary xor: 0, bin xor: 0, bin added: 0 (time: 0.00)
|
||||
c [GE] XORs: 0 (time: 0.87)
|
||||
c [GE] XOR SCCs: 0 (time: 0.00)
|
||||
c [GE] matrices: 0, unary xor: 0, bin xor: 0, bin added: 0 (time: 0.00)
|
||||
c [GE] XORs: 0 (time: 1.29)
|
||||
c [GE] XOR SCCs: 0 (time: 0.00)
|
||||
c [GE] matrices: 0, unary xor: 0, bin xor: 0, bin added: 0 (time: 0.00)
|
||||
c [GE] XORs: 0 (time: 1.10)
|
||||
c [GE] XOR SCCs: 0 (time: 0.00)
|
||||
c [GE] matrices: 0, unary xor: 0, bin xor: 0, bin added: 0 (time: 0.00)
|
||||
c [GE] XORs: 0 (time: 1.10)
|
||||
c [GE] XOR SCCs: 0 (time: 0.00)
|
||||
c [GE] matrices: 0, unary xor: 0, bin xor: 0, bin added: 0 (time: 0.00)
|
||||
c [GE] XORs: 1170 (time: 1.56)
|
||||
c [GE] XOR SCCs: 804 (time: 0.06)
|
||||
c [GE] matrices: 305, unary xor: 0, bin xor: 108, bin added: 216 (time: 0.24)
|
||||
c [GE] XORs: 1170 (time: 1.46)
|
||||
c [GE] XOR SCCs: 804 (time: 0.06)
|
||||
c [GE] matrices: 305, unary xor: 0, bin xor: 108, bin added: 216 (time: 0.31)
|
||||
c [GE] XORs: 1170 (time: 1.43)
|
||||
c [GE] XOR SCCs: 804 (time: 0.01)
|
||||
c [GE] matrices: 305, unary xor: 0, bin xor: 108, bin added: 216 (time: 0.54)
|
||||
c [GE] XORs: 1170 (time: 1.38)
|
||||
c [GE] XOR SCCs: 804 (time: 0.00)
|
||||
c [GE] matrices: 305, unary xor: 0, bin xor: 108, bin added: 216 (time: 0.25)
|
||||
c [GE] XORs: 1170 (time: 1.98)
|
||||
c [GE] XOR SCCs: 804 (time: 0.00)
|
||||
c [GE] matrices: 305, unary xor: 0, bin xor: 108, bin added: 216 (time: 0.63)
|
||||
c [GE] XORs: 1170 (time: 1.53)
|
||||
c [GE] XOR SCCs: 804 (time: 0.00)
|
||||
c [GE] matrices: 305, unary xor: 0, bin xor: 108, bin added: 216 (time: 0.32)
|
||||
c [GE] XORs: 1170 (time: 1.64)
|
||||
c [GE] XOR SCCs: 804 (time: 0.05)
|
||||
c [GE] matrices: 305, unary xor: 0, bin xor: 108, bin added: 216 (time: 0.43)
|
||||
c [GE] XORs: 1170 (time: 1.76)
|
||||
c [GE] XOR SCCs: 804 (time: 0.06)
|
||||
c [GE] matrices: 305, unary xor: 0, bin xor: 108, bin added: 216 (time: 0.41)
|
||||
File diff suppressed because one or more lines are too long
6
run.sh
6
run.sh
@ -21,9 +21,9 @@
|
||||
# - 367c25ad50259a685a25b86d6dd171b2-GP_100_950_33.cnf
|
||||
|
||||
# 这个存在问题
|
||||
DIR=/pub/data/chenzh/data/sat2022
|
||||
# INSTANCE=tseitingrid7x165_shuffled.cnf
|
||||
INSTANCE=f1afd5e8d4b842c15c6a2c420b2b2dba-pj2018_k10.cnf
|
||||
DIR=/pub/data/chenzh/data/sat2020
|
||||
INSTANCE=tseitingrid7x165_shuffled.cnf
|
||||
# INSTANCE=a4bffff28417d6b4d72f7b9122988ba5-reconf10_68_queen15_2.configure
|
||||
|
||||
make -j && 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
|
||||
|
||||
|
||||
@ -19,7 +19,7 @@ int basemaple::configure(const char* name, int val) {
|
||||
// if (strcmp(name, "worker_index") == 0) solver->worker_index = val;
|
||||
// if (strcmp(name, "worker_seed") == 0) solver->worker_seed = val;
|
||||
// if (strcmp(name, "worker_number") == 0) solver->worker_number = val;
|
||||
printf("c maple configure %d\n", id);
|
||||
// printf("c maple configure %d\n", id);
|
||||
// solver->GE = 1;
|
||||
if (id == 1) solver->GE = 1;
|
||||
else solver->GE = 0;
|
||||
@ -78,7 +78,7 @@ bool cbkLstechImportClause(void * issuer, int * lbd, MapleCOMSPS::vec<MapleCOMSP
|
||||
}
|
||||
|
||||
basemaple::basemaple(int id, light* light) : basesolver(id, light) {
|
||||
printf("c id is %d\n", id);
|
||||
// printf("c id is %d\n", id);
|
||||
solver = new MapleCOMSPS::SimpSolver();
|
||||
solver->issuer = this;
|
||||
solver->cbkExportClause = NULL;
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user