diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index e463b8e5df..67427cd223 100644 --- a/ortools/sat/clause.cc +++ b/ortools/sat/clause.cc @@ -244,21 +244,25 @@ bool ClauseManager::Propagate(Trail* trail) { } } - reasons_[trail->Index()] = it->clause; - if (propagation_level == 0 && lrat_proof_handler_ != nullptr) { - const ClauseId clause_id = GetClauseId(it->clause); - const int size = it->clause->size(); - std::vector& unit_ids = clause_ids_scratchpad_; - unit_ids.clear(); - for (int i = 1; i < size; ++i) { - unit_ids.push_back(trail_->GetUnitClauseId(literals[i].Variable())); + if (propagation_level == 0) { + if (lrat_proof_handler_ != nullptr) { + std::vector& unit_ids = clause_ids_scratchpad_; + unit_ids.clear(); + const int size = it->clause->size(); + for (int i = 1; i < size; ++i) { + unit_ids.push_back( + trail_->GetUnitClauseId(literals[i].Variable())); + } + unit_ids.push_back(GetClauseId(it->clause)); + const ClauseId new_clause_id = clause_id_generator_->GetNextId(); + lrat_proof_handler_->AddInferredClause( + new_clause_id, {other_watched_literal}, unit_ids); + helper.EnqueueWithUnitReason(other_watched_literal, new_clause_id); + } else { + trail_->EnqueueWithUnitReason(other_watched_literal); } - unit_ids.push_back(clause_id); - const ClauseId new_clause_id = clause_id_generator_->GetNextId(); - lrat_proof_handler_->AddInferredClause( - new_clause_id, {other_watched_literal}, unit_ids); - helper.EnqueueWithUnitReason(other_watched_literal, new_clause_id); } else { + reasons_[trail->Index()] = it->clause; helper.EnqueueAtLevel(other_watched_literal, propagation_level); } *new_it++ = *it; @@ -296,6 +300,7 @@ SatClause* ClauseManager::ReasonClauseOrNull(BooleanVariable var) const { if (!trail_->Assignment().VariableIsAssigned(var)) return nullptr; if (trail_->AssignmentType(var) != propagator_id_) return nullptr; SatClause* result = reasons_[trail_->Info(var).trail_index]; + DCHECK(result != nullptr) << trail_->Info(var).DebugString(); // Tricky: In some corner case, that clause was subsumed, so we don't want // to check it nor use it. @@ -306,6 +311,7 @@ SatClause* ClauseManager::ReasonClauseOrNull(BooleanVariable var) const { bool ClauseManager::ClauseIsUsedAsReason(SatClause* clause) const { DCHECK(clause != nullptr); + if (clause->empty()) return false; return clause == ReasonClauseOrNull(clause->PropagatedLiteral().Variable()); } @@ -642,6 +648,16 @@ void ClauseManager::CleanUpWatchers() { void ClauseManager::DeleteRemovedClauses() { if (!is_clean_) CleanUpWatchers(); + if (DEBUG_MODE) { + // This help debug issues, as it is easier to check for nullptr rather than + // detect a pointer that has been deleted. + for (int i = 0; i < reasons_.size(); ++i) { + if (reasons_[i] != nullptr && reasons_[i]->empty()) { + reasons_[i] = nullptr; + } + } + } + int new_size = 0; const int old_size = clauses_.size(); for (int i = 0; i < old_size; ++i) { @@ -649,6 +665,7 @@ void ClauseManager::DeleteRemovedClauses() { if (i == to_first_minimize_index_) to_first_minimize_index_ = new_size; if (i == to_probe_index_) to_probe_index_ = new_size; if (clauses_[i]->IsRemoved()) { + DCHECK(!clauses_info_.contains(clauses_[i])); delete clauses_[i]; } else { clauses_[new_size++] = clauses_[i]; diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h index 5aab10b4a4..6bdff62f20 100644 --- a/ortools/sat/clause.h +++ b/ortools/sat/clause.h @@ -313,6 +313,7 @@ class ClauseManager : public SatPropagator { // start so the clauses will be returned in round-robin order. // Note that we only minimize clauses kept forever. SatClause* NextClauseToMinimize(); + // Returns the next clause to probe in round-robin order. SatClause* NextClauseToProbe(); diff --git a/ortools/sat/linear_constraint.cc b/ortools/sat/linear_constraint.cc index c6b099b3f2..744bea31ee 100644 --- a/ortools/sat/linear_constraint.cc +++ b/ortools/sat/linear_constraint.cc @@ -296,17 +296,6 @@ void DivideByGCD(LinearConstraint* constraint) { } } -void MakeAllCoefficientsPositive(LinearConstraint* constraint) { - const int size = constraint->num_terms; - for (int i = 0; i < size; ++i) { - const IntegerValue coeff = constraint->coeffs[i]; - if (coeff < 0) { - constraint->coeffs[i] = -coeff; - constraint->vars[i] = NegationOf(constraint->vars[i]); - } - } -} - void MakeAllVariablesPositive(LinearConstraint* constraint) { const int size = constraint->num_terms; for (int i = 0; i < size; ++i) { diff --git a/ortools/sat/linear_constraint.h b/ortools/sat/linear_constraint.h index 72a0441c83..a512340313 100644 --- a/ortools/sat/linear_constraint.h +++ b/ortools/sat/linear_constraint.h @@ -350,9 +350,6 @@ double ScalarProduct(const LinearConstraint& constraint1, // also tighten the constraint bounds assuming all the variables are integer. void DivideByGCD(LinearConstraint* constraint); -// Makes all coefficients positive by transforming a variable to its negation. -void MakeAllCoefficientsPositive(LinearConstraint* constraint); - // Makes all variables "positive" by transforming a variable to its negation. void MakeAllVariablesPositive(LinearConstraint* constraint); diff --git a/ortools/sat/linear_constraint_test.cc b/ortools/sat/linear_constraint_test.cc index 2a541e285e..7164bd84eb 100644 --- a/ortools/sat/linear_constraint_test.cc +++ b/ortools/sat/linear_constraint_test.cc @@ -181,14 +181,6 @@ TEST(LinearConstraintCopyTest, BasicBehavior) { EXPECT_EQ(ct, other); } -TEST(MakeAllCoefficientsPositiveTest, BasicBehavior) { - // Note that this relies on the fact that the negation of an IntegerVariable - // var is is the one with IntegerVariable(var.value() ^ 1); - LinearConstraint ct = CreateUbConstraintForTest({-2, 0, -7, 0}, 10); - MakeAllCoefficientsPositive(&ct); - EXPECT_EQ(ct, CreateUbConstraintForTest({0, 2, 0, 7}, 10)); -} - TEST(LinearConstraintBuilderTest, DuplicateCoefficient) { Model model; model.GetOrCreate(); diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index 6fa3794c9c..9b0bb04adb 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/ortools/sat/linear_programming_constraint.cc @@ -218,8 +218,8 @@ LinearConstraint ScatteredIntegerVector::ConvertToLinearConstraint( result.ub = upper_bound; if (extra_term != std::nullopt) { - result.vars[new_size] += extra_term->first; - result.coeffs[new_size] += extra_term->second; + result.vars[new_size] = extra_term->first; + result.coeffs[new_size] = extra_term->second; ++new_size; } diff --git a/ortools/sat/sat_inprocessing.cc b/ortools/sat/sat_inprocessing.cc index 1baddcf50c..04927991ea 100644 --- a/ortools/sat/sat_inprocessing.cc +++ b/ortools/sat/sat_inprocessing.cc @@ -1487,10 +1487,9 @@ bool BoundedVariableElimination::DoOneRound(bool log_info) { DCHECK( std::all_of(marked_.begin(), marked_.end(), [](bool b) { return !b; })); - // TODO(user): add a local dtime limit for the corner case where this take too - // much time. We can adapt the limit depending on how much we want to spend on + // TODO(user): adapt the dtime limit depending on how much we want to spend on // inprocessing. - while (!time_limit_->LimitReached() && !queue_.IsEmpty()) { + while (!time_limit_->LimitReached() && !queue_.IsEmpty() && dtime_ < 10.0) { const BooleanVariable top = queue_.Top().var; queue_.Pop(); @@ -1538,7 +1537,6 @@ bool BoundedVariableElimination::DoOneRound(bool log_info) { literal_to_clauses_.clear(); literal_to_num_clauses_.clear(); - dtime_ += 1e-8 * num_inspected_literals_; time_limit_->AdvanceDeterministicTime(dtime_); log_info |= VLOG_IS_ON(2); LOG_IF(INFO, log_info) << "BVE." @@ -1885,10 +1883,12 @@ bool BoundedVariableElimination::CrossProduct(BooleanVariable var) { for (const ClauseIndex i : literal_to_clauses_[lit]) { const auto c = clauses_[i]->AsSpan(); if (!c.empty()) score += clause_weight + c.size(); + dtime_ += 1e-8 * c.size(); } for (const ClauseIndex i : literal_to_clauses_[not_lit]) { const auto c = clauses_[i]->AsSpan(); if (!c.empty()) score += clause_weight + c.size(); + dtime_ += 1.0e-8 * c.size(); } // Compute the new score after BVE. diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index cc6a95ad65..81a60aaf97 100644 --- a/ortools/sat/sat_solver.cc +++ b/ortools/sat/sat_solver.cc @@ -3030,6 +3030,7 @@ void SatSolver::CleanClauseDatabaseIfNeeded() { std::vector entries; auto& clauses_info = *(clauses_propagator_->mutable_clauses_info()); for (auto& entry : clauses_info) { + DCHECK(!entry.first->empty()); // Should have been deleted ! entry.second.num_cleanup_rounds_since_last_bumped++; if (clauses_propagator_->ClauseIsUsedAsReason(entry.first)) continue;