diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index 2093b0cae5..63902f1a09 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -776,7 +776,7 @@ void ExtractElementEncoding(const CpModelProto& model_proto, Model* m) { // TODO(user): It should be safe otherwise the exactly_one will have // duplicate literal, but I am not sure that if presolve is off we can // assume that. - sat_solver->AddProblemClause(clause, /*is_safe=*/false); + sat_solver->AddProblemClause(clause); } } if (need_extra_propagation) { @@ -1011,7 +1011,7 @@ void LoadBoolOrConstraint(const ConstraintProto& ct, Model* m) { for (const int ref : ct.enforcement_literal()) { literals.push_back(mapping->Literal(ref).Negated()); } - sat_solver->AddProblemClause(literals, /*is_safe=*/false); + sat_solver->AddProblemClause(literals); if (literals.size() == 3) { m->GetOrCreate()->ProcessTernaryClause(literals); } @@ -1026,7 +1026,7 @@ void LoadBoolAndConstraint(const ConstraintProto& ct, Model* m) { auto* sat_solver = m->GetOrCreate(); for (const Literal literal : mapping->Literals(ct.bool_and().literals())) { literals.push_back(literal); - sat_solver->AddProblemClause(literals, /*is_safe=*/false); + sat_solver->AddProblemClause(literals); literals.pop_back(); } } diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index fec2568c37..226ebeff7b 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -22,6 +22,7 @@ #include #include #include +#include #include #include #include @@ -5051,30 +5052,68 @@ bool CpModelPresolver::PresolveElement(int c, ConstraintProto* ct) { } } - // If the accessible part of the array is made of a single constant value, - // then we do not care about the index. And, because of the previous target - // domain reduction, the target is also fixed. - if (all_constants && context_->IsFixed(target)) { - context_->UpdateRuleStats("element: one value array"); - return RemoveConstraint(ct); - } - - // Special case when the index is boolean, and the array does not contain - // variables. - if (context_->MinOf(index) == 0 && context_->MaxOf(index) == 1 && - all_constants) { - const int64_t v0 = context_->FixedValue(ct->element().exprs(0)); - const int64_t v1 = context_->FixedValue(ct->element().exprs(1)); - - ConstraintProto* const eq = context_->working_model->add_constraints(); - eq->mutable_linear()->add_domain(v0); - eq->mutable_linear()->add_domain(v0); - AddLinearExpressionToLinearConstraint(target, 1, eq->mutable_linear()); - AddLinearExpressionToLinearConstraint(index, v0 - v1, eq->mutable_linear()); - context_->CanonicalizeLinearConstraint(eq); - context_->UpdateNewConstraintsVariableUsage(); - context_->UpdateRuleStats("element: linearize constant element of size 2"); - return RemoveConstraint(ct); + // Detect is the element is of the form a * index_var + b. + if (all_constants) { + if (context_->IsFixed(target)) { + // If the accessible part of the array is made of a single constant + // value, then we do not care about the index. And, because of the + // previous target domain reduction, the target is also fixed. + context_->UpdateRuleStats("element: one value array"); + return RemoveConstraint(ct); + } + std::optional first_index_var_value; + std::optional first_target_var_value; + std::optional slope; + bool is_affine = true; + const Domain& index_var_domain = context_->DomainOf(index_var); + for (const int64_t index_var_value : index_var_domain.Values()) { + const int64_t index_value = + AffineExpressionValueAt(index, index_var_value); + const int64_t expr_value = + context_->FixedValue(ct->element().exprs(index_value)); + const int64_t target_var_value = GetInnerVarValue(target, expr_value); + if (!first_index_var_value.has_value()) { + first_index_var_value = index_var_value; + first_target_var_value = target_var_value; + } else if (!slope.has_value()) { + const int64_t delta_x = index_var_value - first_index_var_value.value(); + const int64_t delta_y = + target_var_value - first_target_var_value.value(); + if (delta_y % delta_x != 0) { // not an integer slope. + is_affine = false; + break; + } + slope = delta_y / delta_x; + } else { // Non constant. + const int64_t delta_x = index_var_value - first_index_var_value.value(); + const int64_t delta_y = + target_var_value - first_target_var_value.value(); + if (delta_y % delta_x != 0) { // not an integer slope. + is_affine = false; + break; + } + if (slope.value() != delta_y / delta_x) { + is_affine = false; + break; + } + } + } + if (is_affine) { + DCHECK_NE(slope.value(), 0); + ConstraintProto* const lin = context_->working_model->add_constraints(); + lin->mutable_linear()->add_vars(target.vars(0)); + lin->mutable_linear()->add_coeffs(1); + lin->mutable_linear()->add_vars(index_var); + lin->mutable_linear()->add_coeffs(-slope.value()); + const int64_t offset = first_target_var_value.value() - + slope.value() * first_index_var_value.value(); + lin->mutable_linear()->add_domain(offset); + lin->mutable_linear()->add_domain(offset); + context_->CanonicalizeLinearConstraint(lin); + context_->UpdateNewConstraintsVariableUsage(); + context_->UpdateRuleStats("element: rewrite as affine constraint"); + return RemoveConstraint(ct); + } } // If a variable (target or index) appears only in this constraint, it does @@ -7462,7 +7501,7 @@ bool CpModelPresolver::PresolvePureSatPart() { for (const int ref : ct.enforcement_literal()) { clause.push_back(convert(ref).Negated()); } - sat_solver->AddProblemClause(clause, /*is_safe=*/false); + sat_solver->AddProblemClause(clause); context_->working_model->mutable_constraints(i)->Clear(); context_->UpdateConstraintVariableUsage(i); @@ -7488,7 +7527,7 @@ bool CpModelPresolver::PresolvePureSatPart() { clause.push_back(Literal(kNoLiteralIndex)); // will be replaced below. for (const int ref : ct.bool_and().literals()) { clause.back() = convert(ref); - sat_solver->AddProblemClause(clause, /*is_safe=*/false); + sat_solver->AddProblemClause(clause); } context_->working_model->mutable_constraints(i)->Clear(); diff --git a/ortools/sat/cp_model_solver_helpers.cc b/ortools/sat/cp_model_solver_helpers.cc index c78522abf0..e3ee3f9e85 100644 --- a/ortools/sat/cp_model_solver_helpers.cc +++ b/ortools/sat/cp_model_solver_helpers.cc @@ -1027,7 +1027,7 @@ int RegisterClausesLevelZeroImport(int id, for (const auto& [ref1, ref2] : new_binary_clauses) { const Literal l1 = mapping->Literal(ref1); const Literal l2 = mapping->Literal(ref2); - if (!sat_solver->AddBinaryClause(l1, l2)) { + if (!sat_solver->AddProblemClause({l1, l2})) { return false; } } diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index f5fab65702..39e0f4e34b 100644 --- a/ortools/sat/sat_solver.cc +++ b/ortools/sat/sat_solver.cc @@ -57,7 +57,6 @@ namespace sat { SatSolver::SatSolver() : SatSolver(new Model()) { owned_model_.reset(model_); model_->Register(this); - logger_ = model_->GetOrCreate(); } SatSolver::SatSolver(Model* model) @@ -161,7 +160,7 @@ bool SatSolver::AddClauseDuringSearch(absl::Span literals) { // Let filter clauses if we are at level zero if (trail_->CurrentDecisionLevel() == 0) { - return AddProblemClause(literals, /*is_safe=*/false); + return AddProblemClause(literals); } const int index = trail_->Index(); @@ -201,47 +200,36 @@ bool SatSolver::AddTernaryClause(Literal a, Literal b, Literal c) { return AddProblemClause({a, b, c}); } -// Note(user): we assume there is no duplicate literals in the clauses added -// here if is_safe is true. Most of the code works, but some advanced algo might -// be wrong/suboptimal if this is the case. So even when presolve is off we need -// some "cleanup" to enforce this invariant. Alternatively we could have robut -// algo in all the stack, but that seems a worse design. -bool SatSolver::AddProblemClause(absl::Span literals, - bool is_safe) { +// Note that we will do a bit of presolve here, which might not always be +// necessary if we know we are already adding a "clean" clause with no +// duplicates or literal equivalent to others. However, we found that it is +// better to make sure we always have "clean" clause in the solver rather than +// to over-optimize this. In particular, presolve might be disabled or +// incomplete, so such unclean clause might find their way here. +bool SatSolver::AddProblemClause(absl::Span literals) { SCOPED_TIME_STAT(&stats_); + DCHECK_EQ(CurrentDecisionLevel(), 0); if (model_is_unsat_) return false; - // Filter already assigned literals. - if (CurrentDecisionLevel() == 0) { - 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); - } - } else { - literals_scratchpad_.assign(literals.begin(), literals.end()); + // Filter already assigned literals. Note that we also remap literal in case + // we discovered equivalence later in the search. + literals_scratchpad_.clear(); + for (Literal l : literals) { + l = binary_implication_graph_->RepresentativeOf(l); + if (trail_->Assignment().LiteralIsTrue(l)) return true; + if (trail_->Assignment().LiteralIsFalse(l)) continue; + literals_scratchpad_.push_back(l); } - if (!is_safe) { - gtl::STLSortAndRemoveDuplicates(&literals_scratchpad_); - for (int i = 0; i + 1 < literals_scratchpad_.size(); ++i) { - if (literals_scratchpad_[i] == literals_scratchpad_[i + 1].Negated()) { - return true; - } + // A clause with l and not(l) is trivially true. + gtl::STLSortAndRemoveDuplicates(&literals_scratchpad_); + for (int i = 0; i + 1 < literals_scratchpad_.size(); ++i) { + if (literals_scratchpad_[i] == literals_scratchpad_[i + 1].Negated()) { + return true; } } - if (!AddProblemClauseInternal(literals_scratchpad_)) return false; - - // 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; + return AddProblemClauseInternal(literals_scratchpad_); } bool SatSolver::AddProblemClauseInternal(absl::Span literals) { @@ -278,6 +266,13 @@ bool SatSolver::AddProblemClauseInternal(absl::Span literals) { } } + // 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; } diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h index 84bbf0483f..716644da51 100644 --- a/ortools/sat/sat_solver.h +++ b/ortools/sat/sat_solver.h @@ -110,16 +110,21 @@ class SatSolver { 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. - // If is_safe is false, we will do some basic presolving like removing - // duplicate literals. + // Adds a clause to the problem. + // Returns false if the problem is detected to be UNSAT. // - // TODO(user): Rename this to AddClause(), also get rid of the specialized + // This must only be called at level zero, use AddClauseDuringSearch() for + // adding clause at a positive level. + // + // We call this a "problem" clause just because we will never delete such + // clause unless it is proven to always be satisfied. So this can be called + // with the initial clause of a problem, but also infered clause that we + // don't want to delete. + // + // 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, - bool is_safe = true); + bool AddProblemClause(absl::Span literals); // Adds a pseudo-Boolean constraint to the problem. Returns false if the // problem is detected to be UNSAT. If the constraint is always true, this @@ -941,8 +946,7 @@ inline std::function AtMostOneConstraint( inline std::function ClauseConstraint( absl::Span literals) { return [=](Model* model) { - model->GetOrCreate()->AddProblemClause(literals, - /*is_safe=*/false); + model->GetOrCreate()->AddProblemClause(literals); }; }