Skip to content

Commit

Permalink
Improving cooperation with SCIP
Browse files Browse the repository at this point in the history
  • Loading branch information
@marekpiotrow
marekpiotrow committed May 3, 2024
1 parent 5a4c82c commit cb5ebd1
Show file tree
Hide file tree
Showing 3 changed files with 26 additions and 14 deletions.
2 changes: 1 addition & 1 deletion Main_utils.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ maxPreprocessor::PreprocessorInterface *maxpre_ptr = NULL;
bool opt_use_scip_slvr = true;
double opt_scip_cpu = 0;
double opt_scip_cpu_default = 600;
double opt_scip_cpu_add = 400;
double opt_scip_cpu_add = 600;
bool opt_scip_parallel = true;
time_t wall_clock_time;
bool opt_force_scip = false;
Expand Down
8 changes: 5 additions & 3 deletions MsSolver.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1192,10 +1192,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)
char test = OPT_NONE;
bool MSAT_found_opt = satisfied && !asynch_interrupt && cmd != sc_FirstSolution && best_goalvalue < INT_MAX
&& opt_finder.compare_exchange_strong(test, OPT_MSAT);
#else
bool MSAT_found_opt = satisfied && !asynch_interrupt && cmd != sc_FirstSolution && best_goalvalue < INT_MAX;
#endif
;
if (opt_verbosity >= 1 && opt_output_top < 0){
Expand Down
30 changes: 20 additions & 10 deletions ScipSolver.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,15 +93,17 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
extern double opt_scip_cpu, opt_scip_cpu_add;
lbool found_opt = l_Undef;
SCIP_STATUS status;
int64_t best_value = INT64_MAX;
int try_count = 3;
bool try_again, obj_limit_applied = false;
int64_t bound_gap = INT64_MAX;

if (solver->best_goalvalue < WEIGHT_MAX) {
MY_SCIP_CALL(SCIPsetObjlimit(scip,
tolong(solver->best_goalvalue * solver->goal_gcd - obj_offset)));
SCIP_Real(tolong(solver->best_goalvalue * solver->goal_gcd - obj_offset))));
obj_limit_applied = true;
}
MY_SCIP_CALL(SCIPsetObjIntegral(scip));
do {
try_again = false;
MY_SCIP_CALL(SCIPsolve(scip));
Expand All @@ -121,18 +123,25 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
}
}
} else if (status == SCIP_STATUS_INFEASIBLE) {
if (obj_limit_applied) return l_True; // SCIP proved optimality of the best_goalvalue
found_opt = l_False;
if (opt_verbosity > 0) reportf("SCIP result: UNSATISFIABLE\n");
if (!solver->ipamir_used) {
printf("s UNSATISFIABLE\n");
std::_Exit(20);
if (obj_limit_applied) { // SCIP proved optimality of the last MaxSAT o-value
if (!solver->ipamir_used || opt_verbosity > 0)
reportf("SCIP proved optimality of the last o-value\n");
solver->printStats(true);
return l_True;
} else {
found_opt = l_False;
if (opt_verbosity > 0) reportf("SCIP result: UNSATISFIABLE\n");
if (!solver->ipamir_used) {
printf("s UNSATISFIABLE\n");
std::_Exit(20);
}
}
} else {
SCIP_Real dualb = SCIPgetDualbound(scip), primb = SCIPgetPrimalbound(scip);
int64_t lbound = (!SCIPisInfinity(scip, dualb) ? int64_t(round(dualb)) + obj_offset : INT64_MIN);
int64_t ubound = (!SCIPisInfinity(scip, primb) ? int64_t(round(primb)) + obj_offset : INT64_MAX);
if (!solver->ipamir_used || opt_verbosity > 0) reportf("SCIP timeout with lower and upper bounds: [%lld, %lld]\n", lbound, ubound);
if (!solver->ipamir_used || opt_verbosity > 0)
reportf("SCIP timeout with lower and upper bounds: [%lld, %lld]\n", lbound, ubound);
if (!SCIPisInfinity(scip, dualb)) {
int64_t lb = (solver->goal_gcd == 1 ? lbound : (lbound > 0 ? lbound + solver->goal_gcd - 1 : lbound) / solver->goal_gcd);
if (Int(lb) > solver->scip_LB) solver->scip_LB = lb, solver->scip_foundLB = true;
Expand All @@ -150,7 +159,7 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
scip_model[x] = lbool(v > 0.5);
}
std::lock_guard<std::mutex> lck(optsol_mtx);
if (!MS_found_opt) {
if (opt_finder.load() != OPT_MSAT) {
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 Down Expand Up @@ -260,7 +269,7 @@ lbool MsSolver::scip_solve(const Minisat::vec<Lit> *assump_ps,
extern bool opt_force_scip;

if (!res || !opt_force_scip &&
(sat_solver.nFreeVars() >= 100000 || sat_orig_cls >= 150000 || soft_cls.size() >= 100000))
(sat_solver.nFreeVars() >= 100000 || sat_orig_cls >= 600000 || soft_cls.size() >= 100000))
return l_Undef;

extern double opt_scip_cpu, opt_scip_delay;
Expand All @@ -275,6 +284,7 @@ lbool MsSolver::scip_solve(const Minisat::vec<Lit> *assump_ps,
char *base = nullptr;
if (opt_input != nullptr) base = strrchr(opt_input,'/'), base = (base ? base+1 : opt_input);
MY_SCIP_CALL(SCIPcreateProbBasic(scip, (base != nullptr ? base : "IPAMIR of UWrMaxSat")));
MY_SCIP_CALL(SCIPsetEmphasis(scip, SCIP_PARAMEMPHASIS_DEFAULT, TRUE));
if (opt_scip_cpu > 0)
MY_SCIP_CALL(SCIPsetRealParam(scip, "limits/time", opt_scip_cpu));
if (opt_verbosity <= 1)
Expand Down

0 comments on commit cb5ebd1

Please sign in to comment.