Skip to content

Commit

Permalink
Fixing the race condition problem described in Issue #9
Browse files Browse the repository at this point in the history
  • Loading branch information
@marekpiotrow
marekpiotrow committed Apr 28, 2024
1 parent 0a75f48 commit b1d226d
Show file tree
Hide file tree
Showing 4 changed files with 42 additions and 24 deletions.
19 changes: 12 additions & 7 deletions Main.cc
100644 → 100755
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,8 @@ Read a DIMACS file and apply the SAT-solver to it.
#include <unistd.h>
#include <signal.h>
#include <atomic>
#include <chrono>
#include <thread>
#include "System.h"
#include "MsSolver.h"
#include "PbParser.h"
Expand All @@ -48,10 +50,10 @@ Read a DIMACS file and apply the SAT-solver to it.
int main(int argc, char** argv)
{
#ifdef USE_SCIP
extern std::atomic<bool> SCIP_found_opt;
extern std::atomic<char> opt_finder;
time(&wall_clock_time);
#else
bool SCIP_found_opt = false;
char opt_finder = OPT_NONE;
#endif
try {
setOptions(argc, argv);
Expand Down Expand Up @@ -141,18 +143,21 @@ int main(int argc, char** argv)
// <<== write result to file 'opt_result'

if (opt_command == cmd_Minimize) {
if (!SCIP_found_opt) outputResult(*pb_solver, !pb_solver->asynch_interrupt);
if (opt_finder != OPT_SCIP) outputResult(*pb_solver, !pb_solver->asynch_interrupt);
} else if (opt_command == cmd_FirstSolution) {
if (!SCIP_found_opt) outputResult(*pb_solver, false);
if (opt_finder != OPT_SCIP) outputResult(*pb_solver, false);
}

} catch (Minisat::OutOfMemoryException&){
if (opt_verbosity >= 1 && !SCIP_found_opt) {
if (opt_verbosity >= 1 && opt_finder != OPT_SCIP) {
pb_solver->printStats();
reportf("Out of memory exception caught\n");
}
if (!SCIP_found_opt) outputResult(*pb_solver, false);
if (opt_finder != OPT_SCIP) outputResult(*pb_solver, false);
}

#ifdef USE_SCIP
if (opt_scip_parallel)
std::this_thread::sleep_for(std::chrono::milliseconds(10));
#endif
std::_Exit(0); // (faster than "return", which will invoke the destructor for 'PbSolver')
}
19 changes: 11 additions & 8 deletions MsSolver.cc
100644 → 100755
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@

#ifdef USE_SCIP
#include <atomic>
extern std::atomic<bool> SCIP_found_opt, MS_found_opt;
extern std::atomic<char> opt_finder;
#endif

template<typename int_type>
Expand Down Expand Up @@ -638,7 +638,7 @@ void MsSolver::maxsat_solve(solve_Command cmd)
first_time=true; limitTime(start_solving_cpu + (opt_cpu_lim - start_solving_cpu)/4);
}
#ifdef USE_SCIP
if (ipamir_used) SCIP_found_opt.store(false);
if (ipamir_used) opt_finder.store(OPT_NONE);
extern bool opt_use_scip_slvr;
int sat_orig_vars = sat_solver.nVars(), sat_orig_cls = sat_solver.nClauses();
if (opt_use_scip_slvr && UB_goalval < Int(uint64_t(2) << std::numeric_limits<double>::digits) && l_True ==
Expand Down Expand Up @@ -722,7 +722,7 @@ void MsSolver::maxsat_solve(solve_Command cmd)
{
#ifdef USE_SCIP
std::lock_guard<std::mutex> lck(optsol_mtx);
if (!SCIP_found_opt) {
if (opt_finder != OPT_SCIP) {
#endif
best_goalvalue = goalvalue, model.moveTo(best_model);
if (gbmo_remain_goal_ps.size() > 0)
Expand Down Expand Up @@ -1170,6 +1170,12 @@ void MsSolver::maxsat_solve(solve_Command cmd)
if (UB_goalvalue != Int_MAX) UB_goalvalue *= goal_gcd;
}
if (ipamir_used) reset_soft_cls(soft_cls, fixed_soft_cls, modified_soft_cls, goal_gcd);
char test = OPT_NONE;
bool MSAT_found_opt = sat && !asynch_interrupt && cmd != sc_FirstSolution && best_goalvalue < INT_MAX
#ifdef USE_SCIP
&& opt_finder.compare_exchange_strong(test, OPT_MSAT)
#endif
;
if (opt_verbosity >= 1 && opt_output_top < 0){
if (!sat)
reportf(asynch_interrupt ? "\bUNKNOWN\b\n" : "\bUNSATISFIABLE\b\n");
Expand All @@ -1187,11 +1193,8 @@ void MsSolver::maxsat_solve(solve_Command cmd)
} else {
#ifdef USE_SCIP
std::lock_guard<std::mutex> lck(optsol_mtx);
if (!SCIP_found_opt) {
MS_found_opt.store(true);
#else
{
#endif
if (MSAT_found_opt) {
char* tmp = toString(best_goalvalue);
reportf("\bOptimal solution: %s\b\n", tmp);
xfree(tmp);
Expand All @@ -1200,7 +1203,7 @@ void MsSolver::maxsat_solve(solve_Command cmd)
}
if (opt_verbosity >= 1
#ifdef USE_SCIP
&& !SCIP_found_opt
&& opt_finder != OPT_SCIP
#endif
) pb_solver->printStats();
}
Expand Down
2 changes: 2 additions & 0 deletions MsSolver.h
100644 → 100755
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@
#include "VecMaps.h"
#include "Sort.h"

enum OptFinder {OPT_NONE, OPT_SCIP, OPT_MSAT};

Int evalGoal(const vec<Pair<weight_t, Minisat::vec<Lit>* > >& soft_cls, vec<bool>& model, Minisat::vec<Lit>& soft_unsat);

static inline int hleft (int i) { return i * 2; }
Expand Down
26 changes: 17 additions & 9 deletions ScipSolver.cc
100644 → 100755
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,14 @@
#include <vector>
#include <future>
#include <atomic>
#include <chrono>
#include <thread>
#include <scip/struct_message.h>

#define MY_SCIP_CALL(x) do{ SCIP_RETCODE _r_; \
if ((_r_ = (x)) != SCIP_OKAY) { reportf("SCIP error <%d>\n",_r_); return l_Undef; }} while(0)

std::atomic<bool> SCIP_found_opt(false), MS_found_opt(false);
std::atomic<char> opt_finder(OPT_NONE);

lbool set_scip_var(SCIP *scip, MsSolver *solver, std::vector<SCIP_VAR *> &vars, Lit lit)
{
Expand Down Expand Up @@ -90,6 +92,7 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
{
lbool found_opt = l_Undef;
SCIP_STATUS status;
int64_t best_value = INT64_MAX;

MY_SCIP_CALL(SCIPsolve(scip));
status = SCIPgetStatus(scip);
Expand All @@ -100,18 +103,14 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
SCIP_SOL *sol = SCIPgetBestSol(scip);
assert(sol != nullptr);
// MY_SCIP_CALL(SCIPprintSol(scip, sol, nullptr, FALSE));
solver->best_goalvalue = obj_offset + long(round(SCIPgetSolOrigObj(scip, sol)));
if (!solver->ipamir_used || opt_verbosity > 0)
reportf("SCIP optimum (rounded): %ld\n", tolong(solver->best_goalvalue));
best_value = obj_offset + long(round(SCIPgetSolOrigObj(scip, sol)));
for (Var x = 0; x < (int)vars.size(); x++)
{
if (vars[x] != nullptr) {
SCIP_Real v = SCIPgetSolVal(scip, sol, vars[x]);
scip_model[x] = lbool(v > 0.5);
}
}
extern bool opt_satisfiable_out;
opt_satisfiable_out = false;
} else if (status == SCIP_STATUS_INFEASIBLE) {
found_opt = l_False;
if (opt_verbosity > 0) reportf("SCIP result: UNSATISFIABLE\n");
Expand All @@ -130,9 +129,11 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
// if optimum found, exit
if (found_opt == l_True) {
std::lock_guard<std::mutex> lck(optsol_mtx);
if (!MS_found_opt) {
SCIP_found_opt.store(true);

char test = OPT_NONE;
if (opt_finder.compare_exchange_strong(test, OPT_SCIP)) {
if (!solver->ipamir_used || opt_verbosity > 0)
reportf("SCIP optimum (rounded): %" PRId64 "\n", best_value);
solver->best_goalvalue = best_value;
vec<lbool> opt_model(scip_model.size());
for (int i = scip_model.size() - 1; i >= 0 ; i--) opt_model[i] = scip_model[i];
solver->sat_solver.extendGivenModel(opt_model);
Expand All @@ -141,7 +142,12 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
Minisat::vec<Lit> soft_unsat; // Not used in this context
solver->best_goalvalue = (solver->fixed_goalval + evalGoal(solver->soft_cls, solver->best_model, soft_unsat)) * solver->goal_gcd;

extern bool opt_satisfiable_out;
opt_satisfiable_out = false;

if (opt_verbosity >= 1) {

{ std::lock_guard<std::mutex> lck(stdout_mtx);
SCIP_MESSAGEHDLR *mh = SCIPgetMessagehdlr(scip);
auto mi = mh->messageinfo;
mh->messageinfo = uwrMessageInfo;
Expand All @@ -152,10 +158,12 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
SCIPprintTimingStatistics(scip, nullptr);
mh->messageinfo = mi;
MY_SCIP_CALL(SCIPsetMessagehdlr(scip, mh));
}
solver->printStats(false);
}
if (!solver->ipamir_used) {
outputResult(*solver, true);
std::this_thread::sleep_for(std::chrono::milliseconds(10));
//MY_SCIP_CALL(SCIPfree(&scip));
std::_Exit(0);
}
Expand Down

0 comments on commit b1d226d

Please sign in to comment.