Skip to content

Commit

Permalink
Fixing the problem with a goal value of the first assignment given by…
Browse files Browse the repository at this point in the history
… CaDiCaL
  • Loading branch information
marekpiotrow committed Jul 13, 2024
1 parent c9ef220 commit a8a97d4
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions MsSolver.cc
Original file line number Diff line number Diff line change
Expand Up @@ -454,13 +454,17 @@ void MsSolver::maxsat_solve(solve_Command cmd)
for (Var x = 0; x < pb_n_vars; x++)
assert(sat_solver.modelValue(x) != l_Undef),
best_model.push(sat_solver.modelValue(x) == l_True);

}
if (status == l_Undef && termCallback != nullptr && 0 != termCallback(termCallbackState))
asynch_interrupt = true;
if (soft_cls.size() == 0) {
if (!ipamir_used) opt_satisfiable_out = false;
return;
} else if (status == l_True) {
for (int i = 0; i < soft_cls.size(); i++)
if (soft_cls[i].snd->size() > 1)
best_model[var(soft_cls[i].snd->last())] = !sign(soft_cls[i].snd->last());
Minisat::vec<Lit> soft_unsat;
best_goalvalue = fixed_goalval + evalGoal(soft_cls, best_model, soft_unsat);
char* tmp = toString(best_goalvalue);
Expand Down

0 comments on commit a8a97d4

Please sign in to comment.