From 416f282825393c982fcea73af6c4cba0ca642a43 Mon Sep 17 00:00:00 2001 From: YuhangQ Date: Thu, 20 Apr 2023 22:28:48 +0800 Subject: [PATCH] =?UTF-8?q?=E5=A2=9E=E5=8A=A0SAT=E6=A8=A1=E5=BC=8F?= =?UTF-8?q?=EF=BC=8C=E6=94=B9=E8=BF=9BRS?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- kissat-inc/makefile | 18 ++++---- kissat-inc/src/bump.c | 18 +++++++- kissat-inc/src/options.c | 2 + kissat-inc/src/options.h | 4 +- run.sh | 9 ++++ src/light.hpp | 2 +- src/sharer.cpp | 12 ++--- src/solve.cpp | 85 +++++++++++++++++++++-------------- src/solver_api/basekissat.cpp | 4 +- src/solver_api/basekissat.hpp | 2 +- src/solver_api/basesolver.hpp | 2 +- 11 files changed, 103 insertions(+), 55 deletions(-) diff --git a/kissat-inc/makefile b/kissat-inc/makefile index db6dce3..37626dd 100644 --- a/kissat-inc/makefile +++ b/kissat-inc/makefile @@ -1,17 +1,17 @@ all: - $(MAKE) -C "/root/cloud-sat/kissat-inc/build" + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" kissat: - $(MAKE) -C "/root/cloud-sat/kissat-inc/build" kissat + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" kissat tissat: - $(MAKE) -C "/root/cloud-sat/kissat-inc/build" tissat + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" tissat clean: - rm -f "/root/cloud-sat/kissat-inc"/makefile - -$(MAKE) -C "/root/cloud-sat/kissat-inc/build" clean - rm -rf "/root/cloud-sat/kissat-inc/build" + rm -f "/pub/netdisk1/qianyh/Light/kissat-inc"/makefile + -$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" clean + rm -rf "/pub/netdisk1/qianyh/Light/kissat-inc/build" coverage: - $(MAKE) -C "/root/cloud-sat/kissat-inc/build" coverage + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" coverage indent: - $(MAKE) -C "/root/cloud-sat/kissat-inc/build" indent + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" indent test: - $(MAKE) -C "/root/cloud-sat/kissat-inc/build" test + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" test .PHONY: all clean coverage indent kissat test tissat diff --git a/kissat-inc/src/bump.c b/kissat-inc/src/bump.c index 1941c5b..d0df120 100644 --- a/kissat-inc/src/bump.c +++ b/kissat-inc/src/bump.c @@ -54,7 +54,12 @@ rescale_scores (kissat * solver, heap * scores) } void kissat_init_shuffle(kissat * solver, int maxvar) { - int seed = GET_OPTION(order_reset); + int seed = GET_OPTION(worker_seed); + int index = GET_OPTION(worker_index); + int number = GET_OPTION(worker_number); + + printf("c index:%d number:%d seed:%d\n", index, number, seed); + if (seed != -1) { // printf("c init shuffle %d\n", seed); @@ -69,8 +74,17 @@ void kissat_init_shuffle(kissat * solver, int maxvar) { id[i] = id[j]; id[j] = x; } - for (int i = 1; i <= maxvar; i++) + + int block_size = maxvar / number; + int cursor = index * block_size; + for(int i=cursor; i<=maxvar; i++) { kissat_activate_literal(solver, kissat_import_literal(solver, id[i])); + } + + for (int i = 1; i < cursor ; i++) { + kissat_activate_literal(solver, kissat_import_literal(solver, id[i])); + } + free(id); } else diff --git a/kissat-inc/src/options.c b/kissat-inc/src/options.c index 5a9c0cf..d8b5b99 100644 --- a/kissat-inc/src/options.c +++ b/kissat-inc/src/options.c @@ -287,8 +287,10 @@ int kissat_options_set (options * options, const char *name, int value) { const opt *o = kissat_options_has (name); + if (!o) return 0; + return kissat_options_set_opt (options, o, value); } diff --git a/kissat-inc/src/options.h b/kissat-inc/src/options.h index e210198..5ac98c1 100644 --- a/kissat-inc/src/options.h +++ b/kissat-inc/src/options.h @@ -55,7 +55,6 @@ OPTION( mabcint, 4, 0, 10, "mab const floor") \ OPTION( minimizedepth, 1e3, 1, 1e6, "minimization depth") \ OPTION( modeinit, 1e3, 10, 1e8, "initial mode change interval") \ OPTION( modeint, 1e3, 10, 1e8, "base mode change interval") \ -OPTION( order_reset, -1, -1, 1e5, "order seed") \ OPTION( otfs, 1, 0, 1, "on-the-fly strengthening") \ OPTION( phase, 1, 0, 1, "initial decision phase") \ OPTION( phasesaving, 1, 0, 1, "enable phase saving") \ @@ -120,6 +119,9 @@ OPTION( walkmaxeff, 100, 1, INT_MAX, "maximum relative efficiency") \ OPTION( walkmineff, 1e7, 0, INT_MAX, "minimum vivify efficiency") \ OPTION( walkreleff, 10, 0, 1e3, "relative efficiency in per mille") \ OPTION( walkrounds, 1, 1, 1e5, "rounds per walking phase") \ +OPTION( worker_index, -1, -1, 1e5, "worker index") \ +OPTION( worker_number, -1, -1, 1e5, "number of workers") \ +OPTION( worker_seed, -1, -1, 1e5, "worker random shuffle seed") \ OPTION( xors, 1, 0, 1, "extract and eliminate XOR gates") \ OPTION( xorsbound, 1 ,0 , 1<<13, "minimum elimination bound") \ OPTION( xorsclslim, 5, 3, 31, "XOR extraction clause size limit") \ diff --git a/run.sh b/run.sh index 846df2f..d16adc0 100755 --- a/run.sh +++ b/run.sh @@ -27,6 +27,15 @@ INSTANCE=04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf # make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 + +# cd kissat-inc +# make clean +# ./configure +# make -j 64 +# cd .. + +# make clean + 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 #./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 diff --git a/src/light.hpp b/src/light.hpp index 2f5f715..9c6947a 100644 --- a/src/light.hpp +++ b/src/light.hpp @@ -46,7 +46,7 @@ public: sharer* s; std::vector> sharing_groups; - enum { UNSAT, DEFAULT } worker_type; + enum { SAT, UNSAT, DEFAULT } worker_type; MPI_Request terminal_request; diff --git a/src/sharer.cpp b/src/sharer.cpp index b608e4d..b57d619 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -235,11 +235,13 @@ void sharer::do_clause_sharing() { // 增加 lits 限制 int percent = sort_clauses(i); - if (percent < 75) { - producers[i]->broaden_export_limit(); - } - else if (percent > 98) { - producers[i]->restrict_export_limit(); + if(S->worker_type == light::UNSAT) { + if (percent < 75) { + producers[i]->broaden_export_limit(); + } + else if (percent > 98) { + producers[i]->restrict_export_limit(); + } } for (int j = 0; j < consumers.size(); j++) { diff --git a/src/solve.cpp b/src/solve.cpp index 511bdf9..eb018d3 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -69,39 +69,39 @@ void light::init_workers() { void light::diversity_workers() { for (int i = 0; i < OPT(threads); i++) { - // if(worker_type == SAT) { + if(worker_type == SAT) { - // if (OPT(shuffle)) { - // if (i) workers[i]->configure("order_reset", (rank - 1) * OPT(threads) + i); - // } + if (OPT(shuffle)) { + workers[i]->configure("worker_index", i); + workers[i]->configure("worker_number", OPT(threads)); + workers[i]->configure("worker_seed", rank); + // printf("r1: %d, r2: %d, r3: %d\n", r1, r2, r3); + } - // workers[i]->configure("stable", 1); - // workers[i]->configure("target", 2); - // workers[i]->configure("phase", 1); - // // workers[i]->configure("heuristic", 0); + workers[i]->configure("stable", 1); + workers[i]->configure("target", 2); + workers[i]->configure("phase", 1); + // workers[i]->configure("heuristic", 0); - // if (i == 2) - // workers[i]->configure("stable", 0); - // else if (i == 6) - // workers[i]->configure("stable", 2); + if (i == 2) + workers[i]->configure("stable", 0); + else if (i == 6) + workers[i]->configure("stable", 2); - // if (i == 7) - // workers[i]->configure("target", 0); - // else if (i == 0 || i == 2 || i == 3 || i == 6) - // workers[i]->configure("target", 1); + if (i == 7) + workers[i]->configure("target", 0); + else if (i == 0 || i == 2 || i == 3 || i == 6) + workers[i]->configure("target", 1); - // if (i == 3 || i == 11 || i == 12 || i == 13 || i == 15) - // workers[i]->configure("phase", 0); - // } else - - if(worker_type == UNSAT) { - + if (i == 3 || i == 11 || i == 12 || i == 13 || i == 15) + workers[i]->configure("phase", 0); + } else if(worker_type == UNSAT) { OPT(share_lits) = 3000; - workers[i]->configure("chrono", 1); workers[i]->configure("stable", 0); // workers[i]->configure("walkinitially", 0); workers[i]->configure("target", 1); + // workers[i]->configure("phase", 1); // workers[i]->configure("heuristic", 0); // workers[i]->configure("margin", 1)0; @@ -119,10 +119,16 @@ void light::diversity_workers() { workers[i]->configure("target", 0); else if (i == 14) workers[i]->configure("target", 2); + } else { + if (OPT(shuffle)) { - if (i) workers[i]->configure("order_reset", (rank - 1) * OPT(threads) + i); + workers[i]->configure("worker_index", i); + workers[i]->configure("worker_number", OPT(threads)); + workers[i]->configure("worker_seed", rank); + // printf("r1: %d, r2: %d, r3: %d\n", r1, r2, r3); } + if (i == 13 || i == 14 || i == 9) workers[i]->configure("tier1", 3); else @@ -273,26 +279,38 @@ void light::seperate_groups() { int worker_procs = num_procs - 1; if(worker_procs >= 8) { - int unsat_procs = worker_procs / 4; - int default_procs = worker_procs - unsat_procs; - // [1, unsat_procs] for unsat - if(rank >= 1 && rank <= unsat_procs) { - worker_type = light::UNSAT; + int sat_procs = worker_procs / 8; + int unsat_procs = sat_procs; + int default_procs = worker_procs - sat_procs - unsat_procs; + // [1, sat_procs] for sat + if(rank >= 1 && rank <= sat_procs) { + worker_type = light::SAT; } std::vector tmp; - for(int i=1; i<=unsat_procs; i++) { + for(int i=1; i<=sat_procs; i++) { tmp.push_back(i); } sharing_groups.push_back(tmp); - // [unsat_procs+1, worker_procs] - if(rank >= unsat_procs+1 && rank <= worker_procs) { + // [sat_procs+1, sat_procs+unsat_procs] for unsat + if(rank >= sat_procs+1 && rank <= sat_procs+unsat_procs) { + worker_type = light::UNSAT; + } + + tmp.clear(); + for(int i=sat_procs+1; i<=sat_procs+unsat_procs; i++) { + tmp.push_back(i); + } + sharing_groups.push_back(tmp); + + // [sat_procs+unsat_procs+1, worker_procs] + if(rank >= sat_procs+unsat_procs+1 && rank <= worker_procs) { worker_type = light::DEFAULT; } tmp.clear(); - for(int i=unsat_procs+1; i<=worker_procs; i++) { + for(int i=sat_procs+unsat_procs+1; i<=worker_procs; i++) { tmp.push_back(i); } sharing_groups.push_back(tmp); @@ -308,6 +326,7 @@ void light::seperate_groups() { } } + void print_model(vec &model) { printf("v"); for (int i = 0; i < model.size(); i++) { diff --git a/src/solver_api/basekissat.cpp b/src/solver_api/basekissat.cpp index 20deedf..85b9ce4 100644 --- a/src/solver_api/basekissat.cpp +++ b/src/solver_api/basekissat.cpp @@ -15,9 +15,9 @@ void basekissat::add(int l) { kissat_add(solver, l); } -void basekissat::configure(const char* name, int val) { +int basekissat::configure(const char* name, int val) { // printf("c %d set %s to %d\n", id, name, val); - kissat_set_option(solver, name, val); + return kissat_set_option(solver, name, val); } int basekissat::solve() { diff --git a/src/solver_api/basekissat.hpp b/src/solver_api/basekissat.hpp index fe0f741..14a9280 100644 --- a/src/solver_api/basekissat.hpp +++ b/src/solver_api/basekissat.hpp @@ -10,7 +10,7 @@ public: void add(int l); int solve(); int val(int l); - void configure(const char* name, int id); + int configure(const char* name, int id); int get_conflicts(); void parse_from_CNF(char* filename); diff --git a/src/solver_api/basesolver.hpp b/src/solver_api/basesolver.hpp index 573bc18..5b4cdf0 100644 --- a/src/solver_api/basesolver.hpp +++ b/src/solver_api/basesolver.hpp @@ -17,7 +17,7 @@ public: virtual int solve() = 0; virtual int val(int l) = 0; virtual void terminate() = 0; - virtual void configure(const char* name, int id) = 0; + virtual int configure(const char* name, int id) = 0; virtual int get_conflicts() = 0; virtual void parse_from_CNF(char* filename) = 0;