Compare commits
3 Commits
c1fb74d3d9
...
90303c4665
Author | SHA1 | Date | |
---|---|---|---|
|
90303c4665 | ||
|
608ed85289 | ||
|
a24d155005 |
2
run.sh
2
run.sh
@ -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
31
run2.sh
@ -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
|
@ -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");
|
||||
|
Loading…
x
Reference in New Issue
Block a user