From f87f82e1bfd1e005dfd90b2c43229dbd21425f85 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Fri, 9 Aug 2019 11:54:04 -0700 Subject: [PATCH] cleanup flatzinc --- ortools/flatzinc/checker.cc | 2 +- ortools/flatzinc/cp_model_fz_solver.cc | 4 +- .../flatzinc/mznlib_sat/redefinitions-2.0.mzn | 4 + ortools/flatzinc/presolve.cc | 204 ++++++++---------- ortools/flatzinc/presolve.h | 1 + 5 files changed, 100 insertions(+), 115 deletions(-) diff --git a/ortools/flatzinc/checker.cc b/ortools/flatzinc/checker.cc index ece41358c4..8f61cf0ec2 100644 --- a/ortools/flatzinc/checker.cc +++ b/ortools/flatzinc/checker.cc @@ -615,7 +615,7 @@ bool CheckIntLtImp(const Constraint& ct, const int64 left = Eval(ct.arguments[0], evaluator); const int64 right = Eval(ct.arguments[1], evaluator); const bool status = Eval(ct.arguments[2], evaluator) != 0; - return (status && (left < right)) || status; + return (status && (left < right)) || !status; } bool CheckIntLtReif(const Constraint& ct, diff --git a/ortools/flatzinc/cp_model_fz_solver.cc b/ortools/flatzinc/cp_model_fz_solver.cc index de26e9feb7..3e63cc0757 100644 --- a/ortools/flatzinc/cp_model_fz_solver.cc +++ b/ortools/flatzinc/cp_model_fz_solver.cc @@ -691,8 +691,6 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct, void CpModelProtoWithMapping::FillReifOrImpliedConstraint( const fz::Constraint& fz_ct, ConstraintProto* ct) { // Start by adding a non-reified version of the same constraint. - const bool is_implication = absl::EndsWith(fz_ct.type, "_imp"); - std::string simplified_type; if (absl::EndsWith(fz_ct.type, "_reif")) { // Remove _reif. @@ -766,7 +764,7 @@ void CpModelProtoWithMapping::FillReifOrImpliedConstraint( } // One way implication. We can stop here. - if (is_implication) return; + if (absl::EndsWith(fz_ct.type, "_imp")) return; // Add the other side of the reification because CpModelProto only support // half reification. diff --git a/ortools/flatzinc/mznlib_sat/redefinitions-2.0.mzn b/ortools/flatzinc/mznlib_sat/redefinitions-2.0.mzn index d48cb0f6f8..01ccbf1aeb 100644 --- a/ortools/flatzinc/mznlib_sat/redefinitions-2.0.mzn +++ b/ortools/flatzinc/mznlib_sat/redefinitions-2.0.mzn @@ -44,6 +44,10 @@ include "nosets.mzn"; % include "nostring.mzn" % Half-Reified constraints +% Some of the predicated are commented out because: +% - we do not know if they are ever emited. +% - not sure they will improve the solver. +% Keeping them for completeness sake. %predicate array_bool_and_imp(array [int] of var bool: as, var bool: r); %predicate array_bool_or_imp(array [int] of var bool: as, var bool: r); %predicate array_bool_xor_imp(array [int] of var bool: as, var bool: r); diff --git a/ortools/flatzinc/presolve.cc b/ortools/flatzinc/presolve.cc index f3d3955f99..19b55ecc70 100644 --- a/ortools/flatzinc/presolve.cc +++ b/ortools/flatzinc/presolve.cc @@ -33,6 +33,8 @@ DEFINE_bool(fz_floats_are_ints, true, namespace operations_research { namespace fz { namespace { +enum PresolveState { ALWAYS_FALSE, ALWAYS_TRUE, UNDECIDED }; + // TODO(user): accept variables fixed to 0 or 1. bool Has01Values(IntegerVariable* var) { return var->domain.Min() == 0 && var->domain.Max() == 1; @@ -1640,29 +1642,28 @@ Presolver::RuleStatus Presolver::SimplifyLinear(Constraint* ct, } } - // 0 = always false. 1 = always true, 2 = unknown. - int state = 2; + PresolveState state = UNDECIDED; if (absl::StartsWith(ct->type, "int_lin_ge")) { if (rhs_min >= rhs) { - state = 1; + state = ALWAYS_TRUE; } else if (rhs_max < rhs) { - state = 0; + state = ALWAYS_FALSE; } } else if (absl::StartsWith(ct->type, "int_lin_le")) { if (rhs_min > rhs) { - state = 0; + state = ALWAYS_FALSE; } else if (rhs_max <= rhs) { - state = 1; + state = ALWAYS_TRUE; } } else if (rhs < rhs_min || rhs > rhs_max) { if (absl::StartsWith(ct->type, "int_lin_eq")) { - state = 0; + state = ALWAYS_FALSE; } else if (absl::StartsWith(ct->type, "int_lin_ne")) { - state = 1; + state = ALWAYS_TRUE; } } - if (state == 0) { + if (state == ALWAYS_FALSE) { if (absl::EndsWith(ct->type, "_reif") || absl::EndsWith(ct->type, "_imp")) { // Always false. Propagates to enforcement literal. SetConstraintAsIntEq(ct, ct->arguments[3].Var(), 0); @@ -1670,7 +1671,7 @@ Presolver::RuleStatus Presolver::SimplifyLinear(Constraint* ct, } else { return CONSTRAINT_ALWAYS_FALSE; } - } else if (state == 1) { + } else if (state == ALWAYS_TRUE) { if (absl::EndsWith(ct->type, "_reif")) { // Always true, protagate to reified literal. SetConstraintAsIntEq(ct, ct->arguments[3].Var(), 1); @@ -2403,19 +2404,19 @@ Presolver::RuleStatus Presolver::PropagateReifiedComparisons(Constraint* ct, // Propagate implied comparisons: int_eq_imp, int_ge_imp, int_le_imp: // -// Rule1: +// Rule 1: // Input : int_xx_imp(x, x, b) or bool_eq_imp(b1, b1, b) // Action: Remove constraint if xx in {le, ge, eq}, or set b to false otherwise. // Output: inactive constraint. // -// Rule 3: +// Rule 2: // Input : int_xx_imp(x, c, b) or bool_xx_imp(b1, t, b) or // int_xx_imp(c, x, b) or bool_xx_imp(t, b2, b) // Action: Assign b to true or false if this can be decided from the of x and // c, or the comparison of b1/b2 with t. // Output: inactive constraint of b was assigned a value. // -// Rule 4: +// Rule 3: // Input : int_xx_imp(x, y, b) or bool_xx_imp(b1, b1, b2). // Action: Assign b to true or false if this can be decided from the domain of // x and y. @@ -2436,29 +2437,29 @@ Presolver::RuleStatus Presolver::PropagateImpliedComparisons(Constraint* ct, return CONSTRAINT_ALWAYS_TRUE; } - // Rule 3, easy case. Both constants. + // Rule 2, easy case. Both constants. if (ct->arguments[0].HasOneValue() && ct->arguments[1].HasOneValue()) { const int64 a = ct->arguments[0].Value(); const int64 b = ct->arguments[1].Value(); - int state = 2; // 0 force_false, 1 force true, 2 unknown. + PresolveState state = UNDECIDED; if (id == "int_eq_imp" || id == "bool_eq_imp") { - state = (a == b); + state = (a == b) ? ALWAYS_TRUE : ALWAYS_FALSE; } else if (id == "int_ne_imp" || id == "bool_ne_imp") { - state = (a != b); + state = (a != b) ? ALWAYS_TRUE : ALWAYS_FALSE; } else if (id == "int_lt_imp" || id == "bool_lt_imp") { - state = (a < b); + state = (a < b) ? ALWAYS_TRUE : ALWAYS_FALSE; } else if (id == "int_gt_imp" || id == "bool_gt_imp") { - state = (a > b); + state = (a > b) ? ALWAYS_TRUE : ALWAYS_FALSE; } else if (id == "int_le_imp" || id == "bool_le_imp") { - state = (a <= b); + state = (a <= b) ? ALWAYS_TRUE : ALWAYS_FALSE; } else if (id == "int_ge_imp" || id == "bool_ge_imp") { - state = (a >= b); + state = (a >= b) ? ALWAYS_TRUE : ALWAYS_FALSE; } - if (state == 0) { + if (state == ALWAYS_FALSE) { log->append("force enforcement literal to false"); IntersectVarWithSingleton(ct->arguments[2].Var(), 0); return CONSTRAINT_ALWAYS_TRUE; - } else if (state == 1) { + } else if (state == ALWAYS_TRUE) { log->append("remove always true enforced constraint"); return CONSTRAINT_ALWAYS_TRUE; } @@ -2476,130 +2477,111 @@ Presolver::RuleStatus Presolver::PropagateImpliedComparisons(Constraint* ct, reverse = true; } if (var != nullptr) { - if (Has01Values(var) && - (id == "int_eq_imp" || id == "int_ne_imp" || id == "bool_eq_imp" || - id == "bool_ne_imp") && - (value == 0 || value == 1)) { - // Rule 2. (Ignored) - // bool parity = (id == "int_eq_imp" || id == "bool_eq_imp"); - // if (value == 0) { - // parity = !parity; - // } - // log->append("simplify constraint"); - // Argument target = ct->arguments[2]; - // ct->arguments.clear(); - // ct->arguments.push_back(Argument::IntVarRef(var)); - // ct->arguments.push_back(target); - // ct->type = parity ? "bool_eq" : "bool_not"; - // return CONSTRAINT_REWRITTEN; - return NOT_CHANGED; - } else { - // Rule 3. - int state = 2; // 0 force_false, 1 force true, 2 unknown. - if (id == "int_eq_imp" || id == "bool_eq_imp") { - if (var->domain.Contains(value)) { - if (var->domain.HasOneValue()) { - state = 1; - } - } else { - state = 0; - } - } else if (id == "int_ne_imp" || id == "bool_ne_imp") { - if (var->domain.Contains(value)) { - if (var->domain.HasOneValue()) { - state = 0; - } - } else { - state = 1; - } - } else if ((((id == "int_lt_imp" || id == "bool_lt_imp") && reverse) || - ((id == "int_gt_imp" || id == "bool_gt_imp") && !reverse)) && - !var->domain.IsAllInt64()) { // int_gt - if (var->domain.Min() > value) { - state = 1; - } else if (var->domain.Max() <= value) { - state = 0; - } - } else if ((((id == "int_lt_imp" || id == "bool_lt_imp") && !reverse) || - ((id == "int_gt_imp" || id == "bool_gt_imp") && reverse)) && - !var->domain.IsAllInt64()) { // int_lt - if (var->domain.Max() < value) { - state = 1; - } else if (var->domain.Min() >= value) { - state = 0; - } - } else if ((((id == "int_le_imp" || id == "bool_le_imp") && reverse) || - ((id == "int_ge_imp" || id == "bool_ge_imp") && !reverse)) && - !var->domain.IsAllInt64()) { // int_ge - if (var->domain.Min() >= value) { - state = 1; - } else if (var->domain.Max() < value) { - state = 0; - } - } else if ((((id == "int_le_imp" || id == "bool_le_imp") && !reverse) || - ((id == "int_ge_imp" || id == "bool_ge_imp") && reverse)) && - !var->domain.IsAllInt64()) { // int_le - if (var->domain.Max() <= value) { - state = 1; - } else if (var->domain.Min() > value) { - state = 0; + // Rule 2. + PresolveState state = UNDECIDED; + if (id == "int_eq_imp" || id == "bool_eq_imp") { + if (var->domain.Contains(value)) { + if (var->domain.HasOneValue()) { + state = ALWAYS_TRUE; } + } else { + state = ALWAYS_FALSE; } - if (state == 0) { - log->append("force enforcement literal to false"); - IntersectVarWithSingleton(ct->arguments[2].Var(), 0); - return CONSTRAINT_ALWAYS_TRUE; - } else if (state == 1) { - log->append("remove always true enforced constraint"); - return CONSTRAINT_ALWAYS_TRUE; + } else if (id == "int_ne_imp" || id == "bool_ne_imp") { + if (var->domain.Contains(value)) { + if (var->domain.HasOneValue()) { + state = ALWAYS_FALSE; + } + } else { + state = ALWAYS_TRUE; } + } else if ((((id == "int_lt_imp" || id == "bool_lt_imp") && reverse) || + ((id == "int_gt_imp" || id == "bool_gt_imp") && !reverse)) && + !var->domain.IsAllInt64()) { // int_gt + if (var->domain.Min() > value) { + state = ALWAYS_TRUE; + } else if (var->domain.Max() <= value) { + state = ALWAYS_FALSE; + } + } else if ((((id == "int_lt_imp" || id == "bool_lt_imp") && !reverse) || + ((id == "int_gt_imp" || id == "bool_gt_imp") && reverse)) && + !var->domain.IsAllInt64()) { // int_lt + if (var->domain.Max() < value) { + state = ALWAYS_TRUE; + } else if (var->domain.Min() >= value) { + state = ALWAYS_FALSE; + } + } else if ((((id == "int_le_imp" || id == "bool_le_imp") && reverse) || + ((id == "int_ge_imp" || id == "bool_ge_imp") && !reverse)) && + !var->domain.IsAllInt64()) { // int_ge + if (var->domain.Min() >= value) { + state = ALWAYS_TRUE; + } else if (var->domain.Max() < value) { + state = ALWAYS_FALSE; + } + } else if ((((id == "int_le_imp" || id == "bool_le_imp") && !reverse) || + ((id == "int_ge_imp" || id == "bool_ge_imp") && reverse)) && + !var->domain.IsAllInt64()) { // int_le + if (var->domain.Max() <= value) { + state = ALWAYS_TRUE; + } else if (var->domain.Min() > value) { + state = ALWAYS_FALSE; + } + } + if (state == ALWAYS_FALSE) { + log->append("force enforcement literal to false"); + IntersectVarWithSingleton(ct->arguments[2].Var(), 0); + return CONSTRAINT_ALWAYS_TRUE; + } else if (state == ALWAYS_TRUE) { + log->append("remove always true enforced constraint"); + return CONSTRAINT_ALWAYS_TRUE; } } - // Rule 4. + // Rule 3. if (!ct->arguments[0].HasOneValue() && !ct->arguments[1].HasOneValue()) { const Domain& ld = ct->arguments[0].Var()->domain; const Domain& rd = ct->arguments[1].Var()->domain; - int state = 2; // 0 force_false, 1 force true, 2 unknown. + PresolveState state = UNDECIDED; if (id == "int_eq_imp" || id == "bool_eq_imp") { if (!ld.OverlapsDomain(rd)) { - state = 0; + state = ALWAYS_FALSE; } } else if (id == "int_ne_imp" || id == "bool_ne_imp") { // TODO(user): Test if the domain are disjoint. if (ld.Min() > rd.Max() || ld.Max() < rd.Min()) { - state = 1; + state = ALWAYS_TRUE; } } else if (id == "int_lt_imp" || id == "bool_lt_imp") { if (ld.Max() < rd.Min()) { - state = 1; + state = ALWAYS_TRUE; } else if (ld.Min() >= rd.Max()) { - state = 0; + state = ALWAYS_FALSE; } } else if (id == "int_gt_imp" || id == "bool_gt_imp") { if (ld.Max() <= rd.Min()) { - state = 0; + state = ALWAYS_FALSE; } else if (ld.Min() > rd.Max()) { - state = 1; + state = ALWAYS_TRUE; } } else if (id == "int_le_imp" || id == "bool_le_imp") { if (ld.Max() <= rd.Min()) { - state = 1; + state = ALWAYS_TRUE; } else if (ld.Min() > rd.Max()) { - state = 0; + state = ALWAYS_FALSE; } } else if (id == "int_ge_imp" || id == "bool_ge_imp") { if (ld.Max() < rd.Min()) { - state = 0; + state = ALWAYS_FALSE; } else if (ld.Min() >= rd.Max()) { - state = 1; + state = ALWAYS_TRUE; } } - if (state == 0) { + if (state == ALWAYS_FALSE) { log->append("force enforcement literal to false"); IntersectVarWithSingleton(ct->arguments[2].Var(), 0); return CONSTRAINT_ALWAYS_TRUE; - } else if (state == 1) { + } else if (state == ALWAYS_TRUE) { log->append("remove always true enforced constraint"); return CONSTRAINT_ALWAYS_TRUE; } diff --git a/ortools/flatzinc/presolve.h b/ortools/flatzinc/presolve.h index 3b9c3fbea0..a75205e95b 100644 --- a/ortools/flatzinc/presolve.h +++ b/ortools/flatzinc/presolve.h @@ -207,6 +207,7 @@ class Presolver { // Stores abs_map_[x] = y if x = abs(y). absl::flat_hash_map abs_map_; + // Link the abs_var with its constraint. absl::flat_hash_map abs_ct_; // Stores affine_map_[x] = a * y + b.