Skip to content

Commit 230faa1

Browse files
marekpiotrowmarekpiotrow
committed
Tuning the usage of SCIP solver for pseudo-Boolean constraints
1 parent 840c0b0 commit 230faa1

15 files changed

+48
-27
lines changed

‎ADTs/Global.h‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -120,17 +120,17 @@ template<class T> macro T* xmalloc(size_t size) {
120120
T* tmp = (T*)malloc(size * sizeof(T));
121121
assert(size == 0 || tmp != NULL);
122122
if (size != 0 && tmp == NULL) { // M. Piotrow 11.10.2017
123-
exit(0);
124-
//std::bad_alloc exc; throw exc;
123+
//exit(0);
124+
std::bad_alloc exc; throw exc;
125125
}
126126
return tmp; }
127127

128128
template<class T> macro T* xrealloc(T* ptr, size_t size) {
129129
T* tmp = (T*)realloc((void*)ptr, size * sizeof(T));
130130
assert(size == 0 || tmp != NULL);
131131
if (size != 0 && tmp == NULL) { // M. Piotrow 11.10.2017
132-
exit(0);
133-
//std::bad_alloc exc; throw exc;
132+
//exit(0);
133+
std::bad_alloc exc; throw exc;
134134
}
135135
return tmp; }
136136

