diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index 284587dcaa..837aaa9223 100644 --- a/ortools/sat/clause.cc +++ b/ortools/sat/clause.cc @@ -508,7 +508,11 @@ void BinaryImplicationGraph::AddBinaryClause(Literal a, Literal b) { bool BinaryImplicationGraph::AddBinaryClauseDuringSearch(Literal a, Literal b) { SCOPED_TIME_STAT(&stats_); - if (num_implications_ == 0) propagation_trail_index_ = trail_->Index(); + + // Tricky: If this is the first clause, the propagator will be added and + // assumed to be in a "propagated" state. This makes sure this is the case. + if (IsEmpty()) propagation_trail_index_ = trail_->Index(); + AddBinaryClause(a, b); const auto& assignment = trail_->Assignment(); diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h index 84be229cf1..1e29605781 100644 --- a/ortools/sat/clause.h +++ b/ortools/sat/clause.h @@ -51,10 +51,10 @@ namespace sat { // indirection. class SatClause { public: - // Creates a sat clause. There must be at least 2 literals. Smaller clause are - // treated separatly and never constructed. In practice, we do use - // BinaryImplicationGraph for the clause of size 2, so this is mainly used for - // size at least 3. + // Creates a sat clause. There must be at least 2 literals. + // Clause with one literal fix variable directly and are never constructed. + // Note that in practice, we use BinaryImplicationGraph for the clause of size + // 2, so this is used for size at least 3. static SatClause* Create(absl::Span literals); // Non-sized delete because this is a tail-padded class. @@ -357,9 +357,7 @@ class LiteralWatchers : public SatPropagator { // pointers. We currently do not use std::unique_ptr because it // can't be used with some STL algorithms like std::partition. // - // Note that the unit clauses are not kept here and if the parameter - // treat_binary_clauses_separately is true, the binary clause are not kept - // here either. + // Note that the unit clauses and binary clause are not kept here. std::vector clauses_; int to_minimize_index_ = 0; diff --git a/ortools/sat/cp_model_lns.cc b/ortools/sat/cp_model_lns.cc index bc1ab28d5e..5c8581c9d5 100644 --- a/ortools/sat/cp_model_lns.cc +++ b/ortools/sat/cp_model_lns.cc @@ -312,6 +312,7 @@ void NeighborhoodGeneratorHelper::RecomputeHelperData() { } } shared_response_->LogMessage( + "Model", absl::StrCat("var:", active_variables_.size(), "/", num_variables, " constraints:", simplied_model_proto_.constraints().size(), "/", model_proto_.constraints().size(), compo_message)); diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 5108870619..4fbee7c524 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -2048,6 +2048,10 @@ class FullProblemSolver : public SubSolver { shared->incomplete_solutions); } + if (shared->bounds != nullptr) { + local_model_->Register(shared->bounds); + } + if (shared->clauses != nullptr) { local_model_->Register(shared->clauses); } diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index 93792ddd3d..5b0590273e 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -19,6 +19,7 @@ #include #include "absl/container/flat_hash_set.h" +#include "absl/time/time.h" #include "absl/types/span.h" #include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/implied_bounds.h" @@ -1094,14 +1095,29 @@ SatSolver::Status ContinuousProbing( const SatParameters& sat_parameters = *(model->GetOrCreate()); auto* level_zero_callbacks = model->GetOrCreate(); Prober* prober = model->GetOrCreate(); + auto* shared_response_manager = model->Mutable(); + auto* shared_bounds_manager = model->Mutable(); std::vector active_vars; std::vector integer_bounds; absl::flat_hash_set integer_bounds_set; - int loop = 0; + int iteration = 1; + absl::Time last_check = absl::Now(); + while (!time_limit->LimitReached()) { - VLOG(2) << "Probing loop " << loop++; + if (shared_response_manager != nullptr && + shared_bounds_manager != nullptr && + absl::Now() - last_check >= absl::Seconds(10)) { + shared_response_manager->LogMessage( + "Probe", + absl::StrCat("#iterations:", iteration, + " #literals_fixed:", prober->num_new_literals_fixed(), + " #new_integer_bounds:", + shared_bounds_manager->NumBoundsExported("probing"))); + last_check = absl::Now(); + } + iteration++; // Sync the bounds first. auto SyncBounds = [solver, &level_zero_callbacks]() { diff --git a/ortools/sat/integer_search.h b/ortools/sat/integer_search.h index 384807cc63..f8ef487094 100644 --- a/ortools/sat/integer_search.h +++ b/ortools/sat/integer_search.h @@ -30,6 +30,7 @@ #include "ortools/sat/pseudo_costs.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_solver.h" +#include "ortools/sat/synchronization.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/probing.cc b/ortools/sat/probing.cc index e46f04bdde..523ae0ce55 100644 --- a/ortools/sat/probing.cc +++ b/ortools/sat/probing.cc @@ -13,6 +13,7 @@ #include "ortools/sat/probing.h" +#include #include #include @@ -179,11 +180,6 @@ bool Prober::ProbeOneVariableInternal(BooleanVariable b) { } bool Prober::ProbeOneVariable(BooleanVariable b) { - // Reset statistics. - num_new_binary_ = 0; - num_new_holes_ = 0; - num_new_integer_bounds_ = 0; - // Resize the propagated sparse bitset. const int num_variables = sat_solver_->NumVariables(); propagated_.ClearAndResize(LiteralIndex(2 * num_variables)); @@ -192,7 +188,13 @@ bool Prober::ProbeOneVariable(BooleanVariable b) { sat_solver_->SetAssumptionLevel(0); if (!sat_solver_->RestoreSolverToAssumptionLevel()) return false; - return ProbeOneVariableInternal(b); + const int initial_num_fixed = sat_solver_->LiteralTrail().Index(); + if (!ProbeOneVariableInternal(b)) return false; + + // Statistics + const int num_fixed = sat_solver_->LiteralTrail().Index(); + num_new_literals_fixed_ += num_fixed - initial_num_fixed; + return true; } bool Prober::ProbeBooleanVariables( @@ -205,6 +207,7 @@ bool Prober::ProbeBooleanVariables( num_new_binary_ = 0; num_new_holes_ = 0; num_new_integer_bounds_ = 0; + num_new_literals_fixed_ = 0; // Resize the propagated sparse bitset. const int num_variables = sat_solver_->NumVariables(); @@ -243,19 +246,22 @@ bool Prober::ProbeBooleanVariables( } } + // Update stats. + const int num_fixed = sat_solver_->LiteralTrail().Index(); + num_new_literals_fixed_ = num_fixed - initial_num_fixed; + // Display stats. if (logger_->LoggingIsEnabled()) { const double time_diff = time_limit_->GetElapsedDeterministicTime() - initial_deterministic_time; - const int num_fixed = sat_solver_->LiteralTrail().Index(); - const int num_newly_fixed = num_fixed - initial_num_fixed; SOLVER_LOG(logger_, "[Probing] deterministic_time: ", time_diff, " (limit: ", deterministic_time_limit, ") wall_time: ", wall_timer.Get(), " (", (limit_reached ? "Aborted " : ""), num_probed, "/", bool_vars.size(), ")"); - if (num_newly_fixed > 0) { - SOLVER_LOG(logger_, "[Probing] - new fixed Boolean: ", num_newly_fixed, + if (num_new_literals_fixed_ > 0) { + SOLVER_LOG(logger_, + "[Probing] - new fixed Boolean: ", num_new_literals_fixed_, " (", num_fixed, "/", sat_solver_->NumVariables(), ")"); } if (num_new_holes_ > 0) { diff --git a/ortools/sat/probing.h b/ortools/sat/probing.h index 98ced49c9e..0e36cd5a2b 100644 --- a/ortools/sat/probing.h +++ b/ortools/sat/probing.h @@ -72,6 +72,11 @@ class Prober { bool ProbeOneVariable(BooleanVariable b); + // Statistics. + // They are reset each time ProbleBooleanVariables() is called. + // Note however that we do not reset them on a call to ProbeOneVariable(). + int num_new_literals_fixed() const { return num_new_literals_fixed_; } + private: bool ProbeOneVariableInternal(BooleanVariable b); @@ -98,6 +103,7 @@ class Prober { int num_new_holes_ = 0; int num_new_binary_ = 0; int num_new_integer_bounds_ = 0; + int num_new_literals_fixed_ = 0; // Logger. SolverLogger* logger_; diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index a72ce6a7d3..e80f558013 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -129,7 +129,6 @@ message SatParameters { [default = RECURSIVE]; // Whether to expoit the binary clause to minimize learned clauses further. - // This will have an effect only if treat_binary_clauses_separately is true. enum BinaryMinizationAlgorithm { NO_BINARY_MINIMIZATION = 0; BINARY_MINIMIZATION_FIRST = 1; @@ -360,11 +359,6 @@ message SatParameters { // Other parameters // ========================================================================== - // If true, the binary clauses are treated separately from the others. This - // should be faster and uses less memory. However it changes the propagation - // order. - optional bool treat_binary_clauses_separately = 33 [default = true]; - // At the beginning of each solve, the random number generator used in some // part of the solver is reinitialized to this seed. If you change the random // seed, the solver may make different choices during the solving process. diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index 6bcffe12f1..b9df049f86 100644 --- a/ortools/sat/sat_solver.cc +++ b/ortools/sat/sat_solver.cc @@ -138,16 +138,11 @@ bool SatSolver::AddClauseDuringSearch(absl::Span literals) { if (literals.empty()) return SetModelUnsat(); if (literals.size() == 1) return AddUnitClause(literals[0]); if (literals.size() == 2) { - const bool init = binary_implication_graph_->num_implications() == 0; if (!binary_implication_graph_->AddBinaryClauseDuringSearch(literals[0], literals[1])) { CHECK_EQ(CurrentDecisionLevel(), 0); return SetModelUnsat(); } - if (init) { - // This is needed because we just added the first binary clause. - InitializePropagators(); - } } else { if (!clauses_propagator_->AddClause(literals)) { CHECK_EQ(CurrentDecisionLevel(), 0); @@ -163,82 +158,68 @@ bool SatSolver::AddClauseDuringSearch(absl::Span literals) { } bool SatSolver::AddUnitClause(Literal true_literal) { - SCOPED_TIME_STAT(&stats_); - CHECK_EQ(CurrentDecisionLevel(), 0); - if (model_is_unsat_) return false; - if (trail_->Assignment().LiteralIsFalse(true_literal)) return SetModelUnsat(); - if (trail_->Assignment().LiteralIsTrue(true_literal)) return true; - if (drat_proof_handler_ != nullptr) { - // Note that we will output problem unit clauses twice, but that is a small - // price to pay for having a single variable fixing API. - drat_proof_handler_->AddClause({true_literal}); - } - trail_->EnqueueWithUnitReason(true_literal); - if (!Propagate()) return SetModelUnsat(); - return true; + return AddProblemClause({true_literal}); } bool SatSolver::AddBinaryClause(Literal a, Literal b) { - SCOPED_TIME_STAT(&stats_); - tmp_pb_constraint_.clear(); - tmp_pb_constraint_.push_back(LiteralWithCoeff(a, 1)); - tmp_pb_constraint_.push_back(LiteralWithCoeff(b, 1)); - return AddLinearConstraint( - /*use_lower_bound=*/true, /*lower_bound=*/Coefficient(1), - /*use_upper_bound=*/false, /*upper_bound=*/Coefficient(0), - &tmp_pb_constraint_); + return AddProblemClause({a, b}); } bool SatSolver::AddTernaryClause(Literal a, Literal b, Literal c) { - SCOPED_TIME_STAT(&stats_); - tmp_pb_constraint_.clear(); - tmp_pb_constraint_.push_back(LiteralWithCoeff(a, 1)); - tmp_pb_constraint_.push_back(LiteralWithCoeff(b, 1)); - tmp_pb_constraint_.push_back(LiteralWithCoeff(c, 1)); - return AddLinearConstraint( - /*use_lower_bound=*/true, /*lower_bound=*/Coefficient(1), - /*use_upper_bound=*/false, /*upper_bound=*/Coefficient(0), - &tmp_pb_constraint_); + return AddProblemClause({a, b, c}); } bool SatSolver::AddProblemClause(absl::Span literals) { SCOPED_TIME_STAT(&stats_); + CHECK_EQ(CurrentDecisionLevel(), 0); + if (model_is_unsat_) return false; - // TODO(user): To avoid duplication, we currently just call - // AddLinearConstraint(). Make a faster specific version if that becomes a - // performance issue. - tmp_pb_constraint_.clear(); - for (Literal lit : literals) { - tmp_pb_constraint_.push_back(LiteralWithCoeff(lit, 1)); + // Filter already assigned literals. + literals_scratchpad_.clear(); + for (const Literal l : literals) { + if (trail_->Assignment().LiteralIsTrue(l)) return true; + if (trail_->Assignment().LiteralIsFalse(l)) continue; + literals_scratchpad_.push_back(l); } - return AddLinearConstraint( - /*use_lower_bound=*/true, /*lower_bound=*/Coefficient(1), - /*use_upper_bound=*/false, /*upper_bound=*/Coefficient(0), - &tmp_pb_constraint_); + + AddProblemClauseInternal(literals_scratchpad_); + + // Tricky: The PropagationIsDone() condition shouldn't change anything for a + // pure SAT problem, however in the CP-SAT context, calling Propagate() can + // tigger computation (like the LP) even if no domain changed since the last + // call. We do not want to do that. + if (!PropagationIsDone() && !Propagate()) { + return SetModelUnsat(); + } + return true; } bool SatSolver::AddProblemClauseInternal(absl::Span literals) { SCOPED_TIME_STAT(&stats_); - CHECK_EQ(CurrentDecisionLevel(), 0); - - // Deals with clause of size 0 (always false) and 1 (set a literal) right away - // so we guarantee that a SatClause is always of size greater than one. This - // simplifies the code. - CHECK_GT(literals.size(), 0); - if (literals.size() == 1) { - if (trail_->Assignment().LiteralIsFalse(literals[0])) return false; - if (trail_->Assignment().LiteralIsTrue(literals[0])) return true; - trail_->EnqueueWithUnitReason(literals[0]); // Not assigned. - return true; + if (DEBUG_MODE) { + CHECK_EQ(CurrentDecisionLevel(), 0); + for (const Literal l : literals) { + CHECK(!trail_->Assignment().LiteralIsAssigned(l)); + } } - if (parameters_->treat_binary_clauses_separately() && literals.size() == 2) { + if (literals.empty()) return SetModelUnsat(); + + if (literals.size() == 1) { + if (drat_proof_handler_ != nullptr) { + // Note that we will output problem unit clauses twice, but that is a + // small price to pay for having a single variable fixing API. + drat_proof_handler_->AddClause({literals[0]}); + } + trail_->EnqueueWithUnitReason(literals[0]); + } else if (literals.size() == 2) { AddBinaryClauseInternal(literals[0], literals[1]); } else { if (!clauses_propagator_->AddClause(literals, trail_)) { return SetModelUnsat(); } } + return true; } @@ -271,8 +252,7 @@ bool SatSolver::AddLinearConstraintInternal( // Detect at most one constraints. Note that this use the fact that the // coefficient are sorted. - if (parameters_->treat_binary_clauses_separately() && - !parameters_->use_pb_resolution() && max_coeff <= rhs && + if (!parameters_->use_pb_resolution() && max_coeff <= rhs && 2 * min_coeff > rhs) { literals_scratchpad_.clear(); for (const LiteralWithCoeff& term : cst) { @@ -281,10 +261,6 @@ bool SatSolver::AddLinearConstraintInternal( if (!binary_implication_graph_->AddAtMostOne(literals_scratchpad_)) { return SetModelUnsat(); } - - // In case this is the first constraint in the binary_implication_graph_. - // TODO(user): refactor so this is not needed! - InitializePropagators(); return true; } @@ -292,20 +268,12 @@ bool SatSolver::AddLinearConstraintInternal( // TODO(user): If this constraint forces all its literal to false (when rhs is // zero for instance), we still add it. Optimize this? - const bool result = pb_constraints_->AddConstraint(cst, rhs, trail_); - InitializePropagators(); - return result; + return pb_constraints_->AddConstraint(cst, rhs, trail_); } -bool SatSolver::AddLinearConstraint(bool use_lower_bound, - Coefficient lower_bound, - bool use_upper_bound, - Coefficient upper_bound, - std::vector* cst) { - SCOPED_TIME_STAT(&stats_); - CHECK_EQ(CurrentDecisionLevel(), 0); - if (model_is_unsat_) return false; - +void SatSolver::CanonicalizeLinear(std::vector* cst, + Coefficient* bound_shift, + Coefficient* max_value) { // This block removes assigned literals from the constraint. Coefficient fixed_variable_shift(0); { @@ -322,22 +290,43 @@ bool SatSolver::AddLinearConstraint(bool use_lower_bound, cst->resize(index); } - // Canonicalize the constraint. + // Now we canonicalize. // TODO(user): fix variables that must be true/false and remove them. - Coefficient bound_shift; - Coefficient max_value; - CHECK(ComputeBooleanLinearExpressionCanonicalForm(cst, &bound_shift, - &max_value)); - CHECK(SafeAddInto(fixed_variable_shift, &bound_shift)); + Coefficient bound_delta(0); + CHECK(ComputeBooleanLinearExpressionCanonicalForm(cst, &bound_delta, + max_value)); + + CHECK(SafeAddInto(bound_delta, bound_shift)); + CHECK(SafeAddInto(fixed_variable_shift, bound_shift)); +} + +bool SatSolver::AddLinearConstraint(bool use_lower_bound, + Coefficient lower_bound, + bool use_upper_bound, + Coefficient upper_bound, + std::vector* cst) { + SCOPED_TIME_STAT(&stats_); + CHECK_EQ(CurrentDecisionLevel(), 0); + if (model_is_unsat_) return false; + + Coefficient bound_shift(0); if (use_upper_bound) { + Coefficient max_value(0); + CanonicalizeLinear(cst, &bound_shift, &max_value); const Coefficient rhs = ComputeCanonicalRhs(upper_bound, bound_shift, max_value); if (!AddLinearConstraintInternal(*cst, rhs, max_value)) { return SetModelUnsat(); } } + if (use_lower_bound) { + // We need to "re-canonicalize" in case some literal were fixed while we + // processed one direction. + Coefficient max_value(0); + CanonicalizeLinear(cst, &bound_shift, &max_value); + // We transform the constraint into an upper-bounded one. for (int i = 0; i < cst->size(); ++i) { (*cst)[i].literal = (*cst)[i].literal.Negated(); @@ -371,7 +360,7 @@ int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation( return /*lbd=*/1; } - if (literals.size() == 2 && parameters_->treat_binary_clauses_separately()) { + if (literals.size() == 2) { if (track_binary_clauses_) { CHECK(binary_clauses_.Add(BinaryClause(literals[0], literals[1]))); } @@ -380,8 +369,6 @@ int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation( } CHECK(binary_implication_graph_->AddBinaryClauseDuringSearch(literals[0], literals[1])); - // In case this is the first binary clauses. - InitializePropagators(); return /*lbd=*/2; } @@ -454,9 +441,6 @@ void SatSolver::SaveDebugAssignment() { void SatSolver::AddBinaryClauseInternal(Literal a, Literal b) { if (!track_binary_clauses_ || binary_clauses_.Add(BinaryClause(a, b))) { binary_implication_graph_->AddBinaryClause(a, b); - - // In case this is the first binary clauses. - InitializePropagators(); } } @@ -683,8 +667,6 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() { if (!conflict_is_a_clause) { // Use the PB conflict. - // Note that we don't need to call InitializePropagators() since when we - // are here, we are sure we have at least one pb constraint. DCHECK_GT(pb_constraints_->NumberOfConstraints(), 0); CHECK_LT(pb_backjump_level, CurrentDecisionLevel()); Backtrack(pb_backjump_level); @@ -922,7 +904,7 @@ void SatSolver::Backtrack(int target_level) { bool SatSolver::AddBinaryClauses(const std::vector& clauses) { SCOPED_TIME_STAT(&stats_); CHECK_EQ(CurrentDecisionLevel(), 0); - for (BinaryClause c : clauses) { + for (const BinaryClause c : clauses) { if (trail_->Assignment().LiteralIsFalse(c.a) && trail_->Assignment().LiteralIsFalse(c.b)) { return SetModelUnsat(); @@ -1095,7 +1077,7 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) { return; } - if (parameters_->treat_binary_clauses_separately() && candidate.size() == 2) { + if (candidate.size() == 2) { counters_.minimization_num_removed_literals += clause->size() - 2; // The order is important for the drat proof. @@ -1595,7 +1577,7 @@ void SatSolver::ProcessNewlyFixedVariables() { drat_proof_handler_->DeleteClause({clause->begin(), old_size}); } - if (new_size == 2 && parameters_->treat_binary_clauses_separately()) { + if (new_size == 2) { // This clause is now a binary clause, treat it separately. Note that // it is safe to do that because this clause can't be used as a reason // since we are at level zero and the clause is not satisfied. @@ -1625,6 +1607,14 @@ void SatSolver::ProcessNewlyFixedVariables() { // part or the full integer part... bool SatSolver::Propagate() { SCOPED_TIME_STAT(&stats_); + + // If new binary or pb constraint were added for the first time, we need + // to "re-initialize" the list of propagators. + if ((!propagate_binary_ && !binary_implication_graph_->IsEmpty()) || + (!propagate_pb_ && pb_constraints_->NumberOfConstraints() > 0)) { + InitializePropagators(); + } + while (true) { // The idea here is to abort the inspection as soon as at least one // propagation occurs so we can loop over and test again the highest @@ -1649,18 +1639,19 @@ void SatSolver::InitializePropagators() { // To make Propagate() as fast as possible, we only add the // binary_implication_graph_/pb_constraints_ propagators if there is anything - // to propagate. Because of this, it is important to call - // InitializePropagators() after the first constraint of this kind is added. + // to propagate. // // TODO(user): uses the Model classes here to only call // model.GetOrCreate() when the first binary // constraint is needed, and have a mecanism to always make this propagator // first. Same for the linear constraints. if (!binary_implication_graph_->IsEmpty()) { + propagate_binary_ = true; propagators_.push_back(binary_implication_graph_); } propagators_.push_back(clauses_propagator_); if (pb_constraints_->NumberOfConstraints() > 0) { + propagate_pb_ = true; propagators_.push_back(pb_constraints_); } for (int i = 0; i < external_propagators_.size(); ++i) { @@ -1762,6 +1753,12 @@ void SatSolver::EnqueueNewDecision(Literal literal) { void SatSolver::Untrail(int target_trail_index) { SCOPED_TIME_STAT(&stats_); DCHECK_LT(target_trail_index, trail_->Index()); + + if ((!propagate_binary_ && !binary_implication_graph_->IsEmpty()) || + (!propagate_pb_ && pb_constraints_->NumberOfConstraints() > 0)) { + InitializePropagators(); + } + for (SatPropagator* propagator : propagators_) { propagator->Untrail(*trail_, target_trail_index); } diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h index db94d878a6..6cb8fa0d1c 100644 --- a/ortools/sat/sat_solver.h +++ b/ortools/sat/sat_solver.h @@ -97,16 +97,15 @@ class SatSolver { bool AddUnitClause(Literal true_literal); // Same as AddProblemClause() below, but for small clauses. - // - // TODO(user): Remove this and AddUnitClause() when initializer lists can be - // used in the open-source code like in AddClause({a, b}). bool AddBinaryClause(Literal a, Literal b); bool AddTernaryClause(Literal a, Literal b, Literal c); // Adds a clause to the problem. Returns false if the problem is detected to // be UNSAT. // - // TODO(user): Rename this to AddClause(). + // TODO(user): Rename this to AddClause(), also get rid of the specialized + // AddUnitClause(), AddBinaryClause() and AddTernaryClause() since they + // just end up calling this? bool AddProblemClause(absl::Span literals); // Adds a pseudo-Boolean constraint to the problem. Returns false if the @@ -542,6 +541,10 @@ class SatSolver { bool AddLinearConstraintInternal(const std::vector& cst, Coefficient rhs, Coefficient max_value); + // Makes sure a pseudo boolean constraint is in canonical form. + void CanonicalizeLinear(std::vector* cst, + Coefficient* bound_shift, Coefficient* max_value); + // Adds a learned clause to the problem. This should be called after // Backtrack(). The backtrack is such that after it is applied, all the // literals of the learned close except one will be false. Thus the last one @@ -692,6 +695,8 @@ class SatSolver { // Internal propagators. We keep them here because we need more than the // SatPropagator interface for them. + bool propagate_binary_ = false; + bool propagate_pb_ = false; BinaryImplicationGraph* binary_implication_graph_; LiteralWatchers* clauses_propagator_; PbConstraints* pb_constraints_; @@ -794,7 +799,7 @@ class SatSolver { std::vector dfs_stack_; std::vector variable_to_process_; - // Temporary member used by AddLinearConstraintInternal(). + // Temporary member used when adding clauses. std::vector literals_scratchpad_; // A boolean vector used to temporarily mark decision levels. @@ -818,9 +823,6 @@ class SatSolver { // analysis. VariableWithSameReasonIdentifier same_reason_identifier_; - // Temporary vector used by AddProblemClause(). - std::vector tmp_pb_constraint_; - // Boolean used to include/exclude constraints from the core computation. bool is_relevant_for_core_computation_; diff --git a/ortools/sat/synchronization.cc b/ortools/sat/synchronization.cc index 7d9022ad8b..08fd96ee95 100644 --- a/ortools/sat/synchronization.cc +++ b/ortools/sat/synchronization.cc @@ -133,10 +133,11 @@ std::string SatProgressMessage(const std::string& event_or_solution_count, } // namespace -void SharedResponseManager::LogMessage(std::string message) { +void SharedResponseManager::LogMessage(const std::string& prefix, + const std::string& message) { absl::MutexLock mutex_lock(&mutex_); - SOLVER_LOG(logger_, - absl::StrFormat("#Model %6.2fs %s", wall_timer_.Get(), message)); + SOLVER_LOG(logger_, absl::StrFormat("#%-5s %6.2fs %s", prefix, + wall_timer_.Get(), message)); } void SharedResponseManager::InitializeObjective(const CpModelProto& cp_model) { @@ -848,6 +849,13 @@ void SharedBoundsManager::LogStatistics(SolverLogger* logger) { } } +int SharedBoundsManager::NumBoundsExported(const std::string& worker_name) { + absl::MutexLock mutex_lock(&mutex_); + const auto it = bounds_exported_.find(worker_name); + if (it == bounds_exported_.end()) return 0; + return it->second; +} + int SharedClausesManager::RegisterNewId() { absl::MutexLock mutex_lock(&mutex_); const int id = id_to_last_processed_binary_clause_.size(); diff --git a/ortools/sat/synchronization.h b/ortools/sat/synchronization.h index c37926e285..0a7a5fb89e 100644 --- a/ortools/sat/synchronization.h +++ b/ortools/sat/synchronization.h @@ -327,7 +327,7 @@ class SharedResponseManager { // Display improvement stats. void DisplayImprovementStatistics(); - void LogMessage(std::string message); + void LogMessage(const std::string& prefix, const std::string& message); // This is here for the few codepath that needs to modify the returned // response directly. Note that this do not work in parallel. @@ -448,6 +448,7 @@ class SharedBoundsManager { void Synchronize(); void LogStatistics(SolverLogger* logger); + int NumBoundsExported(const std::string& worker_name); private: const int num_variables_;