diff --git a/ortools/flatzinc/cp_model_fz_solver.cc b/ortools/flatzinc/cp_model_fz_solver.cc index 2cd0c74af0..a8d1c8f8c5 100644 --- a/ortools/flatzinc/cp_model_fz_solver.cc +++ b/ortools/flatzinc/cp_model_fz_solver.cc @@ -139,6 +139,9 @@ std::vector CpModelProtoWithMapping::LookupVars( for (int64 value : argument.values) { result.push_back(LookupConstant(value)); } + + } else if (argument.type == fz::Argument::INT_VALUE) { + result.push_back(LookupConstant(argument.Value())); } else { CHECK_EQ(argument.type, fz::Argument::INT_VAR_REF_ARRAY); for (fz::IntegerVariable* var : argument.variables) { @@ -256,9 +259,32 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct, arg->add_literals(FalseLiteral(var)); } } else if (fz_ct.type == "bool_xor") { - auto* arg = ct->mutable_bool_xor(); - arg->add_literals(TrueLiteral(LookupVar(fz_ct.arguments[0]))); - arg->add_literals(TrueLiteral(LookupVar(fz_ct.arguments[1]))); + // This is not the same semantics as the array_bool_xor as this constraint + // is actually a fully reified xor(a, b) <==> x. + const int a = LookupVar(fz_ct.arguments[0]); + const int b = LookupVar(fz_ct.arguments[1]); + const int x = LookupVar(fz_ct.arguments[2]); + + // not(x) => a == b + ct->add_enforcement_literal(NegatedRef(x)); + auto* const refute = ct->mutable_linear(); + refute->add_vars(a); + refute->add_coeffs(1); + refute->add_vars(b); + refute->add_coeffs(-1); + refute->add_domain(0); + refute->add_domain(0); + + // x => a + b == 1 + auto* ct2 = proto.add_constraints(); + ct2->add_enforcement_literal(x); + auto* const enforce = ct2->mutable_linear(); + enforce->add_vars(a); + enforce->add_coeffs(1); + enforce->add_vars(b); + enforce->add_coeffs(1); + enforce->add_domain(1); + enforce->add_domain(1); } else if (fz_ct.type == "array_bool_or") { auto* arg = ct->mutable_bool_or(); for (const int var : LookupVars(fz_ct.arguments[0])) { @@ -428,7 +454,8 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct, fz_ct.type == "array_var_int_element" || fz_ct.type == "array_var_bool_element" || fz_ct.type == "array_int_element_nonshifted") { - if (fz_ct.arguments[0].type == fz::Argument::INT_VAR_REF) { + if (fz_ct.arguments[0].type == fz::Argument::INT_VAR_REF || + fz_ct.arguments[0].type == fz::Argument::INT_VALUE) { auto* arg = ct->mutable_element(); arg->set_index(LookupVar(fz_ct.arguments[0])); arg->set_target(LookupVar(fz_ct.arguments[2])); diff --git a/ortools/flatzinc/fz.cc b/ortools/flatzinc/fz.cc index 9bf5f5a279..a04cac2b77 100644 --- a/ortools/flatzinc/fz.cc +++ b/ortools/flatzinc/fz.cc @@ -150,6 +150,12 @@ Model ParseFlatzincModel(const std::string& input, bool input_is_filename) { timer.Start(); presolve.Run(&model); FZLOG << " - done in " << timer.GetInMs() << " ms" << FZENDL; + } else { + FZLOG << "Presolve model using minimal rules" << FZENDL; + timer.Reset(); + timer.Start(); + presolve.RunMinimal(&model); + FZLOG << " - done in " << timer.GetInMs() << " ms" << FZENDL; } // Print statistics. diff --git a/ortools/flatzinc/presolve.cc b/ortools/flatzinc/presolve.cc index 19b55ecc70..c1a0439f0e 100644 --- a/ortools/flatzinc/presolve.cc +++ b/ortools/flatzinc/presolve.cc @@ -3644,6 +3644,50 @@ bool Presolver::RegroupDifferent(Model* model) { return killed > 0; } +bool Presolver::RunMinimal(Model* model) { + auto constraint = [model](int index) { return model->constraints()[index]; }; + + // Rebuild var_constraint map if empty. + if (var_to_constraint_indices_.empty()) { + for (int i = 0; i < model->constraints().size(); ++i) { + AddConstraintToMapping(i, constraint(i)); + } + } + + bool changed = false; + // Let's presolve the bool2int predicates first. + for (int index = 0; index < model->constraints().size(); ++index) { + Constraint* const ct = constraint(index); + if (ct->active && ct->type == "bool2int") { + std::string log; + ApplyRule(index, ct, "PresolveBool2Int", + [this](Constraint* ct, std::string* log) { + return PresolveBool2Int(ct, log); + }); + changed = true; + } + } + if (!var_representative_map_.empty()) { + // Some new substitutions were introduced. Let's process them. + SubstituteEverywhere(model); + var_representative_map_.clear(); + var_representative_vector_.clear(); + } + + // Report presolve rules statistics. + if (!successful_rules_.empty()) { + for (const auto& rule : successful_rules_) { + if (rule.second == 1) { + FZLOG << " - rule " << rule.first << " was applied 1 time" << FZENDL; + } else { + FZLOG << " - rule " << rule.first << " was applied " << rule.second + << " times" << FZENDL; + } + } + } + return changed; +} + bool Presolver::Run(Model* model) { // Check the validity of variable domains. for (const IntegerVariable* var : model->variables()) { diff --git a/ortools/flatzinc/presolve.h b/ortools/flatzinc/presolve.h index a75205e95b..c866bdc3c8 100644 --- a/ortools/flatzinc/presolve.h +++ b/ortools/flatzinc/presolve.h @@ -48,6 +48,11 @@ class Presolver { // TODO(user): Returns the number of rules applied instead. bool Run(Model* model); + // Minimal version of the presolve. + // TODO(user): Currently, without this, the solver fails on a series of + // problems like hrc_exp1-1-945_sat.fzn. To investigate. + bool RunMinimal(Model* model); + // Cleans the model for the CP solver. // In particular, it knows if we use a sat solver inside the CP // solver. In that case, for Boolean constraints, it remove the link