From 7cb9f2b893a70f6e86601b381e7cec6414754e1d Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Fri, 9 Nov 2018 15:07:37 +0100 Subject: [PATCH] enable some of sat presolve when enumerating all solutions; polish jobshop_sat example --- examples/cpp/jobshop_sat.cc | 32 ++++-- ortools/sat/cp_model.cc | 10 +- ortools/sat/cp_model.h | 2 +- ortools/sat/cp_model_presolve.cc | 172 ++++++++++++++++-------------- ortools/sat/cp_model_presolve.h | 14 ++- ortools/sat/cp_model_solver.cc | 16 ++- ortools/sat/samples/cp_is_fun1.cc | 103 ++++++++++++++++++ ortools/sat/samples/cp_is_fun1.py | 103 ++++++++++++++++++ 8 files changed, 344 insertions(+), 108 deletions(-) create mode 100644 ortools/sat/samples/cp_is_fun1.cc create mode 100644 ortools/sat/samples/cp_is_fun1.py diff --git a/examples/cpp/jobshop_sat.cc b/examples/cpp/jobshop_sat.cc index 2c901fa0db..2869ec7037 100644 --- a/examples/cpp/jobshop_sat.cc +++ b/examples/cpp/jobshop_sat.cc @@ -106,7 +106,7 @@ void Solve(const JsspInputProblem& problem) { std::vector starts; std::vector ends; - Domain all_horizon(0, horizon); + const Domain all_horizon(0, horizon); const IntVar makespan = cp_model.NewIntVar(all_horizon); @@ -117,6 +117,7 @@ void Solve(const JsspInputProblem& problem) { std::vector> machine_to_presences(num_machines); std::vector job_starts(num_jobs); std::vector job_ends(num_jobs); + std::vector task_starts; int64 objective_offset = 0; std::vector objective_vars; std::vector objective_coeffs; @@ -156,6 +157,7 @@ void Solve(const JsspInputProblem& problem) { if (t == job.tasks_size() - 1) { job_ends[j] = end; } + task_starts.push_back(start); // Chain the task belonging to the same job. if (t > 0) { @@ -227,14 +229,24 @@ void Solve(const JsspInputProblem& problem) { // Earliness costs are not supported. CHECK_EQ(0L, job.earliness_cost_per_time_unit()); + const int64 lateness_penalty = job.lateness_cost_per_time_unit(); // Lateness cost. - if (job.lateness_cost_per_time_unit() != 0L) { - const IntVar lateness_var = cp_model.NewIntVar(all_horizon); - cp_model.AddGreaterOrEqual( - lateness_var, - LinearExpr(previous_end).AddConstant(-job.late_due_date())); - objective_vars.push_back(lateness_var); - objective_coeffs.push_back(job.lateness_cost_per_time_unit()); + if (lateness_penalty != 0L) { + const int64 due_date = job.late_due_date(); + if (due_date == 0) { + objective_vars.push_back(previous_end); + objective_coeffs.push_back(lateness_penalty); + } else { + const IntVar shifted_var = + cp_model.NewIntVar(Domain(-due_date, horizon - due_date)); + cp_model.AddEquality(shifted_var, + LinearExpr(previous_end).AddConstant(-due_date)); + const IntVar lateness_var = cp_model.NewIntVar(all_horizon); + cp_model.AddMaxEquality(lateness_var, + {cp_model.NewConstant(0), shifted_var}); + objective_vars.push_back(lateness_var); + objective_coeffs.push_back(lateness_penalty); + } } } @@ -294,11 +306,11 @@ void Solve(const JsspInputProblem& problem) { cp_model.Minimize(LinearExpr::ScalProd(objective_vars, objective_coeffs) .AddConstant(objective_offset)); if (problem.has_scaling_factor()) { - cp_model.SetObjectiveScaling(problem.scaling_factor().value()); + cp_model.ScaleObjectiveBy(problem.scaling_factor().value()); } // Decision strategy. - cp_model.AddDecisionStrategy(job_starts, + cp_model.AddDecisionStrategy(task_starts, DecisionStrategyProto::CHOOSE_LOWEST_MIN, DecisionStrategyProto::SELECT_MIN_VALUE); diff --git a/ortools/sat/cp_model.cc b/ortools/sat/cp_model.cc index 927f7eb7ed..a736e16b8e 100644 --- a/ortools/sat/cp_model.cc +++ b/ortools/sat/cp_model.cc @@ -686,14 +686,10 @@ void CpModelBuilder::Maximize(const LinearExpr& expr) { cp_model_.mutable_objective()->set_scaling_factor(-1.0); } -void CpModelBuilder::SetObjectiveScaling(double scaling) { +void CpModelBuilder::ScaleObjectiveBy(double scaling) { CHECK(cp_model_.has_objective()); - const double current_scaling = cp_model_.objective().scaling_factor(); - if (current_scaling >= 0.0) { - cp_model_.mutable_objective()->set_scaling_factor(scaling); - } else { - cp_model_.mutable_objective()->set_scaling_factor(-scaling); - } + cp_model_.mutable_objective()->set_scaling_factor( + scaling * cp_model_.objective().scaling_factor()); } void CpModelBuilder::AddDecisionStrategy( diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h index 839e62ff61..e2d00a3afc 100644 --- a/ortools/sat/cp_model.h +++ b/ortools/sat/cp_model.h @@ -632,7 +632,7 @@ class CpModelBuilder { // Sets scaling of the objective. (must be called after Minimize() of // Maximize()). 'scaling' must be > 0.0. - void SetObjectiveScaling(double scaling); + void ScaleObjectiveBy(double scaling); // Adds a decision strategy on a list of integer variables. void AddDecisionStrategy( diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 9e90e3c917..3f4627e245 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -94,8 +94,9 @@ struct PresolveContext { } // Returns true if this ref only appear in one constraint. - bool IsUnique(int ref) const { - return var_to_constraints[PositiveRef(ref)].size() == 1; + bool VariableIsUniqueAndRemovable(int ref) const { + return var_to_constraints[PositiveRef(ref)].size() == 1 && + !enumerate_all_solutions; } Domain DomainOf(int ref) const { @@ -343,6 +344,10 @@ struct PresolveContext { // Initially false, and set to true on the first inconsistency. bool is_unsat = false; + // Indicate if we are enumerating all solutions. This disable some presolve + // rules. + bool enumerate_all_solutions = false; + // Just used to display statistics on the presolve rules that were used. std::unordered_map stats_by_rule_name; @@ -390,7 +395,7 @@ bool PresolveEnforcementLiteral(ConstraintProto* ct, PresolveContext* context) { if (context->LiteralIsFalse(literal)) { context->UpdateRuleStats("false enforcement literal"); return RemoveConstraint(ct, context); - } else if (context->IsUnique(literal)) { + } else if (context->VariableIsUniqueAndRemovable(literal)) { // We can simply set it to false and ignore the constraint in this case. context->UpdateRuleStats("enforcement literal not used"); context->SetLiteralToFalse(literal); @@ -433,7 +438,7 @@ bool PresolveBoolOr(ConstraintProto* ct, PresolveContext* context) { // We can just set the variable to true in this case since it is not // used in any other constraint (note that we artifically bump the // objective var usage by 1). - if (context->IsUnique(literal)) { + if (context->VariableIsUniqueAndRemovable(literal)) { context->UpdateRuleStats("bool_or: singleton"); context->SetLiteralToTrue(literal); return RemoveConstraint(ct, context); @@ -506,7 +511,7 @@ bool PresolveBoolAnd(ConstraintProto* ct, PresolveContext* context) { changed = true; continue; } - if (context->IsUnique(literal)) { + if (context->VariableIsUniqueAndRemovable(literal)) { changed = true; context->SetLiteralToTrue(literal); continue; @@ -855,7 +860,7 @@ bool PresolveLinear(ConstraintProto* ct, PresolveContext* context) { // // TODO(user): In some case, we could still remove var, but we also need // to not keep the affine relationship around in the constraint count. - if (context->IsUnique(var) && + if (context->VariableIsUniqueAndRemovable(var) && context->affine_relations.ClassSize(var) == 1) { bool success; const auto term_domain = @@ -1334,8 +1339,8 @@ bool PresolveElement(ConstraintProto* ct, PresolveContext* context) { context->UpdateRuleStats("element: reduced target domain"); } - const bool unique_index = - context->IsUnique(index_ref) || context->IsFixed(index_ref); + const bool unique_index = context->VariableIsUniqueAndRemovable(index_ref) || + context->IsFixed(index_ref); if (all_constants && unique_index) { // This constraint is just here to reduce the domain of the target! We can // add it to the mapping_model to reconstruct the index value during @@ -1346,7 +1351,8 @@ bool PresolveElement(ConstraintProto* ct, PresolveContext* context) { } const bool unique_target = - context->IsUnique(target_ref) || context->IsFixed(target_ref); + context->VariableIsUniqueAndRemovable(target_ref) || + context->IsFixed(target_ref); if (all_included_in_target_domain && unique_target) { context->UpdateRuleStats("element: trivial index domain reduction"); *(context->mapping_model->add_constraints()) = *ct; @@ -1921,7 +1927,9 @@ void Probe(PresolveContext* context) { } void PresolvePureSatPart(PresolveContext* context) { - if (context->is_unsat) return; + // TODO(user, lperron): Reenable some SAT presolve with + // enumerate_all_solutions set to true. + if (context->is_unsat || context->enumerate_all_solutions) return; const int num_variables = context->working_model->variables_size(); SatPostsolver postsolver(num_variables); @@ -2507,18 +2515,75 @@ void PresolveToFixPoint(PresolveContext* context) { } } +void RemoveUnusedEquivalentVariables(PresolveContext* context) { + if (context->is_unsat || context->enumerate_all_solutions) return; + + // Remove all affine constraints (they will be re-added later if + // needed) in the presolved model. + for (int c = 0; c < context->working_model->constraints_size(); ++c) { + ConstraintProto* ct = context->working_model->mutable_constraints(c); + if (gtl::ContainsKey(context->affine_constraints, ct)) { + ct->Clear(); + context->UpdateConstraintVariableUsage(c); + continue; + } + } + + // Add back the affine relations to the presolved model or to the mapping + // model, depending where they are needed. + // + // TODO(user): unfortunately, for now, this duplicates the interval relations + // with a fixed size. + int num_affine_relations = 0; + for (int var = 0; var < context->working_model->variables_size(); ++var) { + if (context->IsFixed(var)) continue; + + const AffineRelation::Relation r = context->GetAffineRelation(var); + if (r.representative == var) continue; + + // We can get rid of this variable, only if: + // - it is not used elsewhere. + // - whatever the value of the representative, we can always find a value + // for this variable. + CpModelProto* proto; + if (context->var_to_constraints[var].empty()) { + // Make sure that domain(representative) is tight. + const Domain implied = context->DomainOf(var) + .AdditionWith({-r.offset, -r.offset}) + .InverseMultiplicationBy(r.coeff); + if (context->IntersectDomainWith(r.representative, implied)) { + LOG(WARNING) << "Domain of " << r.representative + << " was not fully propagated using the affine relation " + << "(representative =" << r.representative + << ", coeff = " << r.coeff << ", offset = " << r.offset + << ")"; + } + proto = context->mapping_model; + } else { + proto = context->working_model; + ++num_affine_relations; + } + + ConstraintProto* ct = proto->add_constraints(); + auto* arg = ct->mutable_linear(); + arg->add_vars(var); + arg->add_coeffs(1); + arg->add_vars(r.representative); + arg->add_coeffs(-r.coeff); + arg->add_domain(r.offset); + arg->add_domain(r.offset); + } + + // Update the variable usage. + context->UpdateNewConstraintsVariableUsage(); +} + } // namespace. // ============================================================================= // Public API. // ============================================================================= -void PresolveCpModel(CpModelProto* presolved_model, CpModelProto* mapping_model, - std::vector* postsolve_mapping) { - return PresolveCpModel(VLOG_IS_ON(1), presolved_model, mapping_model, - postsolve_mapping); -} - // The presolve works as follow: // // First stage: @@ -2534,12 +2599,16 @@ void PresolveCpModel(CpModelProto* presolved_model, CpModelProto* mapping_model, // - All the variables domain will be copied to the mapping_model. // - Everything will be remapped so that only the variables appearing in some // constraints will be kept and their index will be in [0, num_new_variables). -void PresolveCpModel(bool log_info, CpModelProto* presolved_model, - CpModelProto* mapping_model, +void PresolveCpModel(const PresolveOptions& options, + CpModelProto* presolved_model, CpModelProto* mapping_model, std::vector* postsolve_mapping) { PresolveContext context; context.working_model = presolved_model; context.mapping_model = mapping_model; + if (options.parameters != nullptr) { + context.enumerate_all_solutions = + options.parameters->enumerate_all_solutions(); + } // We copy the search strategy to the mapping_model. for (const auto& decision_strategy : presolved_model->search_strategy()) { @@ -2573,6 +2642,7 @@ void PresolveCpModel(bool log_info, CpModelProto* presolved_model, // TODO(user): Expose parameters to control this. Probe(&context); PresolveToFixPoint(&context); + RemoveUnusedEquivalentVariables(&context); // Run SAT specific presolve on the pure-SAT part of the problem. // Note that because this can only remove/fix variable not used in the other @@ -2615,17 +2685,6 @@ void PresolveCpModel(bool log_info, CpModelProto* presolved_model, // Regroup no-overlaps into max-cliques. MergeNoOverlapConstraints(&context); - // Remove all affine constraints (they will be re-added later if - // needed) in the presolved model. - for (int c = 0; c < presolved_model->constraints_size(); ++c) { - ConstraintProto* ct = presolved_model->mutable_constraints(c); - if (gtl::ContainsKey(context.affine_constraints, ct)) { - ct->Clear(); - context.UpdateConstraintVariableUsage(c); - continue; - } - } - if (context.working_model->has_objective()) { ExpandObjective(&context); } @@ -2635,56 +2694,6 @@ void PresolveCpModel(bool log_info, CpModelProto* presolved_model, // though. DCHECK(context.ConstraintVariableUsageIsConsistent()); - // Add back the affine relations to the presolved model or to the mapping - // model, depending where they are needed. - // - // TODO(user): unfortunately, for now, this duplicates the interval relations - // with a fixed size. - int num_affine_relations = 0; - for (int var = 0; var < presolved_model->variables_size(); ++var) { - if (context.IsFixed(var)) continue; - - const AffineRelation::Relation r = context.GetAffineRelation(var); - if (r.representative == var) continue; - - // We can get rid of this variable, only if: - // - it is not used elsewhere. - // - whatever the value of the representative, we can always find a value - // for this variable. - CpModelProto* proto; - if (context.var_to_constraints[var].empty()) { - // Make sure that domain(representative) is tight. - const Domain implied = context.DomainOf(var) - .AdditionWith({-r.offset, -r.offset}) - .InverseMultiplicationBy(r.coeff); - if (context.IntersectDomainWith(r.representative, implied)) { - LOG(WARNING) << "Domain of " << r.representative - << " was not fully propagated using the affine relation " - << "(representative =" << r.representative - << ", coeff = " << r.coeff << ", offset = " << r.offset - << ")"; - } - proto = context.mapping_model; - } else { - // This is needed for the corner cases where 2 variables in affine - // relation with the same representative are present but no one use - // the representative. This makes sure the code below will not try to - // delete the representative. - context.var_to_constraints[r.representative].insert(-1); - proto = context.working_model; - ++num_affine_relations; - } - - ConstraintProto* ct = proto->add_constraints(); - auto* arg = ct->mutable_linear(); - arg->add_vars(var); - arg->add_coeffs(1); - arg->add_vars(r.representative); - arg->add_coeffs(-r.coeff); - arg->add_domain(r.offset); - arg->add_domain(r.offset); - } - // Remove all empty constraints. Note that we need to remap the interval // references. std::vector interval_mapping(presolved_model->constraints_size(), -1); @@ -2780,10 +2789,9 @@ void PresolveCpModel(bool log_info, CpModelProto* presolved_model, ApplyVariableMapping(mapping, presolved_model); // Stats and checks. - if (log_info) { + if (VLOG_IS_ON(1)) { LOG(INFO) << "- " << context.affine_relations.NumRelations() - << " affine relations were detected. " << num_affine_relations - << " were kept."; + << " affine relations were detected."; LOG(INFO) << "- " << context.var_equiv_relations.NumRelations() << " variable equivalence relations were detected."; std::map sorted_rules(context.stats_by_rule_name.begin(), diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h index 4cda2fec22..08b5be3949 100644 --- a/ortools/sat/cp_model_presolve.h +++ b/ortools/sat/cp_model_presolve.h @@ -17,10 +17,18 @@ #include #include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { +struct PresolveOptions { + bool log_info = true; + SatParameters* parameters = nullptr; + TimeLimit* time_limit = nullptr; +}; + // Presolves the initial content of presolved_model. // // This also creates a mapping model that encode the correspondence between the @@ -42,10 +50,8 @@ namespace sat { // TODO(user): Identify disconnected components and returns a vector of // presolved model? If we go this route, it may be nicer to store the indices // inside the model. We can add a IntegerVariableProto::initial_index; -void PresolveCpModel(CpModelProto* presolved_model, CpModelProto* mapping_model, - std::vector* postsolve_mapping); -void PresolveCpModel(bool log_info, CpModelProto* presolved_model, - CpModelProto* mapping_model, +void PresolveCpModel(const PresolveOptions& options, + CpModelProto* presolved_model, CpModelProto* mapping_model, std::vector* postsolve_mapping); // Replaces all the instance of a variable i (and the literals referring to it) diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index b890e3444a..7770eda27f 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1873,7 +1873,12 @@ CpSolverResponse SolveCpModelWithLNS( { CpModelProto mapping_proto; std::vector postsolve_mapping; - PresolveCpModel(&local_problem, &mapping_proto, &postsolve_mapping); + PresolveOptions options; + options.log_info = VLOG_IS_ON(2); + options.parameters = local_model.GetOrCreate(); + options.time_limit = local_model.GetOrCreate(); + PresolveCpModel(options, &local_problem, &mapping_proto, + &postsolve_mapping); local_response = SolveCpModelInternal( local_problem, true, [](const CpSolverResponse& response) {}, &local_model); @@ -2180,12 +2185,15 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { // Presolve? std::function postprocess_solution; - if (params.cp_model_presolve() && !params.enumerate_all_solutions()) { + if (params.cp_model_presolve()) { // Do the actual presolve. CpModelProto mapping_proto; std::vector postsolve_mapping; - PresolveCpModel(VLOG_IS_ON(1), &new_model, &mapping_proto, - &postsolve_mapping); + PresolveOptions options; + options.log_info = VLOG_IS_ON(1); + options.parameters = model->GetOrCreate(); + options.time_limit = model->GetOrCreate(); + PresolveCpModel(options, &new_model, &mapping_proto, &postsolve_mapping); VLOG(1) << CpModelStats(new_model); postprocess_solution = [&model_proto, mapping_proto, postsolve_mapping](CpSolverResponse* response) { diff --git a/ortools/sat/samples/cp_is_fun1.cc b/ortools/sat/samples/cp_is_fun1.cc new file mode 100644 index 0000000000..73e090977c --- /dev/null +++ b/ortools/sat/samples/cp_is_fun1.cc @@ -0,0 +1,103 @@ +// Copyright 2010-2018 Google LLC +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// [START program] +// Cryptarithmetic puzzle +// +// First attempt to solve equation CP + IS + FUN = TRUE +// where each letter represents a unique digit. +// +// This problem has 72 different solutions in base 10. + +#include + +#include "ortools/sat/cp_model.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_parameters.pb.h" + +namespace operations_research { +namespace sat { + +void CPIsFun() { + // Instantiate the solver. + CpModelBuilder cp_model; + + const int64 kBase = 10; + + // [START variables] + // Define decision variables. + Domain digit(0, kBase - 1); + Domain non_zero_digit(1, kBase - 1); + + IntVar c = cp_model.NewIntVar(non_zero_digit).WithName("C"); + IntVar p = cp_model.NewIntVar(digit).WithName("P"); + IntVar i = cp_model.NewIntVar(non_zero_digit).WithName("I"); + IntVar s = cp_model.NewIntVar(digit).WithName("S"); + IntVar f = cp_model.NewIntVar(non_zero_digit).WithName("F"); + IntVar u = cp_model.NewIntVar(digit).WithName("U"); + IntVar n = cp_model.NewIntVar(digit).WithName("N"); + IntVar t = cp_model.NewIntVar(non_zero_digit).WithName("T"); + IntVar r = cp_model.NewIntVar(digit).WithName("R"); + IntVar e = cp_model.NewIntVar(digit).WithName("E"); + // [END variables] + + // [START constraints] + // Define constraints. + cp_model.AddAllDifferent({c, p, i, s, f, u, n, t, r, e}); + + // CP + IS + FUN = TRUE + cp_model.AddEquality( + LinearExpr::ScalProd({c, p, i, s, f, u, n}, + {kBase, 1, kBase, 1, kBase * kBase, kBase, 1}), + LinearExpr::ScalProd({t, r, u, e}, + {kBase * kBase * kBase, kBase * kBase, kBase, 1})); + LOG(INFO) << cp_model.Proto().DebugString(); + // [END constraints] + + // [START solve] + Model model; + + // Tell the solver to enumerate all solutions. + SatParameters parameters; + parameters.set_enumerate_all_solutions(true); + model.Add(NewSatParameters(parameters)); + + int num_solutions = 0; + model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& response) { + LOG(INFO) << "Solution " << num_solutions; + LOG(INFO) << "C=" << SolutionIntegerValue(response, c) << " " + << "P=" << SolutionIntegerValue(response, p) << " " + << "I=" << SolutionIntegerValue(response, i) << " " + << "S=" << SolutionIntegerValue(response, s) << " " + << "F=" << SolutionIntegerValue(response, f) << " " + << "U=" << SolutionIntegerValue(response, u) << " " + << "N=" << SolutionIntegerValue(response, n) << " " + << "T=" << SolutionIntegerValue(response, t) << " " + << "R=" << SolutionIntegerValue(response, r) << " " + << "E=" << SolutionIntegerValue(response, e); + num_solutions++; + })); + const CpSolverResponse response = SolveWithModel(cp_model, &model); + LOG(INFO) << "Number of solutions found: " << num_solutions; +} +// [END solve] + +} // namespace sat +} // namespace operations_research + +// ----- MAIN ----- +int main(int argc, char** argv) { + operations_research::sat::CPIsFun(); + return 0; +} +// [END program] diff --git a/ortools/sat/samples/cp_is_fun1.py b/ortools/sat/samples/cp_is_fun1.py new file mode 100644 index 0000000000..05c380aa75 --- /dev/null +++ b/ortools/sat/samples/cp_is_fun1.py @@ -0,0 +1,103 @@ +# Copyright 2010-2018 Google LLC +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +# [START program] +"""Cryptarithmetic puzzle. + +First attempt to solve equation CP + IS + FUN = TRUE +where each letter represents a unique digit. + +This problem has 72 different solutions in base 10. +""" + +# [START program] +from __future__ import print_function + +from ortools.sat.python import cp_model + + +# [START solution_printing] +class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback): + """Print intermediate solutions.""" + + def __init__(self, variables): + cp_model.CpSolverSolutionCallback.__init__(self) + self.__variables = variables + self.__solution_count = 0 + + def OnSolutionCallback(self): + self.__solution_count += 1 + for v in self.__variables: + print('%s=%i' % (v, self.Value(v)), end=' ') + print() + + def SolutionCount(self): + return self.__solution_count + + +# [END solution_printing] + + +def CPIsFun(): + """Solve the CP+IS+FUN==TRUE cryptarithm.""" + base = 10 + + # Constraint programming engine + model = cp_model.CpModel() + + # [START variables] + c = model.NewIntVar(1, 9, 'C') + p = model.NewIntVar(0, 9, 'P') + i = model.NewIntVar(1, 9, 'I') + s = model.NewIntVar(0, 9, 'S') + f = model.NewIntVar(1, 9, 'F') + u = model.NewIntVar(0, 9, 'U') + n = model.NewIntVar(0, 9, 'N') + t = model.NewIntVar(1, 9, 'T') + r = model.NewIntVar(0, 9, 'R') + e = model.NewIntVar(0, 9, 'E') + + # We need to group variables in a list to use the constraint AllDifferent. + letters = [c, p, i, s, f, u, n, t, r, e] + + # Verify that we have enough digits. + assert base >= len(letters) + # [END variables] + + # [START constraints] + # Define constraints. + model.AddAllDifferent(letters) + + # CP + IS + FUN = TRUE + model.Add(c * base + p + i * base + s + f * base * base + u * base + n == + t * base * base * base + r * base * base + u * base + e) + # [END constraints] + + # [START solve] + ### Solve model. + solver = cp_model.CpSolver() + solution_printer = VarArraySolutionPrinter(letters) + status = solver.SearchForAllSolutions(model, solution_printer) + # [END solve] + + print() + print('Statistics') + print(' - status : %s' % solver.StatusName(status)) + print(' - conflicts : %i' % solver.NumConflicts()) + print(' - branches : %i' % solver.NumBranches()) + print(' - wall time : %f ms' % solver.WallTime()) + print(' - solutions found : %i' % solution_printer.SolutionCount()) + + +if __name__ == '__main__': + CPIsFun() + # [END probram]