diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index 618e50fe20..9f94d13262 100644 --- a/ortools/sat/clause.cc +++ b/ortools/sat/clause.cc @@ -931,7 +931,11 @@ void BinaryImplicationGraph::MinimizeConflictFirst( is_marked_.ClearAndResize(LiteralIndex(implications_.size())); MarkDescendants(conflict->front().Negated()); for (const LiteralIndex i : is_marked_.PositionsSetAtLeastOnce()) { - if (trail.Assignment().LiteralIsFalse(Literal(i))) { + // TODO(user): if this is false, then we actually have a conflict of size 2. + // This can only happen if the binary clause was not propagated properly + // if for instance we do chronological bactracking without re-enqueing the + // consequence of a binary clause. + if (trail.Assignment().LiteralIsTrue(Literal(i))) { marked->Set(Literal(i).Variable()); } } diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index ef62473b46..c5443456cf 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -698,8 +698,18 @@ void InitializeDebugSolution(const CpModelProto& model_proto, Model* model) { debug_sol.ivar_has_value.assign(num_integers, false); debug_sol.ivar_values.assign(num_integers, 0); + std::vector boolean_solution; + const auto& mapping = *model->GetOrCreate(); for (int i = 0; i < debug_sol.proto_values.size(); ++i) { + if (mapping.IsBoolean(i)) { + Literal l = mapping.Literal(i); + if (debug_sol.proto_values[i] == 0) { + l = l.Negated(); + } + boolean_solution.push_back(l); + } + if (!mapping.IsInteger(i)) continue; const IntegerVariable var = mapping.Integer(i); debug_sol.ivar_has_value[var] = true; @@ -708,6 +718,15 @@ void InitializeDebugSolution(const CpModelProto& model_proto, Model* model) { debug_sol.ivar_values[NegationOf(var)] = -debug_sol.proto_values[i]; } + // If the solution is fully boolean (there is no integer variable), and + // we have a decision problem (so no new boolean should be created), we load + // it in the sat solver for debugging too. + if (boolean_solution.size() == debug_sol.proto_values.size() && + !model_proto.has_objective()) { + LOG(INFO) << "Loaded pure Boolean debugging solution."; + model->GetOrCreate()->LoadDebugSolution(boolean_solution); + } + // The objective variable is usually not part of the proto, but it is still // nice to have it, so we recompute it here. auto* objective_def = model->Get(); diff --git a/ortools/sat/diffn_util.cc b/ortools/sat/diffn_util.cc index 2ee7c8b92f..52f0ddc586 100644 --- a/ortools/sat/diffn_util.cc +++ b/ortools/sat/diffn_util.cc @@ -19,6 +19,7 @@ #include #include #include +#include #include #include #include @@ -1460,6 +1461,7 @@ std::vector FindRectanglesWithEnergyConflictMC( const double inv_temp = 1.0 / temperature; absl::InlinedVector candidates; + absl::InlinedVector energy_deltas; absl::InlinedVector weights; while (!ranges.IsMinimal()) { const IntegerValue rect_area = ranges.GetCurrentRectangleArea(); @@ -1471,7 +1473,7 @@ std::vector FindRectanglesWithEnergyConflictMC( break; } candidates.clear(); - weights.clear(); + energy_deltas.clear(); for (int border_idx = 0; border_idx < 4; ++border_idx) { const ProbingRectangle::Edge border = @@ -1482,9 +1484,18 @@ std::vector FindRectanglesWithEnergyConflictMC( candidates.push_back(border); const IntegerValue delta_area = ranges.GetShrinkDeltaArea(border); const IntegerValue delta_energy = ranges.GetShrinkDeltaEnergy(border); - const IntegerValue delta_slack = delta_energy - delta_area; - const int table_lookup = std::max( - 0, std::min((int)(delta_slack.value() * 5 * inv_temp + 50), 100)); + energy_deltas.push_back(delta_energy - delta_area); + } + const IntegerValue min_energy_delta = + *std::min_element(energy_deltas.begin(), energy_deltas.end()); + weights.clear(); + for (const IntegerValue delta_slack : energy_deltas) { + const int64_t table_lookup = + std::max((int64_t)0, + std::min((int64_t)((delta_slack - min_energy_delta).value() * + 5 * inv_temp + + 50), + (int64_t)100)); weights.push_back((*cached_probabilities)[table_lookup]); } // Pick a change with a probability proportional to exp(- delta_E / Temp) diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index 2504b32e04..f0ecc0fec2 100644 --- a/ortools/sat/sat_solver.cc +++ b/ortools/sat/sat_solver.cc @@ -493,6 +493,22 @@ void SatSolver::SaveDebugAssignment() { } } +void SatSolver::LoadDebugSolution(const std::vector& solution) { + debug_assignment_.Resize(num_variables_.value()); + for (BooleanVariable var(0); var < num_variables_; ++var) { + if (!debug_assignment_.VariableIsAssigned(var)) continue; + debug_assignment_.UnassignLiteral(Literal(var, true)); + } + for (const Literal l : solution) { + debug_assignment_.AssignFromTrueLiteral(l); + } + + // We should only call this with complete solution. + for (BooleanVariable var(0); var < num_variables_; ++var) { + CHECK(debug_assignment_.VariableIsAssigned(var)); + } +} + void SatSolver::AddBinaryClauseInternal(Literal a, Literal b) { if (track_binary_clauses_) { // Abort if this clause was already added. @@ -506,7 +522,8 @@ void SatSolver::AddBinaryClauseInternal(Literal a, Literal b) { } bool SatSolver::ClauseIsValidUnderDebugAssignment( - const std::vector& clause) const { + absl::Span clause) const { + if (debug_assignment_.NumberOfVariables() == 0) return true; for (Literal l : clause) { if (l.Variable() >= debug_assignment_.NumberOfVariables() || debug_assignment_.LiteralIsTrue(l)) { @@ -911,6 +928,16 @@ void SatSolver::ProcessCurrentConflict() { drat_proof_handler_->AddClause(learned_conflict_); } + // Because we might change the conflict with this minimization algorithm, we + // cannot just subsume clauses with it blindly. + // + // TODO(user): Either remove that algorithm or support subsumption by just + // checking if it is okay to do so, or doing it on the fly while computing the + // first UIP. + if (parameters_->minimization_algorithm() == SatParameters::EXPERIMENTAL) { + subsumed_clauses_.clear(); + } + // Detach any subsumed clause. They will actually be deleted on the next // clause cleanup phase. bool is_redundant = true; diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h index c478a8780d..923edee5a1 100644 --- a/ortools/sat/sat_solver.h +++ b/ortools/sat/sat_solver.h @@ -444,6 +444,7 @@ class SatSolver { // debug mode, and after this is called, all the learned clauses are tested to // satisfy this saved assignment. void SaveDebugAssignment(); + void LoadDebugSolution(const std::vector& solution); // Returns true iff the loaded problem only contains clauses. bool ProblemIsPureSat() const { return problem_is_pure_sat_; } @@ -518,7 +519,7 @@ class SatSolver { // variables at the time the debug_assignment_ was saved. If new variables // were added since that time, they will be considered unassigned. bool ClauseIsValidUnderDebugAssignment( - const std::vector& clause) const; + absl::Span clause) const; bool PBConstraintIsValidUnderDebugAssignment( const std::vector& cst, Coefficient rhs) const; diff --git a/ortools/sat/scheduling_cuts.cc b/ortools/sat/scheduling_cuts.cc index 91ad890e69..bc0d7982d7 100644 --- a/ortools/sat/scheduling_cuts.cc +++ b/ortools/sat/scheduling_cuts.cc @@ -82,9 +82,6 @@ struct EnergyEvent : BaseEvent { // True if linearized_energy is not exact and a McCormick relaxation. bool energy_is_quadratic = false; - // Used to minimize the increase on the y axis for rectangles. - double y_spread = 0.0; - // The actual value of the presence literal of the interval(s) is checked // when the event is created. A value of kNoLiteralIndex indicates that either // the interval was not optional, or that its presence literal is true at diff --git a/ortools/sat/work_assignment.cc b/ortools/sat/work_assignment.cc index f7f28dee14..2611b8eff1 100644 --- a/ortools/sat/work_assignment.cc +++ b/ortools/sat/work_assignment.cc @@ -259,6 +259,10 @@ void SharedTreeManager::ProposeSplit(ProtoTrail& path, ProtoLiteral decision) { absl::MutexLock mutex_lock(&mu_); if (!IsValid(path)) return; std::vector> nodes = GetAssignedNodes(path); + if (nodes.back().first->closed) { + VLOG(2) << "Cannot split closed node"; + return; + } if (nodes.back().first->children[0] != nullptr) { LOG_IF(WARNING, nodes.size() > 1) << "Cannot resplit previously split node @ " << nodes.back().second @@ -266,11 +270,11 @@ void SharedTreeManager::ProposeSplit(ProtoTrail& path, ProtoLiteral decision) { return; } if (nodes_.size() >= max_nodes_) { - VLOG(1) << "Too many nodes to accept split"; + VLOG(2) << "Too many nodes to accept split"; return; } if (num_splits_wanted_ <= 0) { - VLOG(1) << "Enough splits for now"; + VLOG(2) << "Enough splits for now"; return; } if (params_.shared_tree_split_strategy() == @@ -289,13 +293,13 @@ void SharedTreeManager::ProposeSplit(ProtoTrail& path, ProtoLiteral decision) { // This rule will allow twice as many leaves in the preferred subtree. if (discrepancy + path.MaxLevel() > MaxAllowedDiscrepancyPlusDepth(num_workers_)) { - VLOG(1) << "Too high discrepancy to accept split"; + VLOG(2) << "Too high discrepancy to accept split"; return; } } else if (params_.shared_tree_split_strategy() == SatParameters::SPLIT_STRATEGY_OBJECTIVE_LB) { if (nodes.back().first->objective_lb > nodes.front().first->objective_lb) { - VLOG(1) << "Can only split nodes with minimum objective lb, " + VLOG(2) << "Can only split nodes with minimum objective lb, " << nodes.back().first->objective_lb << " > " << nodes.front().first->objective_lb; return; @@ -303,11 +307,11 @@ void SharedTreeManager::ProposeSplit(ProtoTrail& path, ProtoLiteral decision) { } else if (params_.shared_tree_split_strategy() == SatParameters::SPLIT_STRATEGY_BALANCED_TREE) { if (path.MaxLevel() + 1 > log2(num_workers_)) { - VLOG(1) << "Tree too unbalanced to accept split"; + VLOG(2) << "Tree too unbalanced to accept split"; return; } } - VLOG_EVERY_N(1, 10) << unassigned_leaves_.size() << " unassigned leaves, " + VLOG_EVERY_N(2, 10) << unassigned_leaves_.size() << " unassigned leaves, " << nodes_.size() << " subtrees, " << num_splits_wanted_ << " splits wanted"; Split(nodes, decision); @@ -320,7 +324,7 @@ void SharedTreeManager::ReplaceTree(ProtoTrail& path) { std::vector> nodes = GetAssignedNodes(path); if (nodes.back().first->children[0] == nullptr && !nodes.back().first->closed && nodes.size() > 1) { - VLOG(1) << "Returning leaf to be replaced"; + VLOG(2) << "Returning leaf to be replaced"; unassigned_leaves_.push_back(nodes.back().first); } path.Clear(); @@ -334,7 +338,7 @@ void SharedTreeManager::ReplaceTree(ProtoTrail& path) { return; } } - VLOG(1) << "Assigning root because no unassigned leaves are available"; + VLOG(2) << "Assigning root because no unassigned leaves are available"; // TODO(user): Investigate assigning a random leaf so workers can still // improve shared tree bounds. } @@ -448,7 +452,7 @@ void SharedTreeManager::CloseTree(ProtoTrail& path, int level) { path.Clear(); if (node_id_to_close < node_id_offset_) return; Node* node = &nodes_[node_id_to_close - node_id_offset_]; - VLOG(1) << "Closing subtree at level " << level; + VLOG(2) << "Closing subtree at level " << level; DCHECK(to_close_.empty()); to_close_.push_back(node); ProcessNodeChanges(); @@ -522,7 +526,7 @@ bool SharedTreeWorker::AddDecisionImplication(Literal lit, int level) { CHECK_NE(lit.Index(), kNoLiteralIndex); CHECK(!sat_solver_->Assignment().LiteralIsTrue(lit)); if (sat_solver_->Assignment().LiteralIsFalse(lit)) { - VLOG(1) << "Closing subtree via impl at " << level + 1 + VLOG(2) << "Closing subtree via impl at " << level + 1 << " assigned=" << assigned_tree_.MaxLevel(); integer_trail_->ReportConflict(DecisionReason(level), {}); manager_->CloseTree(assigned_tree_, level); @@ -530,7 +534,7 @@ bool SharedTreeWorker::AddDecisionImplication(Literal lit, int level) { return false; } integer_trail_->EnqueueLiteral(lit, DecisionReason(level), {}); - VLOG(1) << "Learned shared clause"; + VLOG(2) << "Learned shared clause"; return true; } @@ -583,7 +587,7 @@ bool SharedTreeWorker::SyncWithLocalTrail() { if (!sat_solver_->Assignment().LiteralIsAssigned(next_decision)) break; if (sat_solver_->Assignment().LiteralIsFalse(next_decision)) { // Next assigned decision is impossible. - VLOG(1) << "Closing subtree at " << level + 1 + VLOG(2) << "Closing subtree at " << level + 1 << " assigned=" << assigned_tree_.MaxLevel(); manager_->CloseTree(assigned_tree_, level + 1); assigned_tree_literals_.clear(); @@ -602,7 +606,7 @@ bool SharedTreeWorker::NextDecision(LiteralIndex* decision_index) { const int next_level = sat_solver_->CurrentDecisionLevel() + 1; CHECK_EQ(assigned_tree_literals_.size(), assigned_tree_.MaxLevel()); if (next_level <= assigned_tree_.MaxLevel()) { - VLOG(1) << "Following shared trail depth=" << next_level << " " + VLOG(2) << "Following shared trail depth=" << next_level << " " << parameters_->name(); const Literal decision = assigned_tree_literals_[next_level - 1]; CHECK(!sat_solver_->Assignment().LiteralIsFalse(decision)) @@ -665,7 +669,7 @@ void SharedTreeWorker::MaybeProposeSplit() { void SharedTreeWorker::SyncWithSharedTree() { splits_wanted_ = manager_->SplitsToGeneratePerWorker(); - VLOG(1) << "Splits wanted: " << splits_wanted_ << " " << parameters_->name(); + VLOG(2) << "Splits wanted: " << splits_wanted_ << " " << parameters_->name(); manager_->SyncTree(assigned_tree_); // If we have no assignment, try to get one. // We also want to ensure unassigned nodes have their lower bounds bumped @@ -679,7 +683,7 @@ void SharedTreeWorker::SyncWithSharedTree() { manager_->ReplaceTree(assigned_tree_); tree_assignment_restart_ = num_restarts_; } - VLOG(1) << "Assigned level: " << assigned_tree_.MaxLevel() << " " + VLOG(2) << "Assigned level: " << assigned_tree_.MaxLevel() << " " << parameters_->name(); assigned_tree_literals_.clear(); for (int i = 1; i <= assigned_tree_.MaxLevel(); ++i) {