Skip to content

Commit 3d5b65c

Browse files
marekpiotrowmarekpiotrow
committed
Changing the default value of the parameter scip-delay from 0s to 120s
1 parent 7f56c5e commit 3d5b65c

File tree

2 files changed

+40
-26
lines changed

2 files changed

+40
-26
lines changed

‎Main_utils.cc‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@ double opt_scip_cpu_add = 600;
106106
bool opt_scip_parallel = true;
107107
time_t wall_clock_time;
108108
bool opt_force_scip = false;
109-
double opt_scip_delay = 0;
109+
double opt_scip_delay = 120;
110110
#endif
111111

112112
char* opt_input = NULL;
@@ -467,7 +467,7 @@ static cchar* doc =
467467
" -scip-cpu-add= Time in seconds for SCIP solver to increase timeout if the gap <= 10%%. [def: %gs]\n"
468468
" -no-par Do not run SCIP solver in a separate thread. Timeout is changed to %gs if not set by user. \n"
469469
" -force-scip Force to run SCIP solver. (The default setting is to use it for small instances.)\n"
470-
" -scip-delay= Time in seconds to delay SCIP start. Zero - no delay (default)\n"
470+
" -scip-delay= Time in seconds to delay SCIP start. Zero - no delay. [def: %gs]\n"
471471
#endif
472472
"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\n"
473473
;
@@ -514,6 +514,7 @@ static void parseOptions(int argc, char** argv, bool check_files)
514514
#ifdef USE_SCIP
515515
, opt_scip_cpu_add
516516
, opt_scip_cpu_default
517+
, opt_scip_delay
517518
#endif
518519
), exit(0);
519520

@@ -618,6 +619,7 @@ static void parseOptions(int argc, char** argv, bool check_files)
618619
#ifdef USE_SCIP
619620
, opt_scip_cpu_add
620621
, opt_scip_cpu_default
622+
, opt_scip_delay
621623
#endif
622624
), exit(0);
623625
#ifdef USE_SCIP

‎ScipSolver.cc‎

Lines changed: 36 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -145,6 +145,29 @@ lbool printScipStats(ScipSolver *scip_solver)
145145
return l_Undef;
146146
}
147147

148+
void saveFixedVariables(ScipSolver *scip_solver)
149+
{
150+
std::lock_guard<std::mutex> lck(fixed_vars_mtx);
151+
int fixed = 0;
152+
for (int i = 0; i < (int)scip_solver->vars.size(); i++) {
153+
SCIP_VAR *v = scip_solver->vars[i];
154+
if (v != nullptr) {
155+
SCIP_VAR * trans_var = SCIPvarGetTransVar(v);
156+
if (trans_var != nullptr && SCIPvarGetStatus(trans_var) == SCIP_VARSTATUS_FIXED) {
157+
SCIP_Real lb = SCIPvarGetLbGlobal(trans_var),
158+
ub = SCIPvarGetUbGlobal(trans_var);
159+
lbool val = (SCIPisZero(scip_solver->scip, lb) &&
160+
SCIPisZero(scip_solver->scip, ub) ? l_False :
161+
(SCIPisZero(scip_solver->scip, lb - 1) &&
162+
SCIPisZero(scip_solver->scip, ub - 1) ? l_True : l_Undef));
163+
if (val != l_Undef)
164+
scip_solver->fixed_vars.push(mkLit(i, val == l_False)), ++fixed;
165+
}
166+
}
167+
}
168+
if (opt_verbosity >= 2 && fixed > 0) reportf("SCIP fixed %d vars\n", fixed);
169+
}
170+
148171
lbool scip_solve_async(ScipSolver *scip_solver, MsSolver *solver)
149172
{
150173
extern double opt_scip_cpu, opt_scip_cpu_add;
@@ -218,7 +241,7 @@ lbool scip_solve_async(ScipSolver *scip_solver, MsSolver *solver)
218241
int64_t(round(dualb)) + scip_solver->obj_offset : INT64_MIN);
219242
int64_t ubound = (!SCIPisInfinity(scip_solver->scip, primb) ?
220243
int64_t(round(primb)) + scip_solver->obj_offset : INT64_MAX);
221-
if (opt_finder.load() != OPT_MSAT && (!solver->ipamir_used || opt_verbosity > 0))
244+
if (opt_finder.load() != OPT_MSAT && opt_scip_cpu > 0 && (!solver->ipamir_used || opt_verbosity > 0))
222245
reportf("SCIP timeout with lower and upper bounds: [%lld, %lld]\n", lbound, ubound);
223246
int64_t gcd = fromweight(solver->goal_gcd);
224247
if (!SCIPisInfinity(scip_solver->scip, dualb)) {
@@ -268,7 +291,9 @@ lbool scip_solve_async(ScipSolver *scip_solver, MsSolver *solver)
268291
}
269292
}
270293
}
271-
if (!scip_solver->interrupted && lbound != INT64_MIN && try_count > 0 && double(ubound - lbound)/max(int64_t(1),max(abs(lbound),abs(ubound))) < 0.10 && ubound - lbound < bound_gap) {
294+
if (!scip_solver->interrupted && opt_scip_cpu > 0 && lbound != INT64_MIN && try_count > 0 &&
295+
double(ubound - lbound)/max(int64_t(1),max(abs(lbound),abs(ubound))) < 0.10 &&
296+
ubound - lbound < bound_gap) {
272297
try_count--; opt_scip_cpu += opt_scip_cpu_add;
273298
bound_gap = ubound - lbound;
274299
MY_SCIP_CALL(SCIPsetRealParam(scip_solver->scip, "limits/time", opt_scip_cpu));
@@ -278,6 +303,11 @@ lbool scip_solve_async(ScipSolver *scip_solver, MsSolver *solver)
278303
try_again = true;
279304
}
280305
}
306+
if (opt_scip_cpu == 0 && !scip_solver->interrupted) {
307+
saveFixedVariables(scip_solver);
308+
MY_SCIP_CALL(SCIPsetRealParam(scip_solver->scip, "limits/time", 1e+20));
309+
try_again = true;
310+
}
281311
}
282312
} while (try_again);
283313

