Skip to content

Commit 40f10a3

Browse files
marekpiotrowmarekpiotrow
committed
Making the solver compatible with CaDiCaL 3.0 and BVA (factor)
1 parent 4de9cdb commit 40f10a3

17 files changed

Lines changed: 141 additions & 82 deletions

‎CadicalWrap.h‎

Lines changed: 54 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -46,14 +46,12 @@ class SimpSolver {
4646
bool terminate() { return timesup; }
4747
} alarm_term;
4848

49-
int lit2val(Lit p) {
50-
return sign(p) ? -var(p)-1 : var(p)+1;
51-
}
52-
5349

5450
private:
5551
int nvars, nclauses, old_verbosity;
5652
vec<int> model;
53+
vec<int> var_offset, // offsets between CaDiCaL vars and the corresponding MiniSat vars
54+
var_counts; // var_counts[i]: the number of variables with offset <= var_offset[i]
5755

5856
class IpasirTerm : public CaDiCaL::Terminator {
5957
public:
@@ -73,12 +71,37 @@ class SimpSolver {
7371
solver = new CaDiCaL::Solver;
7472
limitTime(opt_cpu_lim);
7573
verbosity = old_verbosity = solver->get("verbose");
74+
var_offset.push(1);
75+
var_counts.push(0);
7676
solver->set("seed",0);
7777
solver->set("stats",0);
7878
solver->prefix("c [CDCL] ");
79+
#if CADICAL_MAJOR >= 3
80+
solver->set("luckyassumptions",0);
81+
solver->set("deduplicateallinit",1);
82+
solver->set("factor",1);
83+
#endif
7984
}
8085
~SimpSolver() { delete solver; }
8186

87+
int lit2val(Lit p) {
88+
int i = 0;
89+
while (i < var_counts.size() && var(p) >= var_counts[i]) i++;
90+
return sign(p) ? -var(p) - var_offset[i] : var(p) + var_offset[i];
91+
}
92+
93+
Var cadical_declared_var(int v) {
94+
if (v <= 0 || v >= var_counts.last() + var_offset.last()) return var_Undef;
95+
int i = 0;
96+
while (v >= var_counts[i] + var_offset[i]) i++;
97+
return i > 0 && abs(v) < var_counts[i - 1] + var_offset[i] ? var_Undef : v - var_offset[i];
98+
}
99+
100+
Lit val2lit(int v) {
101+
Var p = cadical_declared_var(abs(v));
102+
return p == var_Undef ? lit_Undef : mkLit(p, v < 0);
103+
}
104+
82105
void limitTime(int time_limit) {
83106
alarm_term.timesup = false;
84107
#if !defined(_MSC_VER) && !defined(__MINGW32__)
@@ -103,7 +126,11 @@ class SimpSolver {
103126
public:
104127
vec<uint32_t> elimCls;
105128
public:
129+
#if CADICAL_MAJOR >= 3
130+
bool witness (const std::vector<int> &cl, const std::vector<int> &witness, int64_t ) {
131+
#else
106132
bool witness (const std::vector<int> &cl, const std::vector<int> &witness, uint64_t ) {
133+
#endif
107134
for (const int w : witness) elimCls.push(toInt(mkLit(abs(w) - 1, w < 0)));
108135
elimCls.push(witness.size());
109136
for (const int c : cl) elimCls.push(toInt(mkLit(abs(c) - 1, c < 0)));
@@ -114,9 +141,18 @@ class SimpSolver {
114141

115142
Var newVar(bool polarity = true, bool dvar = true) {
116143
(void)polarity; (void)dvar;
117-
Var v = nvars++;
118-
solver->reserve((int)(v+1));
119-
return v;
144+
Var evar = nvars++;
145+
#if CADICAL_MAJOR >= 3
146+
int cvar = solver->declare_one_more_variable(); // CaDiCaL new var
147+
#else
148+
int cvar = nvars;
149+
#endif
150+
if (cvar == var_counts.last() + var_offset.last()) var_counts.last()++;
151+
else {
152+
var_offset.push(cvar - var_counts.last());
153+
var_counts.push(var_counts.last() + 1);
154+
}
155+
return evar;
120156
}
121157
int nVars() const { return solver->vars(); }
122158
int nFreeVars() const { return solver->active(); }
@@ -164,8 +200,9 @@ class SimpSolver {
164200
int ret = solver->solve();
165201
conflicts = solver->conflicts();
166202
if (ret == 10) {
167-
model.growTo(nvars);
168-
for (int v = 0 ; v < nvars; v++) model[v] = solver->val(v + 1);
203+
int nv = solver->vars();
204+
model.growTo(nv);
205+
for (int v = 0 ; v < nv; v++) model[v] = solver->val(v + 1);
169206
}
170207
return ret == 10 ? l_True : (ret == 20 ? l_False : l_Undef);
171208
}
@@ -195,22 +232,24 @@ class SimpSolver {
195232
bool eliminate(bool) { return solver->simplify() != 20; }
196233
bool isEliminated(Var) { /* not needed */ return false; }
197234

198-
lbool value(Var v) const {
199-
int val = solver->fixed(v+1);
235+
lbool value(Var v) {
236+
int cvar = lit2val(mkLit(v));
237+
int val = solver->fixed(cvar);
200238
return val == 0 ? l_Undef : (val > 0 ? l_True : l_False);
201239
}
202-
lbool value(Lit p) const {
240+
lbool value(Lit p) {
203241
lbool val = value(var(p));
204242
if (sign(p))
205243
if (val == l_True) val = l_False; else if (val == l_False) val = l_True;
206244
return val;
207245
}
208246

209-
lbool modelValue(Var v) const {
210-
int val = (v < model.size() ? model[v] : 0);
247+
lbool modelValue(Var v) {
248+
int cvar = lit2val(mkLit(v));
249+
int val = (cvar <= model.size() ? model[cvar - 1] : 0);
211250
return val == 0 ? l_Undef : (val > 0 ? l_True : l_False);
212251
}
213-
lbool modelValue(Lit p) const {
252+
lbool modelValue(Lit p) {
214253
lbool val = modelValue(var(p));
215254
if (sign(p))
216255
if (val == l_True) val = l_False; else if (val == l_False) val = l_True;

‎Main_utils.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
2222
#define MAIN_UTILS_H
2323

2424
#ifndef UWR_VERSION
25-
#define UWR_VERSION "1.7.3"
25+
#define UWR_VERSION "1.7.4"
2626
#endif
2727

2828
extern bool opt_model_out;

‎MsSolver.cc‎

Lines changed: 18 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -88,19 +88,25 @@ Int evalGoal(const vec<Pair<weight_t, Minisat::vec<Lit>* > >& soft_cls, vec<bool
8888
Minisat::vec<Lit>&soft_unsat)
8989
{
9090
Int sum = 0;
91-
bool sat = false;
9291
soft_unsat.clear();
9392
for (int i = 0; i < soft_cls.size(); i++) {
94-
Lit p = soft_cls[i].snd->last(); if (soft_cls[i].snd->size() == 1) p = ~p;
93+
bool sat;
94+
Lit p = soft_cls[i].snd->last();
9595
assert(var(p) < model.size());
96-
if ((( sign(p) && !model[var(p)]) || (!sign(p) && model[var(p)]))
97-
&& !(sat = satisfied_soft_cls(soft_cls[i].snd, model))) {
96+
97+
if (soft_cls[i].snd->size() == 1) {
98+
sat = (sign(p) && !model[var(p)]) || (!sign(p) && model[var(p)]);
99+
p = ~p;
100+
} else {
101+
sat = satisfied_soft_cls(soft_cls[i].snd, model);
102+
model[var(p)] = (sat ? sign(p) : !sign(p));
103+
}
104+
if (! sat) {
98105
if (opt_output_top > 0) soft_unsat.push(~p);
99106
sum += soft_cls[i].fst;
100107
} else if (opt_output_top > 0) {
101108
soft_unsat.push(p);
102109
}
103-
if (sat) { sat = false; model[var(p)] = !model[var(p)]; }
104110
}
105111
return sum;
106112
}
@@ -546,9 +552,6 @@ void MsSolver::maxsat_solve(solve_Command cmd)
546552
}
547553
return;
548554
} else if (status == l_True) {
549-
for (int i = 0; i < soft_cls.size(); i++)
550-
if (soft_cls[i].snd->size() > 1)
551-
best_model[var(soft_cls[i].snd->last())] = !sign(soft_cls[i].snd->last());
552555
Minisat::vec<Lit> soft_unsat;
553556
best_goalvalue = fixed_goalval + evalGoal(soft_cls, best_model, soft_unsat);
554557
char* tmp = toString(best_goalvalue);
@@ -755,6 +758,8 @@ void MsSolver::maxsat_solve(solve_Command cmd)
755758
lbool status;
756759
do { // a loop to process GBMO splitting points
757760
while (1) {
761+
if (opt_unsat_cpu == 0 && opt_minimization == 1 && opt_to_bin_search)
762+
goto SwitchSearchMethod;
758763
if (opt_minimization != 1 && opt_to_bin_search && opt_alternating_bin_search)
759764
opt_minimization = 2 - opt_minimization;
760765
#ifdef USE_SCIP
@@ -787,7 +792,9 @@ void MsSolver::maxsat_solve(solve_Command cmd)
787792
}
788793
}
789794
signal(SIGINT, SIGINT_interrupt);
795+
#ifdef SIGALRM
790796
signal(SIGALRM, SIGINT_interrupt);
797+
#endif
791798
signal(SIGTERM, SIGTERM_handler);
792799
#ifdef SIGXCPU
793800
signal(SIGXCPU,SIGINT_interrupt);
@@ -884,9 +891,6 @@ void MsSolver::maxsat_solve(solve_Command cmd)
884891
for (Var x = 0; x < pb_n_vars; x++)
885892
assert(sat_solver.modelValue(x) != l_Undef),
886893
model.push(sat_solver.modelValue(x) == l_True);
887-
for (int i = 0; i < top_for_strat; i++)
888-
if (soft_cls[i].snd->size() > 1)
889-
model[var(soft_cls[i].snd->last())] = !sign(soft_cls[i].snd->last());
890894
sat_solver.optimizeModel(soft_cls, model, top_for_strat, top_for_hard - 1);
891895
Int goalvalue = evalGoal(soft_cls, model, soft_unsat) + fixed_goalval;
892896
extern bool opt_satisfiable_out;
@@ -1213,13 +1217,13 @@ void MsSolver::maxsat_solve(solve_Command cmd)
12131217
if (weighted_instance && satisfied && sat_solver.conflicts > 10000)
12141218
harden_soft_cls(assump_ps, assump_Cs, sorted_assump_Cs, delayed_assump, delayed_assump_sum);
12151219
if (opt_minimization >= 1 && opt_verbosity >= 2) {
1216-
char *t; reportf("Lower bound: %s, assump. size: %d, stratif. level: %d (cls: %d, wght: %s)\n", t=toString(LB_goalvalue * goal_gcd),
1217-
assump_ps.size(), sorted_assump_Cs.size(), top_for_strat, toString(sorted_assump_Cs.size() > 0 ? sorted_assump_Cs.last() : 0)); xfree(t); }
1220+
char *t; reportf("Lower bound: %s, assump. size: %d, stratif. level: %d (cls: %d, wght: %s), conflicts: %lu\n", t=toString(LB_goalvalue * goal_gcd),
1221+
assump_ps.size(), sorted_assump_Cs.size(), top_for_strat, toString(sorted_assump_Cs.size() > 0 ? sorted_assump_Cs.last() : 0), sat_solver.conflicts); xfree(t); }
12181222
if (opt_minimization == 2 && opt_verbosity == 1 && use_base_assump) {
12191223
char *t; reportf("Lower bound: %s\n", t=toString(LB_goalvalue * goal_gcd)); xfree(t); }
12201224
SwitchSearchMethod:
12211225
if (opt_minimization == 1 && opt_to_bin_search && LB_goalvalue + 5 < UB_goalvalue &&
1222-
cpuTime() >= opt_unsat_cpu + start_solving_cpu && sat_solver.conflicts > opt_unsat_conflicts) {
1226+
cpuTime() >= opt_unsat_cpu + start_solving_cpu && sat_solver.conflicts >= opt_unsat_conflicts) {
12231227
int cnt = 0;
12241228
for (int j = 0, i = 0; i < psCs.size(); i++) {
12251229
const Int &w = soft_cls[psCs[i].snd].fst;

‎MsSolver.h‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -170,8 +170,8 @@ class MsSolver final : public PbSolver {
170170
else res = sat_solver.addClause(p);
171171
return res;
172172
}
173-
virtual lbool value(Var x) const { return sat_solver.value(x); }
174-
virtual lbool value(Lit p) const { return sat_solver.value(p); }
173+
virtual lbool value(Var x) { return sat_solver.value(x); }
174+
virtual lbool value(Lit p) { return sat_solver.value(p); }
175175
bool addUnit (Lit p) {
176176
if (value(p) == l_Undef) trail.push(p);
177177
return addUnitClause(p);

‎PbSolver.h‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -161,8 +161,8 @@ class PbSolver {
161161

162162
// Helpers (semi-internal):
163163
//
164-
virtual lbool value(Var x) const { return sat_solver.value(x); }
165-
virtual lbool value(Lit p) const { return sat_solver.value(p); }
164+
virtual lbool value(Var x) { return sat_solver.value(x); }
165+
virtual lbool value(Lit p) { return sat_solver.value(p); }
166166
int nVars() const { return sat_solver.nVars(); }
167167
int nClauses() const { return sat_solver.nClauses(); }
168168
int nConstrs() const { return constrs.size(); }

‎SatSolver.cc‎

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,14 @@ static Var mapVar(Var x, Minisat::vec<Var>& map, Var& max)
3434
}
3535
#endif
3636

37+
Var ExtSimpSolver::defined_var(int i) {
38+
#if defined(CADICAL)
39+
return cadical_declared_var(i + 1);
40+
#else
41+
return i >= 0 && i < nvars ? i : var_Undef;
42+
#endif
43+
}
44+
3745
#if !defined(CADICAL) && !defined(CRYPTOMS)
3846
const Minisat::Clause& ExtSimpSolver::getClause (int i, bool &is_satisfied) const
3947
{
@@ -102,18 +110,18 @@ void ExtSimpSolver::optimizeModel(const vec<Pair<weight_t, Minisat::vec<Lit>* >
102110
#if defined(CADICAL)
103111
extern bool satisfied_soft_cls(Minisat::vec<Lit> *cls, vec<bool>& model);
104112
Int sum = 0;
105-
bool sat = false, opt = false;
113+
bool opt = false;
106114
for (int i = to_soft; i >= from_soft; i--) {
107115
Lit p = soft_cls[i].snd->last(); if (soft_cls[i].snd->size() == 1) p = ~p;
108116
assert(var(p) < model.size());
109117
if ((( sign(p) && !model[var(p)]) || (!sign(p) && model[var(p)]))
110-
&& !(sat = satisfied_soft_cls(soft_cls[i].snd, model))) {
111-
if (solver->flip(var(p) + 1)) model[var(p)] = !model[var(p)], opt = true;
118+
&& !satisfied_soft_cls(soft_cls[i].snd, model)) {
119+
if (solver->flip(abs(lit2val(p)))) model[var(p)] = !model[var(p)], opt = true;
112120
}
113-
if (sat) { sat = false; model[var(p)] = !model[var(p)]; }
114121
}
115122
if (opt)
116-
for (int v = model.size() - 1 ; v >= 0; v--) model[v] = solver->val(v + 1) > 0;
123+
for (int v = model.size() - 1 ; v >= 0; v--)
124+
model[v] = solver->val(abs(lit2val(mkLit(v)))) > 0;
117125
#endif
118126
}
119127

@@ -212,8 +220,8 @@ bool ExtSimpSolver::impliedObservedLits(Lit lit, Minisat::vec<Lit>& props, const
212220
if (ret != l_False && extPropagator->dec_level > 1) {
213221
for (const int clit : extPropagator->last_trails[1 - extPropagator->dec_level % 2]) {
214222
if (clit != 0) {
215-
Lit l = mkLit(abs(clit) - 1, clit < 0);
216-
if (l != lit) props.push(l);
223+
Lit l = val2lit(clit);
224+
if (l != lit_Undef && l != lit) props.push(l);
217225
}
218226
}
219227
}

‎SatSolver.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,7 @@ class ExtSimpSolver: public SimpSolver {
102102
#endif
103103
);
104104
}
105+
Var defined_var(int i); // vars in CaDiCaL 3.0 should be explicitly declared
105106
#if !defined(CADICAL) && !defined(CRYPTOMS)
106107
const Minisat::Clause& getClause (int i, bool &is_satisfied) const;
107108
#endif

‎ScipSolver.cc‎

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,11 @@ void scip_interrupt_solve(ScipSolver &scip_solver)
4848

4949
lbool set_scip_var(SCIP *scip, MsSolver *solver, std::vector<SCIP_VAR *> &vars, Lit lit)
5050
{
51+
if (size_t(var(lit)) >= vars.size())
52+
vars.resize(var(lit) + 1, nullptr);
53+
if (size_t(var(lit)) >= solver->scip_solver.model.size())
54+
solver->scip_solver.model.resize(var(lit) + 1);
55+
5156
SCIP_VAR *scip_var = vars[var(lit)];
5257
if (scip_var == nullptr) {
5358
Var v = var(lit);
@@ -145,7 +150,7 @@ lbool printScipStats(ScipSolver *scip_solver)
145150
return l_Undef;
146151
}
147152

148-
void saveFixedVariables(ScipSolver *scip_solver)
153+
void saveFixedVariables(ScipSolver *scip_solver, MsSolver *solver)
149154
{
150155
std::lock_guard<std::mutex> lck(fixed_vars_mtx);
151156
int fixed = 0;
@@ -160,8 +165,10 @@ void saveFixedVariables(ScipSolver *scip_solver)
160165
SCIPisZero(scip_solver->scip, ub) ? l_False :
161166
(SCIPisZero(scip_solver->scip, lb - 1) &&
162167
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;
168+
Var v = solver->sat_solver.defined_var(i);
169+
if (val != l_Undef && v != var_Undef) {
170+
scip_solver->fixed_vars.push(mkLit(v, val == l_False)), ++fixed;
171+
}
165172
}
166173
}
167174
}
@@ -304,7 +311,7 @@ lbool scip_solve_async(ScipSolver *scip_solver, MsSolver *solver)
304311
}
305312
}
306313
if (opt_scip_cpu == 0 && !scip_solver->interrupted) {
307-
saveFixedVariables(scip_solver);
314+
saveFixedVariables(scip_solver, solver);
308315
MY_SCIP_CALL(SCIPsetRealParam(scip_solver->scip, "limits/time", 1e+20));
309316
try_again = true;
310317
}
@@ -342,7 +349,7 @@ lbool scip_solve_async(ScipSolver *scip_solver, MsSolver *solver)
342349
std::_Exit(30);
343350
}
344351
}
345-
} else saveFixedVariables(scip_solver);
352+
} else saveFixedVariables(scip_solver, solver);
346353
clean_and_return:
347354
// release SCIP vars
348355
for (auto v: scip_solver->vars)

‎config.cadical‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ MAXPRE?=-D MAXPRE
33
USESCIP?=-D USE_SCIP -pthread -lmpfr
44
BIGWEIGHTS?=#-D BIG_WEIGHTS
55
MINISATP_RELSYM?=
6-
MINISATP_REL?=-std=c++11 -O3 -D NDEBUG -Wno-strict-aliasing -D CADICAL $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)
7-
MINISATP_DEB?=-std=c++11 -O0 -D DEBUG -Wno-strict-aliasing -D CADICAL $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)
8-
MINISATP_PRF?=-std=c++11 -O3 -D NDEBUG -Wno-strict-aliasing -D CADICAL $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)
6+
MINISATP_REL?=-std=c++14 -O3 -D NDEBUG -Wno-strict-aliasing -D CADICAL $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)
7+
MINISATP_DEB?=-std=c++14 -O0 -D DEBUG -Wno-strict-aliasing -D CADICAL $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)
8+
MINISATP_PRF?=-std=c++14 -O3 -D NDEBUG -Wno-strict-aliasing -D CADICAL $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)
99
MINISATP_FPIC?=-fpic
1010
MINISAT_INCLUDE?=-I/include -I/include/minisat -I../cominisatps -I../cadical/src
11-
MINISAT_LIB?=-L/lib -L../cadical/build -lcadical $(USESCIP)
11+
MINISAT_LIB?=-flto -L/lib -L../cadical/build -lcadical $(USESCIP)
1212
ifneq ($(MAXPRE),)
1313
MCL_INCLUDE?=-I../maxpre/src
1414
MCL_LIB?=-L../maxpre/src/lib -lmaxpre

‎config.cominisatps‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ MAXPRE?=-D MAXPRE
33
USESCIP?=-D USE_SCIP -pthread -lmpfr
44
BIGWEIGHTS?=#-D BIG_WEIGHTS
55
MINISATP_RELSYM?=
6-
MINISATP_REL?=-std=c++11 -O3 -D NDEBUG -Wno-strict-aliasing -D COMINISATPS $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)
7-
MINISATP_DEB?=-std=c++11 -O0 -D DEBUG -Wno-strict-aliasing -D COMINISATPS $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)
8-
MINISATP_PRF?=-std=c++11 -O3 -D NDEBUG -Wno-strict-aliasing -D COMINISATPS $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)
6+
MINISATP_REL?=-std=c++14 -O3 -D NDEBUG -Wno-strict-aliasing -D COMINISATPS $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)
7+
MINISATP_DEB?=-std=c++14 -O0 -D DEBUG -Wno-strict-aliasing -D COMINISATPS $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)
8+
MINISATP_PRF?=-std=c++14 -O3 -D NDEBUG -Wno-strict-aliasing -D COMINISATPS $(MAXPRE) $(USESCIP) $(BIGWEIGHTS)
99
MINISATP_FPIC?=-fpic
1010
MINISAT_INCLUDE?=-I/include -I/include/cominisatps -I../cominisatps
11-
MINISAT_LIB?=-L/lib -L../cominisatps/build/release/lib -lcominisatps $(USESCIP)
11+
MINISAT_LIB?=-flto -L/lib -L../cominisatps/build/release/lib -lcominisatps $(USESCIP)
1212
ifneq ($(MAXPRE),)
1313
MCL_INCLUDE?=-I../maxpre/src
1414
MCL_LIB?=-L../maxpre/src/lib -lmaxpre

0 commit comments

Comments
 (0)