‎MsSolver.cc‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -445,6 +445,7 @@ void MsSolver::maxsat_solve(solve_Command cmd)
445445
#ifdef USE_SCIP
446446
extern bool opt_force_scip, opt_use_scip_slvr, opt_scip_parallel;
447447
extern double opt_scip_delay;
448+
bool start_delayed_scip_solver = false;
448449
#endif
449450
bool opt_alternating_bin_search = (opt_minimization == 1 && opt_to_bin_search);
450451
bool pb_decision_problem = (!opt_maxsat && !ipamir_used && soft_cls.size() == 0);
@@ -471,9 +472,10 @@ void MsSolver::maxsat_solve(solve_Command cmd)
471472
reportf("Converting %d PB-constraints to clauses...\n", constrs.size());
472473
propagate();
473474
#ifdef USE_SCIP
474-
if (opt_use_scip_slvr && declared_intsize <= std::numeric_limits<double>::digits) {
475+
if (opt_use_scip_slvr && declared_intsize <= std::numeric_limits<double>::digits - 6) {
475476
opt_force_scip = true;
476477
scip_init(scip_solver, sat_solver.nVars());
478+
scip_solver.pb_decision_problem = pb_decision_problem;
477479
if (opt_scip_parallel && opt_scip_delay == 0) {
478480
Minisat::vec<Lit> assump_ps;
479481
vec<Int> assump_Cs;
@@ -758,8 +760,8 @@ void MsSolver::maxsat_solve(solve_Command cmd)
758760
if (opt_minimization != 1 && opt_to_bin_search && opt_alternating_bin_search)
759761
opt_minimization = 2 - opt_minimization;
760762
#ifdef USE_SCIP
761-
if (scip_solver.must_be_started && cpuTime() >= opt_scip_delay) {
762-
scip_solver.must_be_started = false;
763+
if (scip_solver.must_be_started && (cpuTime() >= opt_scip_delay || start_delayed_scip_solver)) {
764+
scip_solver.must_be_started = start_delayed_scip_solver = false;
763765
if (opt_cpu_lim > cpuTime()) LimitTime(opt_cpu_lim); else break;
764766
sat_solver.clearInterrupt();
765767
if (asynch_interrupt)
@@ -833,6 +835,7 @@ void MsSolver::maxsat_solve(solve_Command cmd)
833835
sat_solver.clearInterrupt();
834836
asynch_interrupt = cpu_interrupt = false; LimitTime(opt_cpu_lim);
835837
}
838+
start_delayed_scip_solver = true;
836839
continue;
837840
}
838841
#endif

‎PbSolver_convert.cc‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,8 @@ Formula buildConstraint(const Linear& c, bool soft_constr = true, int max_cost =
3131
Formula convertToBdd (const Linear& c, int max_cost = INT_MAX); // From: PbSolver_convertBdd.C
3232
//-------------------------------------------------------------------------------------------------
3333

34+
extern void handlerOutputResult(const PbSolver& S, bool optimum);
35+
3436
void clear_shared_formulas() {
3537
extern void clear_clausifier_static_maps();
3638

@@ -93,6 +95,7 @@ bool PbSolver::convertPbs(bool first_call)
9395
if (opt_convert != ct_Adders) { opt_convert = ct_Adders; continue; }
9496
else {
9597
reportf("Out of memery in converting constraints: %s\n",ba.what());
98+
handlerOutputResult(*this, false);
9699
_Exit(0);
97100
}
98101
}
@@ -114,6 +117,7 @@ bool PbSolver::convertPbs(bool first_call)
114117
reportf("New vars/cls: %d/%d\n", -nvars, -ncls);
115118
} catch (std::bad_alloc& ba) {
116119
reportf("Out of memery in clausifying constraints: %s\n",ba.what());
120+
handlerOutputResult(*this, false);
117121
_Exit(0);
118122
}
119123
return okay();

‎README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ Since version 1.7.0 the default SAT solver is changed to CaDiCaL by Armin Biere.
4646
tar zxvf scipoptsuite-9.2.2.tgz
4747
cd scipoptsuite-9.2.2
4848
mkdir build && cd build
49-
cmake -DSYM=nauty -DSHARED=off -DNO_EXTERNAL_CODE=on -DSOPLEX=on -DGMP=on -DBOOTS=on -DTPI=tny ..
49+
cmake -DSYM=nauty -DSHARED=off -DNO_EXTERNAL_CODE=on -DSOPLEX=on -DGMP=on -DMPFR=on -DBOOTS=on -DTPI=tny ..
5050
cmake --build . --config Release --target libscip libsoplex-pic
5151
cd ../..
5252

‎ScipSolver.cc‎

Lines changed: 21 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -178,6 +178,10 @@ lbool scip_solve_async(ScipSolver *scip_solver, MsSolver *solver)
178178
SCIP_SOL *sol = SCIPgetBestSol(scip_solver->scip);
179179
assert(sol != nullptr);
180180
// MY_SCIP_CALL(SCIPprintSol(scip_solver->scip, sol, nullptr, FALSE));
181+
SCIP_Bool feasible = FALSE;
182+
MY_SCIP_CALL(SCIPcheckSolOrig(scip_solver->scip, sol, &feasible, FALSE, FALSE));
183+
if (!feasible) { found_opt = l_Undef; goto clean_and_return; }
184+
181185
best_value = scip_solver->obj_offset + long(round(SCIPgetSolOrigObj(scip_solver->scip, sol)));
182186
for (Var x = 0; x < (int)scip_solver->vars.size(); x++)
183187
{
@@ -236,7 +240,9 @@ lbool scip_solve_async(ScipSolver *scip_solver, MsSolver *solver)
236240
SCIP_SOL *sol = SCIPgetBestSol(scip_solver->scip);
237241
if (sol != nullptr) {
238242
Int scip_sol = (scip_solver->obj_offset + int64_t(round(SCIPgetSolOrigObj(scip_solver->scip, sol))))/gcd;
239-
if (scip_sol < solver->best_goalvalue) {
243+
SCIP_Bool feasible = FALSE;
244+
MY_SCIP_CALL(SCIPcheckSolOrig(scip_solver->scip, sol, &feasible, FALSE, FALSE));
245+
if (feasible && scip_sol < solver->best_goalvalue) {
240246
for (Var x = 0; x < (int)scip_solver->vars.size(); x++)
241247
if (scip_solver->vars[x] != nullptr) {
242248
SCIP_Real v = SCIPgetSolVal(scip_solver->scip, sol, scip_solver->vars[x]);
@@ -280,7 +286,7 @@ lbool scip_solve_async(ScipSolver *scip_solver, MsSolver *solver)
280286
std::lock_guard<std::mutex> lck(optsol_mtx);
281287
char test = OPT_NONE;
282288
if (opt_finder.compare_exchange_strong(test, OPT_SCIP)) {
283-
if (!solver->ipamir_used || opt_verbosity > 0)
289+
if (!scip_solver->pb_decision_problem && (!solver->ipamir_used || opt_verbosity > 0))
284290
reportf("SCIP optimum (rounded): %" PRId64 "\n", best_value);
285291
solver->best_goalvalue = best_value;
286292
vec<lbool> opt_model(scip_solver->model.size());
@@ -293,14 +299,14 @@ lbool scip_solve_async(ScipSolver *scip_solver, MsSolver *solver)
293299
solver->best_goalvalue = (solver->fixed_goalval + evalGoal(solver->soft_cls, solver->best_model, soft_unsat)) * solver->goal_gcd;
294300

295301
extern bool opt_satisfiable_out;
296-
opt_satisfiable_out = false;
302+
opt_satisfiable_out = scip_solver->pb_decision_problem;
297303

298304
if (opt_verbosity >= 1) {
299305
printScipStats(scip_solver);
300306
solver->printStats(false);
301307
}
302308
if (!solver->ipamir_used) {
303-
outputResult(*solver, true);
309+
outputResult(*solver, !scip_solver->pb_decision_problem);
304310
std::this_thread::sleep_for(std::chrono::milliseconds(10));
305311
//MY_SCIP_CALL(SCIPfree(&scip_solver->scip));
306312
std::_Exit(30);
@@ -372,9 +378,16 @@ lbool MsSolver::scip_init(ScipSolver &scip_solver, int sat_orig_vars)
372378
if (opt_verbosity <= 1)
373379
MY_SCIP_CALL(SCIPsetIntParam(scip, "display/verblevel", 0));
374380
if (declared_intsize > 0 && declared_intsize < 49) {
375-
SCIP_Real feastol = pow(0.5,declared_intsize);
376-
if (feastol < 1e-06)
377-
MY_SCIP_CALL(SCIPsetRealParam(scip, "numerics/feastol", feastol));
381+
SCIP_Real feastol, newfeastol = pow(0.5,declared_intsize), epsilon, sumepsilon;
382+
MY_SCIP_CALL(SCIPgetRealParam(scip, "numerics/feastol", &feastol));
383+
MY_SCIP_CALL(SCIPgetRealParam(scip, "numerics/epsilon", &epsilon));
384+
MY_SCIP_CALL(SCIPgetRealParam(scip, "numerics/sumepsilon", &sumepsilon));
385+
if (newfeastol < feastol)
386+
MY_SCIP_CALL(SCIPsetRealParam(scip, "numerics/feastol", newfeastol));
387+
if (newfeastol < epsilon)
388+
MY_SCIP_CALL(SCIPsetRealParam(scip, "numerics/epsilon", newfeastol));
389+
if (newfeastol < sumepsilon)
390+
MY_SCIP_CALL(SCIPsetRealParam(scip, "numerics/sumepsilon", newfeastol));
378391
}
379392
scip_solver.model.resize(sat_orig_vars);
380393
for (Var x = sat_orig_vars - 1; x >= 0; x--) scip_solver.model[x] = sat_solver.value(x);
@@ -499,7 +512,7 @@ lbool MsSolver::scip_solve(const Minisat::vec<Lit> *assump_ps,
499512
(opt_scip_parallel? "in a separate thread" : ""), opt_scip_cpu);
500513

501514
scip_solver.obj_offset = obj_offset;
502-
if (opt_scip_delay > cpuTime() + 1) {
515+
if (opt_scip_delay > cpuTime() + 10) {
503516
scip_solver.must_be_started = true;
504517
if (!ipamir_used || opt_verbosity > 0) reportf("SCIP start delayed for at least %.0fs\n", opt_scip_delay - cpuTime());
505518
return l_Undef;

‎ScipSolver.h‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,13 +30,14 @@ struct ScipSolver {
3030
std::vector<SCIP_VAR *> vars;
3131
std::vector<lbool> model;
3232
int64_t obj_offset;
33+
bool pb_decision_problem;
3334
bool must_be_started;
3435
bool started;
3536
bool interrupted;
3637
std::future<lbool> asynch_result;
3738

38-
ScipSolver() : scip(nullptr), obj_offset(0), must_be_started(false), started(false),
39-
interrupted(false) {}
39+
ScipSolver() : scip(nullptr), obj_offset(0), pb_decision_problem(false), must_be_started(false),
40+
started(false), interrupted(false) {}
4041
} ;
4142

4243
void scip_interrupt_solve(ScipSolver &scip);

‎config.cadical‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
BUILD_DIR?=build
22
MAXPRE?=-D MAXPRE
3-
USESCIP?=-D USE_SCIP -pthread
3+
USESCIP?=-D USE_SCIP -pthread -lmpfr
44
BIGWEIGHTS?=#-D BIG_WEIGHTS
55
MINISATP_RELSYM?=
66
MINISATP_REL?=-std=c++11 -O3 -D NDEBUG -Wno-strict-aliasing -D CADICAL $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)

‎config.cominisatps‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
BUILD_DIR?=build
22
MAXPRE?=-D MAXPRE
3-
USESCIP?=-D USE_SCIP -pthread
3+
USESCIP?=-D USE_SCIP -pthread -lmpfr
44
BIGWEIGHTS?=#-D BIG_WEIGHTS
55
MINISATP_RELSYM?=
66
MINISATP_REL?=-std=c++11 -O3 -D NDEBUG -Wno-strict-aliasing -D COMINISATPS $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)

‎config.cryptoms‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
BUILD_DIR?=build
22
MAXPRE?=-D MAXPRE
3-
USESCIP?=#-D USE_SCIP -pthread
3+
USESCIP?=#-D USE_SCIP -pthread -lmpfr
44
BIGWEIGHTS?=#-D BIG_WEIGHTS
55
MINISATP_RELSYM?=
66
MINISATP_REL?=-std=c++11 -O3 -D NDEBUG -Wno-strict-aliasing -D CRYPTOMS $(USESCIP) $(MAXPRE) $(BIGWEIGHTS)

‎config.glucose3‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
BUILD_DIR?=build
22
MAXPRE?=-D MAXPRE
3-
USESCIP?=-D USE_SCIP -pthread
3+
USESCIP?=-D USE_SCIP -pthread -lmpfr
44
BIGWEIGHTS?=#-D BIG_WEIGHTS
55
MINISATP_RELSYM?=
66
MINISATP_REL?=-std=c++11 -O3 -D NDEBUG -Wno-strict-aliasing -D INCREMENTAL -D GLUCOSE3 $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)

0 commit comments

Comments
 (0)