Skip to content

Commit ddec42c

Browse files
committed
enable simplification in probing
1 parent 8cb49eb commit ddec42c

File tree

1 file changed

+3
-4
lines changed

1 file changed

+3
-4
lines changed

ortools/sat/integer_search.cc

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1634,10 +1634,9 @@ SatSolver::Status ContinuousProber::Probe() {
16341634
if (!sat_solver_->ResetToLevelZero()) return SatSolver::INFEASIBLE;
16351635

16361636
while (!time_limit_->LimitReached()) {
1637-
// Run sat in-processing to reduce the size of the clause database.
1638-
if (parameters_.use_sat_inprocessing() &&
1639-
!model_->GetOrCreate<Inprocessing>()->InprocessingRound()) {
1640-
return SatSolver::INFEASIBLE;
1637+
if (parameters_.minimize_with_propagation_restart_period() >= 0) {
1638+
sat_solver_->MinimizeSomeClauses(
1639+
parameters_.minimize_with_propagation_num_decisions());
16411640
}
16421641

16431642
// Probe each Boolean variable at most once per loop.

0 commit comments

Comments
 (0)