File tree Expand file tree Collapse file tree 1 file changed +7
-4
lines changed
Expand file tree Collapse file tree 1 file changed +7
-4
lines changed Original file line number Diff line number Diff line change @@ -190,7 +190,7 @@ bool ProbeLiteral(Literal assumption, SatSolver* solver) {
190190 }
191191
192192 solver->mutable_logger ()->EnableLogging (old_log_state);
193- return solver-> Assignment (). LiteralIsAssigned (assumption) ;
193+ return true ;
194194}
195195
196196// A core cannot be all true.
@@ -775,9 +775,12 @@ SatSolver::Status CoreBasedOptimizer::OptimizeWithSatEncoding(
775775 }
776776
777777 if (parameters_->cover_optimization () && encoder.nodes ().size () > 1 ) {
778- if (ProbeLiteral (
779- encoder.mutable_nodes ()->back ()->GetAssumption (sat_solver_),
780- sat_solver_)) {
778+ const Literal last_assumption =
779+ encoder.mutable_nodes ()->back ()->GetAssumption (sat_solver_);
780+ if (!ProbeLiteral (last_assumption, sat_solver_)) {
781+ return SatSolver::INFEASIBLE;
782+ }
783+ if (sat_solver_->Assignment ().LiteralIsAssigned (last_assumption)) {
781784 previous_core_info = " cover" ;
782785 continue ;
783786 }
You can’t perform that action at this time.
0 commit comments