diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 323f2cd3de..b6a7853227 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -936,7 +936,8 @@ bool PresolveIntDiv(ConstraintProto* ct, PresolveContext* context) { } // Linearize if everything is positive. - if (context->MinOf(target) >= 0 && context->MinOf(ref_x) >= 0) { + if (context->MinOf(target) >= 0 && context->MinOf(ref_x) >= 0 && + divisor > 1) { LinearConstraintProto* const lin = context->working_model->add_constraints()->mutable_linear(); lin->add_vars(ref_x); diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index cf53cac26a..9f747693e4 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1441,12 +1441,16 @@ void SolveLoadedCpModel(const CpModelProto& model_proto, vars.push_back(var); values.push_back(IntegerValue(model_proto.solution_hint().values(i))); } - std::vector> decision_policies = { + + SearchHeuristics& search_heuristics = + *model->GetOrCreate(); + search_heuristics.policy_index = 0; + search_heuristics.decision_policies = { SequentialSearch({FollowHint(vars, values, model), SatSolverHeuristic(model), next_decision})}; auto no_restart = []() { return false; }; - const SatSolver::Status status = - SolveProblemWithPortfolioSearch(decision_policies, {no_restart}, model); + search_heuristics.restart_policies = {no_restart}; + const SatSolver::Status status = ResetAndSolveIntegerProblem({}, model); if (status == SatSolver::Status::FEASIBLE) { bool hint_is_valid = true; @@ -1507,9 +1511,9 @@ void SolveLoadedCpModel(const CpModelProto& model_proto, SatSolver::Status status; if (!model_proto.has_objective()) { + ConfigureSearchHeuristics(next_decision, model); while (true) { - status = SolveIntegerProblemWithLazyEncoding( - /*assumptions=*/{}, next_decision, model); + status = ResetAndSolveIntegerProblem(/*assumptions=*/{}, model); if (status != SatSolver::Status::FEASIBLE) break; solution_observer(*model); if (!parameters.enumerate_all_solutions()) break; @@ -1980,8 +1984,8 @@ void SolveCpModelWithLNS(const CpModelProto& model_proto, int num_workers, if (local_response.solution_info().empty()) { local_response.set_solution_info(solution_info); } else { - local_response.set_solution_info( - absl::StrCat(local_response.solution_info(), " ", solution_info)); + local_response.set_solution_info( + absl::StrCat(local_response.solution_info(), " ", solution_info)); } const bool neighborhood_is_reduced = neighborhood.is_reduced; diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index 04671ad54d..0a7beb779b 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -487,64 +487,60 @@ std::function SatSolverRestartPolicy(Model* model) { return [policy]() { return policy->ShouldRestart(); }; } -SatSolver::Status SolveIntegerProblemWithLazyEncoding( - const std::vector& assumptions, - const std::function& next_decision, Model* model) { - if (model->GetOrCreate()->LimitReached()) { - return SatSolver::LIMIT_REACHED; - } - SatSolver* const solver = model->GetOrCreate(); - if (!solver->ResetWithGivenAssumptions(assumptions)) { - return solver->UnsatStatus(); - } +void ConfigureSearchHeuristics( + const std::function& fixed_search, Model* model) { + SearchHeuristics& heuristics = *model->GetOrCreate(); + heuristics.policy_index = 0; + heuristics.decision_policies.clear(); + heuristics.restart_policies.clear(); + const SatParameters& parameters = *(model->GetOrCreate()); switch (parameters.search_branching()) { case SatParameters::AUTOMATIC_SEARCH: { - std::function search; + std::function decision_policy; if (parameters.randomize_search()) { - search = SequentialSearch( - {RandomizeOnRestartHeuristic(model), next_decision}); + decision_policy = RandomizeOnRestartHeuristic(model); } else { - search = SequentialSearch({SatSolverHeuristic(model), next_decision}); + decision_policy = SatSolverHeuristic(model); } + decision_policy = SequentialSearch({decision_policy, fixed_search}); if (parameters.exploit_integer_lp_solution() || parameters.exploit_all_lp_solution()) { - search = ExploitLpSolution(search, model); + decision_policy = ExploitLpSolution(decision_policy, model); } - return SolveProblemWithPortfolioSearch( - {search}, {SatSolverRestartPolicy(model)}, model); + heuristics.decision_policies = {decision_policy}; + heuristics.restart_policies = {SatSolverRestartPolicy(model)}; + return; } case SatParameters::FIXED_SEARCH: { - // Not all Boolean might appear in next_decision(), so once there is no + // Not all Boolean might appear in fixed_search(), so once there is no // decision left, we fix all Booleans that are still undecided. + heuristics.decision_policies = { + SequentialSearch({fixed_search, SatSolverHeuristic(model)})}; + if (parameters.randomize_search()) { - return SolveProblemWithPortfolioSearch( - {SequentialSearch({next_decision, SatSolverHeuristic(model)})}, - {SatSolverRestartPolicy(model)}, model); - } else { - // TODO(user): We might want to restart if external info is available. - // Code a custom restart for this? - auto no_restart = []() { return false; }; - return SolveProblemWithPortfolioSearch( - {SequentialSearch({next_decision, SatSolverHeuristic(model)})}, - {no_restart}, model); + heuristics.restart_policies = {SatSolverRestartPolicy(model)}; + return; } + + // TODO(user): We might want to restart if external info is available. + // Code a custom restart for this? + auto no_restart = []() { return false; }; + heuristics.restart_policies = {no_restart}; + return; } case SatParameters::PORTFOLIO_SEARCH: { - auto incomplete_portfolio = AddModelHeuristics({next_decision}, model); - auto portfolio = CompleteHeuristics( - incomplete_portfolio, - SequentialSearch({SatSolverHeuristic(model), next_decision})); + heuristics.decision_policies = CompleteHeuristics( + AddModelHeuristics({fixed_search}, model), + SequentialSearch({SatSolverHeuristic(model), fixed_search})); if (parameters.exploit_integer_lp_solution()) { - for (auto& ref : portfolio) { + for (auto& ref : heuristics.decision_policies) { ref = ExploitLpSolution(ref, model); } } - auto default_restart_policy = SatSolverRestartPolicy(model); - auto restart_policies = std::vector>( - portfolio.size(), default_restart_policy); - return SolveProblemWithPortfolioSearch(portfolio, restart_policies, - model); + heuristics.restart_policies.assign(heuristics.decision_policies.size(), + SatSolverRestartPolicy(model)); + return; } case SatParameters::LP_SEARCH: { // Fill portfolio with pseudocost heuristics. @@ -553,36 +549,36 @@ SatSolver::Status SolveIntegerProblemWithLazyEncoding( *(model->GetOrCreate())) { lp_heuristics.push_back(ct->LPReducedCostAverageBranching()); } - if (lp_heuristics.empty()) { // Revert to automatic search. - return SolveProblemWithPortfolioSearch( - {SequentialSearch({next_decision, SatSolverHeuristic(model)})}, - {SatSolverRestartPolicy(model)}, model); + if (lp_heuristics.empty()) { // Revert to fixed search. + heuristics.decision_policies = {SequentialSearch( + {fixed_search, SatSolverHeuristic(model)})}, + heuristics.restart_policies = {SatSolverRestartPolicy(model)}; + return; } - auto portfolio = CompleteHeuristics( + heuristics.decision_policies = CompleteHeuristics( lp_heuristics, - SequentialSearch({SatSolverHeuristic(model), next_decision})); - auto default_restart_policy = SatSolverRestartPolicy(model); - auto restart_policies = std::vector>( - portfolio.size(), default_restart_policy); - return SolveProblemWithPortfolioSearch(portfolio, restart_policies, - model); + SequentialSearch({SatSolverHeuristic(model), fixed_search})); + heuristics.restart_policies.assign(heuristics.decision_policies.size(), + SatSolverRestartPolicy(model)); + return; } case SatParameters::PSEUDO_COST_SEARCH: { std::function search = SequentialSearch( - {PseudoCost(model), SatSolverHeuristic(model), next_decision}); - search = IntegerValueSelectionHeuristic(search, model); - return SolveProblemWithPortfolioSearch( - {search}, {SatSolverRestartPolicy(model)}, model); + {PseudoCost(model), SatSolverHeuristic(model), fixed_search}); + heuristics.decision_policies = { + IntegerValueSelectionHeuristic(search, model)}; + heuristics.restart_policies = {SatSolverRestartPolicy(model)}; + return; } case SatParameters::PORTFOLIO_WITH_QUICK_RESTART_SEARCH: { std::function search = - SequentialSearch({RandomizeOnRestartHeuristic(model), next_decision}); - return SolveProblemWithPortfolioSearch( - {search}, - {RestartEveryKFailures(10, model->GetOrCreate())}, model); + SequentialSearch({RandomizeOnRestartHeuristic(model), fixed_search}); + heuristics.decision_policies = {search}; + heuristics.restart_policies = { + RestartEveryKFailures(10, model->GetOrCreate())}; + return; } } - return SatSolver::LIMIT_REACHED; } std::vector> AddModelHeuristics( @@ -617,24 +613,26 @@ void SolutionDetails::LoadFromTrail(const IntegerTrail& integer_trail) { solution_count++; } -SatSolver::Status SolveProblemWithPortfolioSearch( - std::vector> decision_policies, - std::vector> restart_policies, Model* model) { - const int num_policies = decision_policies.size(); - if (num_policies == 0) return SatSolver::FEASIBLE; - CHECK_EQ(num_policies, restart_policies.size()); - SatSolver* const solver = model->GetOrCreate(); +SatSolver::Status SolveIntegerProblem(Model* model) { + TimeLimit* time_limit = model->GetOrCreate(); + if (time_limit->LimitReached()) return SatSolver::LIMIT_REACHED; + + SearchHeuristics& heuristics = *model->GetOrCreate(); + const int num_policies = heuristics.decision_policies.size(); + CHECK_NE(num_policies, 0); + CHECK_EQ(num_policies, heuristics.restart_policies.size()); // This is needed for recording the pseudo-costs. IntegerVariable objective_var = kNoIntegerVariable; { const ObjectiveDefinition* objective = model->Get(); - if (objective != nullptr) objective_var = kNoIntegerVariable; + if (objective != nullptr) objective_var = objective->objective_var; } // Note that it is important to do the level-zero propagation if it wasn't // already done because EnqueueDecisionAndBackjumpOnConflict() assumes that // the solver is in a "propagated" state. + SatSolver* const solver = model->GetOrCreate(); if (!solver->FinishPropagation()) return solver->UnsatStatus(); // Create and initialize pseudo costs. @@ -645,19 +643,17 @@ SatSolver::Status SolveProblemWithPortfolioSearch( IntegerTrail* const integer_trail = model->GetOrCreate(); // Main search loop. - int policy_index = 0; - TimeLimit* time_limit = model->GetOrCreate(); const int64 old_num_conflicts = solver->num_failures(); const int64 conflict_limit = model->GetOrCreate()->max_number_of_conflicts(); while (!time_limit->LimitReached() && (solver->num_failures() - old_num_conflicts < conflict_limit)) { // If needed, restart and switch decision_policy. - if (restart_policies[policy_index]()) { + if (heuristics.restart_policies[heuristics.policy_index]()) { if (!solver->RestoreSolverToAssumptionLevel()) { return solver->UnsatStatus(); } - policy_index = (policy_index + 1) % num_policies; + heuristics.policy_index = (heuristics.policy_index + 1) % num_policies; } if (solver->CurrentDecisionLevel() == 0) { @@ -671,7 +667,8 @@ SatSolver::Status SolveProblemWithPortfolioSearch( } // Get next decision, try to enqueue. - const LiteralIndex decision = decision_policies[policy_index](); + const LiteralIndex decision = + heuristics.decision_policies[heuristics.policy_index](); // Record the changelist and objective bounds for updating pseudo costs. const std::vector bound_changes = @@ -712,8 +709,15 @@ SatSolver::Status SolveProblemWithPortfolioSearch( return SatSolver::Status::LIMIT_REACHED; } -// Shortcut when there is no assumption, and we consider all variables in -// order for the search decision. +SatSolver::Status ResetAndSolveIntegerProblem( + const std::vector& assumptions, Model* model) { + SatSolver* const solver = model->GetOrCreate(); + if (!solver->ResetWithGivenAssumptions(assumptions)) { + return solver->UnsatStatus(); + } + return SolveIntegerProblem(model); +} + SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model* model) { const IntegerVariable num_vars = model->GetOrCreate()->NumIntegerVariables(); @@ -721,11 +725,16 @@ SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model* model) { for (IntegerVariable var(0); var < num_vars; ++var) { all_variables.push_back(var); } - return SolveIntegerProblemWithLazyEncoding( - {}, FirstUnassignedVarAtItsMinHeuristic(all_variables, model), model); + + SearchHeuristics& heuristics = *model->GetOrCreate(); + heuristics.policy_index = 0; + heuristics.decision_policies = {SequentialSearch( + {SatSolverHeuristic(model), + FirstUnassignedVarAtItsMinHeuristic(all_variables, model)})}; + heuristics.restart_policies = {SatSolverRestartPolicy(model)}; + return ResetAndSolveIntegerProblem(/*assumptions=*/{}, model); } -// Logging helper. void LogNewSolution(const std::string& event_or_solution_count, double time_in_seconds, double obj_lb, double obj_ub, const std::string& solution_info) { diff --git a/ortools/sat/integer_search.h b/ortools/sat/integer_search.h index 8b9c2f4788..28234221e8 100644 --- a/ortools/sat/integer_search.h +++ b/ortools/sat/integer_search.h @@ -11,6 +11,15 @@ // See the License for the specific language governing permissions and // limitations under the License. +// This file contains all the top-level logic responsible for driving the search +// of a satisfiability integer problem. What decision we take next, which new +// Literal associated to an IntegerLiteral we create and when we restart. +// +// For an optimization problem, our algorithm solves a sequence of decision +// problem using this file as an entry point. Note that some heuristics here +// still use the objective if there is one in order to orient the search towards +// good feasible solution though. + #ifndef OR_TOOLS_SAT_INTEGER_SEARCH_H_ #define OR_TOOLS_SAT_INTEGER_SEARCH_H_ @@ -23,6 +32,68 @@ namespace operations_research { namespace sat { +// Model struct that contains the search heuristics used to find a feasible +// solution to an integer problem. +// +// This is reset by ConfigureSearchHeuristics() and used by +// SolveIntegerProblem(), see below. +struct SearchHeuristics { + // Decision and restart heuristics. The two vectors must be of the same size + // and restart_policies[i] will always be used in conjunction with + // decision_policies[i]. + std::vector> decision_policies; + std::vector> restart_policies; + + // Index in the vector above that indicate the current configuration. + int policy_index; +}; + +// Given a base "fixed_search" function that should mainly control in which +// order integer variables are lazily instantiated (and at what value), this +// uses the current solver parameters to set the SearchHeuristics class in the +// given model. +void ConfigureSearchHeuristics( + const std::function& fixed_search, Model* model); + +// For an optimization problem, this contains the internal integer objective +// to minimize and information on how to display it correctly in the logs. +struct ObjectiveDefinition { + double scaling_factor = 1.0; + double offset = 0.0; + IntegerVariable objective_var = kNoIntegerVariable; + + double ScaleIntegerObjective(IntegerValue value) const { + return (ToDouble(value) + offset) * scaling_factor; + } +}; + +// Callbacks that will be called when the search goes back to level 0. +// Callbacks should return false if the propagation fails. +struct LevelZeroCallbackHelper { + std::vector> callbacks; +}; + +// Tries to find a feasible solution to the current model. +// +// This function continues from the current state of the solver and loop until +// all variables are instantiated (i.e. the next decision is kNoLiteralIndex) or +// a search limit is reached. It uses the heuristic from the SearchHeuristics +// class in the model to decide when to restart and what next decision to take. +// +// Each time a restart happen, this increment the policy index modulo the number +// of heuristics to act as a portfolio search. +SatSolver::Status SolveIntegerProblem(Model* model); + +// Resets the solver to the given assumptions before calling +// SolveIntegerProblem(). +SatSolver::Status ResetAndSolveIntegerProblem( + const std::vector& assumptions, Model* model); + +// Mainly used for tests. This configures the model SearchHeuristics with a +// simple default heuristic and then call ResetAndSolveIntegerProblem() +// without any assumptions. +SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model* model); + // Returns decision corresponding to var at its lower bound. Returns // kNoLiteralIndex if the variable is fixed. LiteralIndex AtMinValue(IntegerVariable var, IntegerTrail* integer_trail, @@ -162,48 +233,6 @@ std::vector> CompleteHeuristics( const std::vector>& incomplete_heuristics, const std::function& completion_heuristic); -// A wrapper around SatSolver::Solve that handles integer variable with lazy -// encoding. Repeatedly calls SatSolver::Solve() on the model until the given -// next_decision() function return kNoLiteralIndex or the model is proved to -// be UNSAT. -// -// Returns the status of the last call to SatSolver::Solve(). -// -// Note that the next_decision() function must always return an unassigned -// literal or kNoLiteralIndex to end the search. -SatSolver::Status SolveIntegerProblemWithLazyEncoding( - const std::vector& assumptions, - const std::function& next_decision, Model* model); - -// Solves a problem with the given heuristics. -// heuristics[i] will be used with restart_policies[i] only. -SatSolver::Status SolveProblemWithPortfolioSearch( - std::vector> decision_policies, - std::vector> restart_policies, Model* model); - -// Shortcut for SolveIntegerProblemWithLazyEncoding() when there is no -// assumption and we consider all variables in their index order for the next -// search decision. -SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model* model); - -// For an optimization problem, this contains the internal integer objective -// to minimize and information on how to display it correctly in the logs. -struct ObjectiveDefinition { - double scaling_factor = 1.0; - double offset = 0.0; - IntegerVariable objective_var = kNoIntegerVariable; - - double ScaleIntegerObjective(IntegerValue value) const { - return (ToDouble(value) + offset) * scaling_factor; - } -}; - -// Callbacks that will be called when the search goes back to level 0. -// Callbacks should return false if the propagation fails. -struct LevelZeroCallbackHelper { - std::vector> callbacks; -}; - // Prints out a new optimization solution in a fixed format. void LogNewSolution(const std::string& event_or_solution_count, double time_in_seconds, double obj_lb, double obj_ub, diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc index d169ba31a7..7306fe9f18 100644 --- a/ortools/sat/optimization.cc +++ b/ortools/sat/optimization.cc @@ -1085,14 +1085,6 @@ SatSolver::Status SolveWithCardinalityEncodingAndCore( } } -SatSolver::Status MinimizeIntegerVariableWithLinearScan( - IntegerVariable objective_var, - const std::function& feasible_solution_observer, - Model* model) { - return MinimizeIntegerVariableWithLinearScanAndLazyEncoding( - true, objective_var, {}, feasible_solution_observer, model); -} - namespace { void LogSolveInfo(SatSolver::Status result, const SatSolver& sat_solver, const WallTimer& wall_timer, const UserTimer& user_timer, @@ -1118,7 +1110,7 @@ void LogSolveInfo(SatSolver::Status result, const SatSolver& sat_solver, SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding( bool log_info, IntegerVariable objective_var, - const std::function& next_decision, + const std::function& fixed_search, const std::function& feasible_solution_observer, Model* model) { // Timing. @@ -1140,8 +1132,8 @@ SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding( bool model_is_feasible = false; IntegerValue objective(kint64max); while (true) { - result = SolveIntegerProblemWithLazyEncoding(/*assumptions=*/{}, - next_decision, model); + ConfigureSearchHeuristics(fixed_search, model); + result = ResetAndSolveIntegerProblem(/*assumptions=*/{}, model); if (result != SatSolver::FEASIBLE) break; // The objective is the current lower bound of the objective_var. @@ -1186,7 +1178,7 @@ SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding( void RestrictObjectiveDomainWithBinarySearch( IntegerVariable objective_var, - const std::function& next_decision, + const std::function& fixed_search, const std::function& feasible_solution_observer, Model* model) { const SatParameters old_params = *model->GetOrCreate(); @@ -1228,13 +1220,13 @@ void RestrictObjectiveDomainWithBinarySearch( << " tried: [" << unknown_min << "," << unknown_max << "]" << " target: obj<=" << target; SatSolver::Status result; + ConfigureSearchHeuristics(fixed_search, model); if (target < ub) { const Literal assumption = integer_encoder->GetOrCreateAssociatedLiteral( IntegerLiteral::LowerOrEqual(objective_var, target)); - result = SolveIntegerProblemWithLazyEncoding({assumption}, next_decision, - model); + result = ResetAndSolveIntegerProblem({assumption}, model); } else { - result = SolveIntegerProblemWithLazyEncoding({}, next_decision, model); + result = ResetAndSolveIntegerProblem({}, model); } switch (result) { @@ -1295,14 +1287,15 @@ namespace { // - LIMIT_REACHED if we reached the time-limit before one of the two status // above could be decided. SatSolver::Status FindCores(std::vector assumptions, - const std::function& next_decision, + const std::function& fixed_search, Model* model, std::vector>* cores) { cores->clear(); SatSolver* sat_solver = model->GetOrCreate(); do { + ConfigureSearchHeuristics(fixed_search, model); const SatSolver::Status result = - SolveIntegerProblemWithLazyEncoding(assumptions, next_decision, model); + ResetAndSolveIntegerProblem(assumptions, model); if (result != SatSolver::ASSUMPTIONS_UNSAT) return result; std::vector core = sat_solver->GetLastIncompatibleDecisions(); if (sat_solver->parameters().minimize_core()) { @@ -1331,7 +1324,7 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding( bool log_info, IntegerVariable objective_var, const std::vector& variables, const std::vector& coefficients, - const std::function& next_decision, + const std::function& fixed_search, const std::function& feasible_solution_observer, Model* model) { const SatParameters& parameters = *(model->GetOrCreate()); @@ -1488,7 +1481,7 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding( -objective_offset.value())); result = MinimizeIntegerVariableWithLinearScanAndLazyEncoding( - false, objective_var, next_decision, feasible_solution_observer, + false, objective_var, fixed_search, feasible_solution_observer, model); break; } @@ -1545,10 +1538,11 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding( // Simple linear scan algorithm to find the optimal of var. some_cover_opt = true; while (best > integer_trail->LowerBound(var)) { - const Literal a = integer_encoder->GetOrCreateAssociatedLiteral( - IntegerLiteral::LowerOrEqual(var, best - 1)); - result = - SolveIntegerProblemWithLazyEncoding({a}, next_decision, model); + const Literal assumption = + integer_encoder->GetOrCreateAssociatedLiteral( + IntegerLiteral::LowerOrEqual(var, best - 1)); + ConfigureSearchHeuristics(fixed_search, model); + result = ResetAndSolveIntegerProblem({assumption}, model); if (result != SatSolver::FEASIBLE) break; best = integer_trail->LowerBound(var); @@ -1608,7 +1602,7 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding( // Solve under the assumptions. std::vector> cores; - result = FindCores(assumptions, next_decision, model, &cores); + result = FindCores(assumptions, fixed_search, model, &cores); if (result == SatSolver::FEASIBLE) { process_solution(); if (parameters.stop_after_first_solution()) { @@ -1723,7 +1717,7 @@ SatSolver::Status MinimizeWithHittingSetAndLazyEncoding( bool log_info, IntegerVariable objective_var, std::vector variables, std::vector coefficients, - const std::function& next_decision, + const std::function& fixed_search, const std::function& feasible_solution_observer, Model* model) { #if !defined(__PORTABLE_PLATFORM__) && (defined(USE_CBC) || defined(USE_SCIP)) @@ -1865,7 +1859,7 @@ SatSolver::Status MinimizeWithHittingSetAndLazyEncoding( // TODO(user): we could also randomly shuffle the assumptions to find more // cores for only one MIP solve. std::vector> cores; - result = FindCores(assumptions, next_decision, model, &cores); + result = FindCores(assumptions, fixed_search, model, &cores); if (result == SatSolver::FEASIBLE) { process_solution(); if (parameters.stop_after_first_solution()) { diff --git a/ortools/sat/optimization.h b/ortools/sat/optimization.h index acf96bffa5..eac322ef89 100644 --- a/ortools/sat/optimization.h +++ b/ortools/sat/optimization.h @@ -128,20 +128,15 @@ SatSolver::Status SolveWithCardinalityEncodingAndCore( // Model-based API, for now we just provide a basic algorithm that minimizes a // given IntegerVariable by solving a sequence of decision problem. // +// This keep solving the problem as long as fixed_search() do not return +// kNoLiteralIndex and hence lazily encode new variables. See the doc of +// SolveIntegerProblemWithLazyEncoding() for more details. +// // The "observer" function will be called each time a new feasible solution is // found. -SatSolver::Status MinimizeIntegerVariableWithLinearScan( - IntegerVariable objective_var, - const std::function& feasible_solution_observer, - Model* model); - -// Same as MinimizeIntegerVariableWithLinearScan() but keep solving the problem -// as long as next_decision() do not return kNoLiteralIndex and hence lazily -// encode new variables. See the doc of SolveIntegerProblemWithLazyEncoding() -// for more details. SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding( bool log_info, IntegerVariable objective_var, - const std::function& next_decision, + const std::function& fixed_search, const std::function& feasible_solution_observer, Model* model); @@ -149,7 +144,7 @@ SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding( // domain of objective_var. void RestrictObjectiveDomainWithBinarySearch( IntegerVariable objective_var, - const std::function& next_decision, + const std::function& fixed_search, const std::function& feasible_solution_observer, Model* model); @@ -161,7 +156,7 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding( bool log_info, IntegerVariable objective_var, const std::vector& variables, const std::vector& coefficients, - const std::function& next_decision, + const std::function& fixed_search, const std::function& feasible_solution_observer, Model* model); @@ -183,7 +178,7 @@ SatSolver::Status MinimizeWithHittingSetAndLazyEncoding( bool log_info, IntegerVariable objective_var, std::vector variables, std::vector coefficients, - const std::function& next_decision, + const std::function& fixed_search, const std::function& feasible_solution_observer, Model* model); diff --git a/ortools/sat/table.cc b/ortools/sat/table.cc index 7a25c5f4aa..f01f95de89 100644 --- a/ortools/sat/table.cc +++ b/ortools/sat/table.cc @@ -20,11 +20,13 @@ #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" +#include "absl/strings/str_cat.h" #include "absl/strings/str_join.h" #include "ortools/base/int_type.h" #include "ortools/base/logging.h" #include "ortools/base/map_util.h" #include "ortools/base/stl_util.h" +#include "ortools/sat/sat_base.h" #include "ortools/sat/sat_solver.h" #include "ortools/util/sorted_interval_list.h" @@ -94,16 +96,38 @@ void ProcessOneColumn( } } -void AddRegularPositiveTable( +void AddPositiveTable( const std::vector& vars, const std::vector>& tuples, const std::vector> values_per_var, - int64 any_value, Model* model) { - IntegerTrail* const integer_trail = model->GetOrCreate(); + int64 any_value, bool prefix_mode, Model* model) { const int n = vars.size(); + + // Domains have be propagated. Fully encode variables. + std::vector> encodings(n); + for (int i = 0; i < n; ++i) { + if (values_per_var.size() > 1) { + model->Add(FullyEncodeVariable(vars[i])); + encodings[i] = GetEncoding(vars[i], model); + } + } + + // Create one Boolean variable per tuple to indicate if it can still be + // selected or not. Note that we don't enforce exactly one tuple to be + // selected because these variables are just used by this constraint, so + // only the information "can't be selected" is important. + // + // TODO(user): If a value in one column is unique, we don't need to create + // a new BooleanVariable corresponding to this line since we can use the one + // corresponding to this value in that column. + // + // Note that if there is just one tuple, there is no need to create such + // variables since they are not used. std::vector tuple_literals; tuple_literals.reserve(tuples.size()); - if (tuples.size() == 2) { + if (tuples.size() == 1) { + tuple_literals.push_back(Literal(kTrueLiteralIndex)); + } else if (tuples.size() == 2) { tuple_literals.emplace_back(model->Add(NewBooleanVariable()), true); tuple_literals.emplace_back(tuple_literals[0].Negated()); } else if (tuples.size() > 2) { @@ -118,19 +142,14 @@ void AddRegularPositiveTable( std::vector active_values; std::vector any_tuple_literals; for (int i = 0; i < n; ++i) { + if (values_per_var[i].size() == 1) continue; + active_tuple_literals.clear(); active_values.clear(); any_tuple_literals.clear(); - const int64 first = tuples[0][i]; - bool all_equals = true; - for (int j = 0; j < tuple_literals.size(); ++j) { const int64 v = tuples[j][i]; - if (v != first) { - all_equals = false; - } - if (v == any_value) { any_tuple_literals.push_back(tuple_literals[j]); } else { @@ -139,51 +158,43 @@ void AddRegularPositiveTable( } } - if (all_equals && any_tuple_literals.empty() && first != any_value) { - model->Add(Equality(vars[i], first)); - } else if (!active_tuple_literals.empty()) { - const std::vector reached_values(values_per_var[i].begin(), - values_per_var[i].end()); - integer_trail->UpdateInitialDomain(vars[i], - Domain::FromValues(reached_values)); - model->Add(FullyEncodeVariable(vars[i])); + if (!active_tuple_literals.empty()) { ProcessOneColumn(active_tuple_literals, active_values, GetEncoding(vars[i], model), any_tuple_literals, model); } } -} -void AddFullyPrefixedPositiveTable( - const std::vector& vars, - const std::vector>& tuples, - const std::vector> values_per_var, - int64 any_value, Model* model) { - const int n = vars.size(); - std::vector> encodings(n); - for (int i = 0; i < n; ++i) { - model->Add(FullyEncodeVariable(vars[i])); - encodings[i] = GetEncoding(vars[i], model); - } + if (prefix_mode) { + // For each tuple, we add a clause prefix => last value. + std::vector clause; + for (int j = 0; j < tuples.size(); ++j) { + clause.clear(); + bool tuple_is_valid = true; + for (int i = 0; i + 1 < n; ++i) { + // Ignore fixed variables. + if (values_per_var[i].size() == 1) continue; - std::vector clause; - for (int j = 0; j < tuples.size(); ++j) { - clause.clear(); - bool tuple_is_valid = true; - for (int i = 0; i + 1 < n; ++i) { - const int64 v = tuples[j][i]; - if (v == any_value) continue; - if (!encodings[i].contains(IntegerValue(v))) { - tuple_is_valid = false; - break; + const int64 v = tuples[j][i]; + // Ignored 'any' created during compression. + if (v == any_value) continue; + + // Check the validity of the tuple. + const IntegerValue value(v); + if (!encodings[i].contains(value)) { + tuple_is_valid = false; + break; + } + clause.push_back(gtl::FindOrDie(encodings[i], value).Negated()); + } + + // Add the target of the implication. + const IntegerValue target_value = IntegerValue(tuples[j][n - 1]); + if (tuple_is_valid && encodings[n - 1].contains(target_value)) { + const Literal target_literal = + gtl::FindOrDie(encodings[n - 1], target_value); + clause.push_back(target_literal); + model->Add(ClauseConstraint(clause)); } - clause.push_back(gtl::FindOrDie(encodings[i], IntegerValue(v)).Negated()); - } - const IntegerValue target_value = IntegerValue(tuples[j][n - 1]); - if (tuple_is_valid && encodings[n - 1].contains(target_value)) { - const Literal target_literal = - gtl::FindOrDie(encodings[n - 1], target_value); - clause.push_back(target_literal); - model->Add(ClauseConstraint(clause)); } } } @@ -197,7 +208,6 @@ void CompressTuples(const std::vector& domain_sizes, int64 any_value, // Remove duplicates if any. gtl::STLSortAndRemoveDuplicates(tuples); - const int initial_num_tuples = tuples->size(); const int num_vars = (*tuples)[0].size(); std::vector to_remove; @@ -228,10 +238,6 @@ void CompressTuples(const std::vector& domain_sizes, int64 any_value, tuples->pop_back(); } } - if (initial_num_tuples != tuples->size()) { - VLOG(1) << "Compressed tuples from " << initial_num_tuples << " to " - << tuples->size(); - } } // Makes a static decomposition of a table constraint into clauses. @@ -243,8 +249,10 @@ void AddTableConstraint(const std::vector& vars, std::vector> tuples, Model* model) { const int n = vars.size(); IntegerTrail* integer_trail = model->GetOrCreate(); + const int num_original_tuples = tuples.size(); // Compute the set of possible values for each variable (from the table). + // Remove invalid tuples along the way. std::vector> values_per_var(n); int index = 0; while (index < tuples.size()) { @@ -267,12 +275,15 @@ void AddTableConstraint(const std::vector& vars, index++; } } + const int num_valid_tuples = tuples.size(); if (tuples.empty()) { model->GetOrCreate()->NotifyThatModelIsUnsat(); return; } + // Detect the case when the first n-1 columns are all different. + // This encodes the implication table (tuple of size n - 1) implies value. absl::flat_hash_set> prefixes; std::vector prefix(n); for (const std::vector& tuple : tuples) { @@ -280,19 +291,14 @@ void AddTableConstraint(const std::vector& vars, prefix.pop_back(); prefixes.insert(prefix); } - double prefix_space_size = 1.0; + const int num_prefix_tuples = prefixes.size(); + // Compute the maximum number of such prefix tuples. + double max_num_prefix_tuples = 1.0; for (int i = 0; i + 1 < n; ++i) { - prefix_space_size *= values_per_var[i].size(); - } - const bool prefix_is_key = prefixes.size() == tuples.size(); - const bool prefix_is_covering_domain = prefixes.size() == prefix_space_size; - - if (prefix_is_key && !prefix_is_covering_domain) { - VLOG(2) << "tuples = " << prefixes.size() - << " space = " << prefix_space_size << " | " << n; - } else if (prefix_is_key && prefix_is_covering_domain) { - VLOG(2) << "prefix = " << prefixes.size() << " | " << n; + max_num_prefix_tuples *= values_per_var[i].size(); } + // Detect if prefix tuples are all different. + const bool prefix_are_all_different = num_prefix_tuples == num_valid_tuples; // Compress tuples. const int64 any_value = kint64min; @@ -301,23 +307,64 @@ void AddTableConstraint(const std::vector& vars, domain_sizes.push_back(values_per_var[i].size()); } CompressTuples(domain_sizes, any_value, &tuples); + const int num_compressed_tuples = tuples.size(); - // Create one Boolean variable per tuple to indicate if it can still be - // selected or not. Note that we don't enforce exactly one tuple to be - // selected because these variables are just used by this constraint, so - // only the information "can't be selected" is important. - // - // TODO(user): If a value in one column is unique, we don't need to create - // a new BooleanVariable corresponding to this line since we can use the one - // corresponding to this value in that column. - // - // Note that if there is just one tuple, there is no need to create such - // variables since they are not used. - if (prefix_is_key && prefix_is_covering_domain) { - AddFullyPrefixedPositiveTable(vars, tuples, values_per_var, any_value, - model); - } else { - AddRegularPositiveTable(vars, tuples, values_per_var, any_value, model); + if (VLOG_IS_ON(2)) { + std::string message = absl::StrCat( + "Table: ", n, " variables, original tuples = ", num_original_tuples); + if (num_valid_tuples != num_original_tuples) { + absl::StrAppend(&message, ", valid tuples = ", num_valid_tuples); + } + if (prefix_are_all_different) { + if (num_prefix_tuples < max_num_prefix_tuples) { + absl::StrAppend(&message, ", partial prefix = ", num_prefix_tuples, "/", + max_num_prefix_tuples); + } else { + absl::StrAppend(&message, ", full prefix = true"); + } + } else { + absl::StrAppend(&message, ", num prefix tuples = ", prefixes.size()); + } + if (num_compressed_tuples != num_valid_tuples) { + absl::StrAppend(&message, + ", compressed tuples = ", num_compressed_tuples); + } + LOG(INFO) << message; + } + AddPositiveTable(vars, tuples, values_per_var, any_value, + prefix_are_all_different, model); + + if (prefix_are_all_different && num_prefix_tuples < max_num_prefix_tuples) { + // If we have a table of 'unique prefix' => value tuples. + // This table will likely not be negated, as the density of tuples will be + // less than 1 / size of the domain of the last variable. + // Still, just on the prefix part, it can be close to complete. + // For each missing prefix, we can add their negation as a valid clause. + // For this, we negate the prefix tuples, and add a negative table + // constraint on these. + std::vector> var_domains(n - 1); + for (int j = 0; j + 1 < n; ++j) { + var_domains[j].assign(values_per_var[j].begin(), values_per_var[j].end()); + std::sort(var_domains[j].begin(), var_domains[j].end()); + } + std::vector> negated_tuples; + std::vector tmp_tuple; + for (int i = 0; i < max_num_prefix_tuples; ++i) { + tmp_tuple.assign(n - 1, 0); + int index = i; + for (int j = 0; j + 1 < n; ++j) { + tmp_tuple[j] = var_domains[j][index % var_domains[j].size()]; + index /= var_domains[j].size(); + } + if (!gtl::ContainsKey(prefixes, tmp_tuple)) { + negated_tuples.push_back(tmp_tuple); + } + } + std::vector prefix_vars = vars; + prefix_vars.pop_back(); + VLOG(2) << " . add negated table with " << negated_tuples.size() + << " tuples"; + AddNegatedTableConstraint(prefix_vars, negated_tuples, model); } }