YuhangQ/cloud-sat
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge branch 'main' of gitea.yuhangq.com:YuhangQ/cloud-sat into main

Browse Source
This commit is contained in:
YuhangQ 2023-04-21 18:50:59 +08:00
commit b8835a74e1
12 changed files with 31 additions and 374 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
hostfile Normal file
View File

@ -0,0 +1,2 @@
192.168.100.6
192.168.100.9

18
kissat-inc/makefile
View File

@ -1,17 +1,17 @@
all: all:
$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build"
kissat: kissat:
$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" kissat $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" kissat
tissat: tissat:
$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" tissat $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" tissat
clean: clean:
rm -f "/pub/netdisk1/qianyh/Light/kissat-inc"/makefile rm -f "/home/chenzh/solvers/cloud-sat/kissat-inc"/makefile
-$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" clean -$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" clean
rm -rf "/pub/netdisk1/qianyh/Light/kissat-inc/build" rm -rf "/home/chenzh/solvers/cloud-sat/kissat-inc/build"
coverage: coverage:
$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" coverage $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" coverage
indent: indent:
$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" indent $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" indent
test: test:
$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" test $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" test
.PHONY: all clean coverage indent kissat test tissat .PHONY: all clean coverage indent kissat test tissat

52
src/clause.hpp
View File

@ -54,56 +54,4 @@ struct clause_store {
} }
}; };
struct period_clauses {
int period;
std::atomic<int> refs;
std::vector<shared_ptr<clause_store>> cls;
period_clauses(int p = 0) {
refs = 0;
period = p;
}
void increase_refs(int inc) {
refs += inc;
}
bool free_clause() {
int ref = refs.fetch_sub(1);
if (ref <= 1) {
if (ref <= 0) puts("**************************========================");
return true;
}
return false;
}
void release_clause() {
for (int i = 0; i < cls.size(); i++)
cls[i]->free_clause();
}
void push(shared_ptr<clause_store> c) {
cls.push_back(c);
}
};
struct period_queue {
std::deque<period_clauses *> q;
mutable boost::mutex mtx;
void push(period_clauses * c) {
boost::mutex::scoped_lock lock(mtx);
q.push_back(c);
}
void pop(int assert_period = -1) {
boost::mutex::scoped_lock lock(mtx);
if (assert_period != -1 && q.front()->period != assert_period) printf("c ............false free pos\n");
q.front()->release_clause();
q.pop_front();
}
period_clauses* find(int period) {
boost::mutex::scoped_lock lock(mtx);
int sp = q.front()->period;
if (period - sp >= q.size()) puts("may occur wrong");
return q[period - sp];
}
};
#endif #endif

48
src/light.cpp
View File

@ -8,8 +8,7 @@
light::light(): light::light():
finalResult (0), finalResult (0),
winner_period (1e9), winner_id (1e9),
winner_id (-1),
maxtime (5000) maxtime (5000)
{ {
// opt = new paras(); // opt = new paras();
@ -21,50 +20,6 @@ light::~light() {
workers.clear(true); workers.clear(true);
} }
void light::configure_from_file(const char* file) {
if (!strcmp(file, "")) {
configure_name = new vec<char*>[OPT(threads)];
configure_val = new vec<double>[OPT(threads)];
return;
}
assert(false);
// printf("c Get configure file: %s\n", file);
// std::ifstream fin(file);
// char buf[1000];
// fin.getline(buf, 1000);
// char *p = buf + 6;
// int ws, ss, id = 0;
// p = read_int(p, &ws);
// p = read_int(p, &ss);
// printf("%d %d\n", ws, ss);
// opt->set_para("threads", ws);
// configure_name = new vec<char*>[ws];
// configure_val = new vec<double>[ws];
// while (fin.getline(buf, 1000)) {
// p = strtok(buf, " ");
// printf("%s\n", p);
// solver_type.push(0);
// while (p) {
// p = strtok(NULL, " ");
// printf("%s\n", p);
// if (!p) break;
// int l = strlen(p), pos = 0;
// for (int i = 1; i < l; i++)
// if (p[i] == '=') pos = i;
// char *name = new char[pos];
// strncpy(name, p, pos);
// printf("%s\n", name);
// configure_name[id].push(name);
// char *val = p + pos + 1;
// double v = atof(val);
// printf("%.2lf\n", v);
// configure_val[id].push(v);
// }
// printf("out\n");
// id++;
// }
}
void light::arg_parse(int argc, char **argv) { void light::arg_parse(int argc, char **argv) {
cmdline::parser parser; cmdline::parser parser;
@ -97,6 +52,5 @@ void light::arg_parse(int argc, char **argv) {
memcpy(filename, file_string.c_str(), file_string.length()); memcpy(filename, file_string.c_str(), file_string.length());
filename[file_string.length()] = '\0'; filename[file_string.length()] = '\0';
configure_from_file(OPT(config).c_str());
} }

17
src/light.hpp
View File

@ -55,26 +55,18 @@ public:
char* filename; char* filename;
char* instance; char* instance;
vec<char*> *configure_name;
vec<double> *configure_val;
int finalResult; int finalResult;
int winner_period, winner_id; int winner_id;
mutable boost::mutex winner_mtx; mutable boost::mutex winner_mtx;
int maxtime; int maxtime;
void update_winner(int id, int period) { void update_winner(int id, int period) {
boost::mutex::scoped_lock lock(winner_mtx); boost::mutex::scoped_lock lock(winner_mtx);
if (period < winner_period || (period == winner_period && id < winner_id)) { if (id < winner_id) {
winner_period = period;
winner_id = id; winner_id = id;
} }
} }
int get_winner_period() {
boost::mutex::scoped_lock lock(winner_mtx);
return winner_period;
}
void arg_parse(int argc, char **argv); void arg_parse(int argc, char **argv);
void init_workers(); void init_workers();
void diversity_workers(); void diversity_workers();
@ -83,7 +75,6 @@ public:
int run(); int run();
int solve(); int solve();
void terminate_workers(); void terminate_workers();
void configure_from_file(const char*);
}; };
#endif #endif

