This commit is contained in:
Laurent Perron
2025-12-15 14:20:08 +01:00
committed by Corentin Le Molgat
parent ae82a37616
commit 39b915c763

View File

@@ -190,7 +190,7 @@ bool ProbeLiteral(Literal assumption, SatSolver* solver) {
}
solver->mutable_logger()->EnableLogging(old_log_state);
return solver->Assignment().LiteralIsAssigned(assumption);
return true;
}
// A core cannot be all true.
@@ -775,9 +775,12 @@ SatSolver::Status CoreBasedOptimizer::OptimizeWithSatEncoding(
}
if (parameters_->cover_optimization() && encoder.nodes().size() > 1) {
if (ProbeLiteral(
encoder.mutable_nodes()->back()->GetAssumption(sat_solver_),
sat_solver_)) {
const Literal last_assumption =
encoder.mutable_nodes()->back()->GetAssumption(sat_solver_);
if (!ProbeLiteral(last_assumption, sat_solver_)) {
return SatSolver::INFEASIBLE;
}
if (sat_solver_->Assignment().LiteralIsAssigned(last_assumption)) {
previous_core_info = "cover";
continue;
}