Compare commits

...

3 Commits

Author SHA1 Message Date
ihan-o
90303c4665 fixed sharing bug 2023-05-14 00:18:13 +08:00
ihan-o
608ed85289 Merge branch 'main' of gitea.yuhangq.com:YuhangQ/cloud-sat into main 2023-05-14 00:12:03 +08:00
ihan-o
a24d155005 fixed maple sharing bug 2023-05-14 00:09:50 +08:00
5 changed files with 395 additions and 65038 deletions

65201
res.txt

File diff suppressed because one or more lines are too long

197
res2.txt

File diff suppressed because one or more lines are too long

2
run.sh
View File

@ -23,7 +23,7 @@
# 这个存在问题
DIR=/pub/data/chenzh/data/sat2022
# INSTANCE=tseitingrid7x165_shuffled.cnf
INSTANCE=a44fce1796383ea31df08af3b0f65db3-soelberg_unit_159.cnf
INSTANCE=5601a7e094f61f3c5af461300c25243f-summle_X111107_steps8_I1-2-2-4-4-8-25-100.cnf
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

31
run2.sh
View File

@ -1,31 +0,0 @@
#!/bin/bash
# cd kissat-inc
# make clean
# ./configure
# make -j 64
# cd ..
# make clean
# buglist
# - fe96b630b3e761821308b544368dd521-GP_100_950_34.cnf
# - 0d4970edf84353e5a5798bca3f7f270e-SAT_H_instances_childsnack_p10.hddl_2.cnf
# 退出慢
# - 00aefd1fc30c425075166ca051e57218-barman-pfile10-038.sas.ex.15.cnf
# - 23e61c50ee2ac5cad1d337572abdebcf-aws-encryption-sdk-c:aws_cryptosdk_priv_hdr_parse_edks.cnf
# 解不出来
# - 72329bc80f5f55dcc356a22f3f11ebec-GP_200_313_5.cnf
# - 367c25ad50259a685a25b86d6dd171b2-GP_100_950_33.cnf
# 这个存在问题
DIR=/pub/data/chenzh/data/sat2022
# INSTANCE=tseitingrid7x165_shuffled.cnf
INSTANCE=a44fce1796383ea31df08af3b0f65db3-soelberg_unit_159.cnf
make -j && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --shuffle=1 --share=0 --threads=16 --times=3600 --share_method=0
# make -j 16 && mpirun --mca btl_tcp_if_include 192.168.100.0/24 --hostfile ./experiment/hostfile --bind-to none -np 65 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 --share_method=0
#./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600

View File

@ -9,7 +9,7 @@
// Macros for minisat literal representation conversion
#define MINI_LIT(lit) lit > 0 ? MapleCOMSPS::mkLit(lit - 1, false) : MapleCOMSPS::mkLit((-lit) - 1, true)
#define INT_LIT(lit) sign(lit) ? -(var(lit) + 1) : (var(lit) + 1)
#define INT_LIT(lit) MapleCOMSPS::sign(lit) ? -(var(lit) + 1) : (var(lit) + 1)
void basemaple::add(int l) {
puts("wrong");