31
src/sharer.cpp
View File

@ -256,37 +256,6 @@ void sharer::do_clause_sharing() {
auto clk_ed = std::chrono::high_resolution_clock::now(); auto clk_ed = std::chrono::high_resolution_clock::now();
share_time += 0.001 * std::chrono::duration_cast<std::chrono::milliseconds>(clk_ed - clk_now).count(); share_time += 0.001 * std::chrono::duration_cast<std::chrono::milliseconds>(clk_ed - clk_now).count();
} }
int sharer::import_clauses(int id) {
int current_period = producers[id]->get_period() - 1, import_period = current_period - OPT(margin);
if (import_period < 0) return 0;
basesolver *t = producers[id];
for (int i = 0; i < producers.size(); i++) {
if (i == id) continue;
basesolver *s = producers[i];
//wait for s reach period $import_period
// printf("c %d start waiting, since import_p is %d, current_p is %d\n", id, import_period, s->get_period());
boost::mutex::scoped_lock lock(s->mtx);
while (s->period <= import_period && s->terminate_period > import_period && !s->terminated) {
s->cond.wait(lock);
}
if (s->terminated) return -1;
if (s->terminate_period <= import_period) return -1;
period_clauses *pc = s->pq.find(import_period);
if (pc->period != import_period) {
printf("thread %d, now period = %d, import period = %d, import thread %d\n", id, current_period, import_period, i);
puts("*******************************************************");
}
// printf("c %d finish waiting %d %d\n", id, import_period, s->period_queue[pos]->period);
t->import_clauses_from(pc->cls);
}
t->unfree.push(import_period);
return 1;
// printf("c thread %d, period %d, import finish\n", id, current_period);
}
int sharer::sort_clauses(int x) { int sharer::sort_clauses(int x) {
for (int i = 0; i < cls.size(); i++) { for (int i = 0; i < cls.size(); i++) {

1
src/sharer.hpp
View File

@ -36,7 +36,6 @@ public:
int receive_clauses_from_other_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter); int receive_clauses_from_other_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter);
int sort_clauses(int x); int sort_clauses(int x);
int import_clauses(int id);
private: private:
light* S; light* S;

46
src/solve.cpp
View File

@ -29,32 +29,18 @@ void * solve_worker(void *arg) {
basesolver * sq = (basesolver *)arg; basesolver * sq = (basesolver *)arg;
while (!terminated) { while (!terminated) {
int res = sq->solve(); int res = sq->solve();
if (OPT(DPS)) {
//printf("c %d solved, res is %d\n", sq->id, res); if (res && !terminated) {
if (res) { //printf("c result: %d, winner is %d, winner run %d confs\n", res, sq->id, sq->get_conflicts());
terminated = 1; terminated = 1;
result = res; sq->controller->terminate_workers();
//printf("c %d solved 1\n", sq->id); result = res;
sq->internal_terminate(); sq->controller->update_winner(sq->id, 0);
//printf("c %d solved 2\n", sq->id); winner_conf = sq->get_conflicts();
sq->controller->update_winner(sq->id, sq->period); if (res == 10) sq->get_model(sq->model);
//printf("c %d solved 3\n", sq->id);
if (res == 10) sq->get_model(sq->model);
}
//printf("c %d really solved, period is %d\n", sq->id, sq->period);
}
else {
if (res && !terminated) {
//printf("c result: %d, winner is %d, winner run %d confs\n", res, sq->id, sq->get_conflicts());
terminated = 1;
sq->controller->terminate_workers();
result = res;
sq->controller->update_winner(sq->id, 0);
winner_conf = sq->get_conflicts();
if (res == 10) sq->get_model(sq->model);
}
//printf("get result %d with res %d\n", sq->id, res);
} }
//printf("get result %d with res %d\n", sq->id, res);
} }
return NULL; return NULL;
} }
@ -163,20 +149,13 @@ void light::diversity_workers() {
else else
workers[i]->configure("phase", 1); workers[i]->configure("phase", 1);
} }
for (int j = 0; j < configure_name[i].size(); j++) {
workers[i]->configure(configure_name[i][j], configure_val[i][j]);
}
} }
} }
void light::terminate_workers() { void light::terminate_workers() {
// printf("c controller reach limit\n"); // printf("c controller reach limit\n");
for (int i = 0; i < OPT(threads); i++) { for (int i = 0; i < OPT(threads); i++) {
if (OPT(share) == 1 && OPT(DPS) == 1) workers[i]->terminate();
workers[i]->external_terminate();
else
workers[i]->terminate();
} }
} }
@ -211,7 +190,6 @@ int light::solve() {
for (int j = 0; j < OPT(threads); j++) { for (int j = 0; j < OPT(threads); j++) {
s->producers.push(workers[j]); s->producers.push(workers[j]);
s->consumers.push(workers[j]); s->consumers.push(workers[j]);
workers[j]->in_sharer = s;
} }
printf("==============run1============\n"); printf("==============run1============\n");
s->clause_sharing_init(sharing_groups); s->clause_sharing_init(sharing_groups);

26
src/solver_api/basekissat.cpp
View File

@ -108,8 +108,6 @@ basekissat::basekissat(int id, light* light) : basesolver(id, light) {
if (OPT(share)) { if (OPT(share)) {
solver -> cbkImportClause = call_back_in; solver -> cbkImportClause = call_back_in;
solver -> cbkExportClause = call_back_out; solver -> cbkExportClause = call_back_out;
solver -> cbk_start_new_period = cbk_start_new_period;
solver -> cbk_free_clauses = cbk_free_clauses;
solver -> dps = OPT(DPS); solver -> dps = OPT(DPS);
solver -> dps_period = OPT(DPS_period); solver -> dps_period = OPT(DPS_period);
} }
@ -119,19 +117,6 @@ basekissat::~basekissat(){
delete solver; delete solver;
} }
void basekissat::parse_from_CNF(char* filename) {
int vars, clauses;
vec<vec<int>> clause;
readfile(filename, &vars, &clauses, clause);
maxvar = vars;
kissat_reserve(solver, vars);
for (int i = 1; i <= clauses; i++) {
int l = clause[i].size();
for (int j = 0; j < l; j++)
add(clause[i][j]);
add(0);
}
}
void basekissat::parse_from_MEM(char* instance) { void basekissat::parse_from_MEM(char* instance) {
int vars, clauses; int vars, clauses;
@ -147,17 +132,6 @@ void basekissat::parse_from_MEM(char* instance) {
} }
} }
void basekissat::parse_from_PAR(preprocess* pre) {
maxvar = pre->vars;
kissat_reserve(solver, pre->vars);
for (int i = 1; i <= pre->clauses; i++) {
int l = pre->clause[i].size();
for (int j = 0; j < l; j++)
add(pre->clause[i][j]);
add(0);
}
}
int basekissat::get_conflicts() { int basekissat::get_conflicts() {
return solver->nconflict; return solver->nconflict;
} }

