always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

enable some of sat presolve when enumerating all solutions; polish jobshop_sat example

Browse Source
This commit is contained in:
Laurent Perron
2018-11-09 15:07:37 +01:00
parent 5d28e9fbcb
commit 7cb9f2b893
8 changed files with 344 additions and 108 deletions
Download Patch File Download Diff File Expand all files Collapse all files

32
examples/cpp/jobshop_sat.cc
View File

@@ -106,7 +106,7 @@ void Solve(const JsspInputProblem& problem) {
std::vector<int> starts;
std::vector<int> 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<std::vector<BoolVar>> machine_to_presences(num_machines);
std::vector<IntVar> job_starts(num_jobs);
std::vector<IntVar> job_ends(num_jobs);
std::vector<IntVar> task_starts;
int64 objective_offset = 0;
std::vector<IntVar> objective_vars;
std::vector<int64> 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);

10
ortools/sat/cp_model.cc
View File

@@ -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(

2
ortools/sat/cp_model.h
View File

@@ -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(

172
ortools/sat/cp_model_presolve.cc
View File

@@ -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<std::string, int> 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<int>* 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<int>* 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<int> 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<std::string, int> sorted_rules(context.stats_by_rule_name.begin(),

14
ortools/sat/cp_model_presolve.h
View File

@@ -17,10 +17,18 @@
#include <vector>
#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<int>* 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<int>* postsolve_mapping);
// Replaces all the instance of a variable i (and the literals referring to it)

16
ortools/sat/cp_model_solver.cc
View File

@@ -1873,7 +1873,12 @@ CpSolverResponse SolveCpModelWithLNS(
{
CpModelProto mapping_proto;
std::vector<int> postsolve_mapping;
PresolveCpModel(&local_problem, &mapping_proto, &postsolve_mapping);
PresolveOptions options;
options.log_info = VLOG_IS_ON(2);
options.parameters = local_model.GetOrCreate<SatParameters>();
options.time_limit = local_model.GetOrCreate<TimeLimit>();
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<void(CpSolverResponse * response)> 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<int> 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<SatParameters>();
options.time_limit = model->GetOrCreate<TimeLimit>();
PresolveCpModel(options, &new_model, &mapping_proto, &postsolve_mapping);
VLOG(1) << CpModelStats(new_model);
postprocess_solution = [&model_proto, mapping_proto,
postsolve_mapping](CpSolverResponse* response) {

103
ortools/sat/samples/cp_is_fun1.cc Normal file
View File

@@ -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 <vector>
#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]

103
ortools/sat/samples/cp_is_fun1.py Normal file
View File

@@ -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]