@@ -312,27 +342,7 @@ lbool scip_solve_async(ScipSolver *scip_solver, MsSolver *solver)
312342
std::_Exit(30);
313343
}
314344
}
315-
} else {
316-
std::lock_guard<std::mutex> lck(fixed_vars_mtx);
317-
int fixed = 0;
318-
for (int i = 0; i < (int)scip_solver->vars.size(); i++) {
319-
SCIP_VAR *v = scip_solver->vars[i];
320-
if (v != nullptr) {
321-
SCIP_VAR * trans_var = SCIPvarGetTransVar(v);
322-
if (trans_var != nullptr && SCIPvarGetStatus(trans_var) == SCIP_VARSTATUS_FIXED) {
323-
SCIP_Real lb = SCIPvarGetLbGlobal(trans_var),
324-
ub = SCIPvarGetUbGlobal(trans_var);
325-
lbool val = (SCIPisZero(scip_solver->scip, lb) &&
326-
SCIPisZero(scip_solver->scip, ub) ? l_False :
327-
(SCIPisZero(scip_solver->scip, lb - 1) &&
328-
SCIPisZero(scip_solver->scip, ub - 1) ? l_True : l_Undef));
329-
if (val != l_Undef)
330-
scip_solver->fixed_vars.push(mkLit(i, val == l_False)), ++fixed;
331-
}
332-
}
333-
}
334-
if (opt_verbosity >= 2 && fixed > 0) reportf("SCIP fixed %d vars\n", fixed);
335-
}
345+
} else saveFixedVariables(scip_solver);
336346
clean_and_return:
337347
// release SCIP vars
338348
for (auto v: scip_solver->vars)
@@ -369,7 +379,7 @@ class ScipClauseIterator : public CaDiCaL::ClauseIterator {
369379

370380
lbool MsSolver::scip_init(ScipSolver &scip_solver, int sat_orig_vars)
371381
{
372-
extern double opt_scip_cpu;
382+
extern double opt_scip_cpu, opt_scip_cpu_add;
373383
extern bool opt_force_scip;
374384

375385
if (scip_solver.scip != nullptr) return l_Undef;
@@ -395,6 +405,8 @@ lbool MsSolver::scip_init(ScipSolver &scip_solver, int sat_orig_vars)
395405
MY_SCIP_CALL(SCIPsetEmphasis(scip, SCIP_PARAMEMPHASIS_DEFAULT, TRUE));
396406
if (opt_scip_cpu > 0)
397407
MY_SCIP_CALL(SCIPsetRealParam(scip, "limits/time", opt_scip_cpu));
408+
else
409+
MY_SCIP_CALL(SCIPsetRealParam(scip, "limits/time", opt_scip_cpu_add));
398410
if (opt_verbosity <= 1)
399411
MY_SCIP_CALL(SCIPsetIntParam(scip, "display/verblevel", 0));
400412
if (declared_intsize > 0 && declared_intsize < 49) {

0 commit comments

Comments
 (0)