3
src/solver_api/basekissat.hpp
View File

@ -13,8 +13,6 @@ public:
int configure(const char* name, int id); int configure(const char* name, int id);
int get_conflicts(); int get_conflicts();
void parse_from_CNF(char* filename);
void parse_from_PAR(preprocess *pre);
void parse_from_MEM(char* instance); void parse_from_MEM(char* instance);
void exp_clause(void *cl, int lbd); void exp_clause(void *cl, int lbd);
bool imp_clause(shared_ptr<clause_store>cls, void *cl); bool imp_clause(shared_ptr<clause_store>cls, void *cl);
@ -25,5 +23,4 @@ public:
friend int cbkImportClause(void *, int *, cvec *); friend int cbkImportClause(void *, int *, cvec *);
friend int cbkExportClause(void *, int *, cvec *); friend int cbkExportClause(void *, int *, cvec *);
friend void cbk_free_clauses(void *);
}; };

135
src/solver_api/basesolver.cpp
View File

@ -1,33 +1,6 @@
#include "basesolver.hpp" #include "basesolver.hpp"
#include "../sharer.hpp" #include "../sharer.hpp"
int basesolver::get_period() {
boost::mutex::scoped_lock lock(mtx);
return period;
};
void basesolver::inc_period() {
boost::mutex::scoped_lock lock(mtx);
period++;
if (period % 100 == 0) printf("c %d reach period %d\n", id, period);
cond.notify_all();
};
void basesolver::internal_terminate() {
boost::mutex::scoped_lock lock(mtx);
terminate_period = period;
cond.notify_all();
}
void basesolver::external_terminate() {
{
boost::mutex::scoped_lock lock(mtx);
terminated = 1;
cond.notify_all();
// printf("c thread %d terminated\n", id);
}
terminate();
}
void basesolver::broaden_export_limit() { void basesolver::broaden_export_limit() {
++good_clause_lbd; ++good_clause_lbd;
} }
@ -37,23 +10,11 @@ void basesolver::restrict_export_limit() {
--good_clause_lbd; --good_clause_lbd;
} }
double basesolver::get_waiting_time() {
return waiting_time;
}
void basesolver::export_clauses_to(std::vector<shared_ptr<clause_store>> &clauses) { void basesolver::export_clauses_to(std::vector<shared_ptr<clause_store>> &clauses) {
shared_ptr<clause_store> cls; shared_ptr<clause_store> cls;
while (export_clause.pop(cls)) { while (export_clause.pop(cls))
// printf("size: %d [", cls->size);
// for(int i=0; i<cls->size; i++) {
// printf("%d ", cls->data[i]);
// }
// printf("] \n");
clauses.push_back(cls); clauses.push_back(cls);
}
} }
void basesolver::import_clauses_from(std::vector<shared_ptr<clause_store>> &clauses) { void basesolver::import_clauses_from(std::vector<shared_ptr<clause_store>> &clauses) {
@ -62,101 +23,9 @@ void basesolver::import_clauses_from(std::vector<shared_ptr<clause_store>> &clau
} }
} }
void basesolver::select_clauses() {
sharer *share = in_sharer;
cls.clear();
export_clauses_to(cls);
for (int i = 0; i < cls.size(); i++) {
int sz = cls[i]->size;
while (sz > bucket.size()) bucket.push();
if (sz * (bucket[sz - 1].size() + 1) <= OPT(share_lits))
bucket[sz - 1].push_back(cls[i]);
}
period_clauses *pcls = new period_clauses(period);
int space = OPT(share_lits);
for (int i = 0; i < bucket.size(); i++) {
int clause_num = space / (i + 1);
if (!clause_num) break;
if (clause_num >= bucket[i].size()) {
space -= bucket[i].size() * (i + 1);
for (int j = 0; j < bucket[i].size(); j++)
pcls->push(bucket[i][j]);
bucket[i].clear();
}
else {
space -= clause_num * (i + 1);
for (int j = 0; j < clause_num; j++) {
pcls->push(bucket[i].back());
bucket[i].pop_back();
}
}
}
int percent = (OPT(share_lits) - space) * 100 / OPT(share_lits);
if (percent < 75) broaden_export_limit();
if (percent > 98) restrict_export_limit();
//sort finish
pcls->increase_refs(share->producers.size() - 1);
pq.push(pcls);
}
void basesolver::get_model(vec<int> &model) { void basesolver::get_model(vec<int> &model) {
model.clear(); model.clear();
for (int i = 1; i <= maxvar; i++) { for (int i = 1; i <= maxvar; i++) {
model.push(val(i)); model.push(val(i));
} }
} }
void cbk_start_new_period(void *solver) {
auto clk_st = std::chrono::high_resolution_clock::now();
basesolver* S = (basesolver *) solver;
sharer *share = S->in_sharer;
int should_free = 1;
if (S->period >= S->controller->get_winner_period()) {
S->internal_terminate();
S->terminate();
return;
}
printf("c thread %d into select %d\n", S->id, S->period);
S->select_clauses();
// printf("c %d now finish period %d\n", S->id, S->get_period());
S->inc_period();
// printf("c thread %d start import at %d\n", S->id, S->period);
should_free = share->import_clauses(S->id);
printf("c thread %d finish import at %d\n", S->id, S->period);
if (should_free == -1) {
S->internal_terminate();
S->terminate();
}
auto clk_now = std::chrono::high_resolution_clock::now();
int solve_time = std::chrono::duration_cast<std::chrono::milliseconds>(clk_now - clk_st).count();
S->waiting_time += 0.001 * solve_time;
// printf("c %d wait for %d.%03ds\n", S->id, solve_time / 1000, solve_time % 1000);
// printf("c %d finish sharing\n", S->id);
}
void cbk_free_clauses(void *solver) {
basesolver* S = (basesolver *) solver;
sharer *share = S->in_sharer;
if (S->unfree.size()) printf("free %d period\n", S->unfree.size());
for (int id = 0; id < S->unfree.size(); id++) {
int import_period = S->unfree[id];
// int current_period = S->get_period() - 1, import_period = current_period - share->margin;
// if (import_period < 0) return;
for (int i = 0; i < share->producers.size(); i++) {
if (i == S->id) continue;
basesolver *s = share->producers[i];
period_clauses *pc = s->pq.find(import_period);
if (pc->period != import_period)
puts("*******************************************************");
if (pc->free_clause()) {
s->pq.pop(import_period);
// printf("thread %d enter, %d is free\n", S->id, i);
}
}
}
S->unfree.clear();
}

26
src/solver_api/basesolver.hpp
View File

@ -20,8 +20,6 @@ public:
virtual int configure(const char* name, int id) = 0; virtual int configure(const char* name, int id) = 0;
virtual int get_conflicts() = 0; virtual int get_conflicts() = 0;
virtual void parse_from_CNF(char* filename) = 0;
virtual void parse_from_PAR(preprocess* pre) = 0;
virtual void parse_from_MEM(char* instance) = 0; virtual void parse_from_MEM(char* instance) = 0;
virtual void exp_clause(void *cl, int lbd) = 0; virtual void exp_clause(void *cl, int lbd) = 0;
virtual bool imp_clause(shared_ptr<clause_store>cls, void *cl) = 0; virtual bool imp_clause(shared_ptr<clause_store>cls, void *cl) = 0;
@ -30,38 +28,21 @@ public:
void import_clauses_from(std::vector<shared_ptr<clause_store>> &clauses); void import_clauses_from(std::vector<shared_ptr<clause_store>> &clauses);
void get_model(vec<int> &model); void get_model(vec<int> &model);
void select_clauses();
void broaden_export_limit(); void broaden_export_limit();
void restrict_export_limit(); void restrict_export_limit();
double get_waiting_time();
int get_period();
void inc_period();
void internal_terminate();
void external_terminate();
double waiting_time = 0;
int good_clause_lbd = 0; int good_clause_lbd = 0;
light * controller; light * controller;
int id; int id;
sharer* in_sharer;
vec<int> model; vec<int> model;
int terminate_period = 1e9; int maxvar, terminated = 0;
int maxvar, period, margin, terminated = 0;
mutable boost::mutex mtx;
boost::condition_variable cond;
period_queue pq;
std::vector<shared_ptr<clause_store>> cls;
vec<std::vector<shared_ptr<clause_store>>> bucket;
vec<int> unfree;
boost::lockfree::spsc_queue<shared_ptr<clause_store>, boost::lockfree::capacity<10240000>> import_clause; boost::lockfree::spsc_queue<shared_ptr<clause_store>, boost::lockfree::capacity<10240000>> import_clause;
boost::lockfree::spsc_queue<shared_ptr<clause_store>, boost::lockfree::capacity<10240000>> export_clause; boost::lockfree::spsc_queue<shared_ptr<clause_store>, boost::lockfree::capacity<10240000>> export_clause;
basesolver(int sid, light* light) : id(sid), controller(light) { basesolver(int sid, light* light) : id(sid), controller(light) {
good_clause_lbd = 2; good_clause_lbd = 2;
period = 0;
margin = 0;
} }
~basesolver() { ~basesolver() {
@ -69,11 +50,6 @@ public:
controller = NULL; controller = NULL;
} }
} }
friend void cbk_start_new_period(void *);
friend void cbk_free_clauses(void *);
}; };
void cbk_start_new_period(void *);
void cbk_free_clauses(void *);
#endif #endif