diff --git a/ortools/flatzinc/cp_model_fz_solver.cc b/ortools/flatzinc/cp_model_fz_solver.cc index 8b21ec8cec..456ad64fef 100644 --- a/ortools/flatzinc/cp_model_fz_solver.cc +++ b/ortools/flatzinc/cp_model_fz_solver.cc @@ -424,7 +424,11 @@ void CpModelProtoWithMapping::BuildTableFromDomainIntLinEq( const std::vector vars = LookupVars(fz_ct.arguments[1]); const int rhs = fz_ct.arguments[2].Value(); CHECK_EQ(coeffs.back(), -1); - for (const int var : vars) ct->mutable_table()->add_vars(var); + for (const int var : vars) { + LinearExpressionProto* expr = ct->mutable_table()->add_exprs(); + expr->add_vars(var); + expr->add_coeffs(1); + } switch (vars.size()) { case 3: { @@ -732,7 +736,15 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct, } } else if (fz_ct.type == "ortools_table_int") { auto* arg = ct->mutable_table(); - for (const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(var); + for (const VarOrValue v : LookupVarsOrValues(fz_ct.arguments[0])) { + LinearExpressionProto* expr = arg->add_exprs(); + if (v.var != kNoVar) { + expr->add_vars(v.var); + expr->add_coeffs(1); + } else { + expr->set_offset(v.value); + } + } for (const int64_t value : fz_ct.arguments[1].values) arg->add_values(value); } else if (fz_ct.type == "ortools_regular") { diff --git a/ortools/flatzinc/fz.cc b/ortools/flatzinc/fz.cc index e8131937e4..74b3a3c608 100644 --- a/ortools/flatzinc/fz.cc +++ b/ortools/flatzinc/fz.cc @@ -32,6 +32,7 @@ #include "absl/strings/match.h" #include "absl/strings/str_split.h" #include "absl/strings/string_view.h" +#include "absl/time/time.h" #include "ortools/base/commandlineflags.h" #include "ortools/base/logging.h" #include "ortools/base/path.h" @@ -127,7 +128,7 @@ std::vector FixAndParseParameters(int* argc, char*** argv) { } Model ParseFlatzincModel(const std::string& input, bool input_is_filename, - SolverLogger* logger) { + SolverLogger* logger, absl::Duration* parse_duration) { WallTimer timer; timer.Start(); @@ -147,8 +148,9 @@ Model ParseFlatzincModel(const std::string& input, bool input_is_filename, CHECK(ParseFlatzincString(input, &model)); } + *parse_duration = timer.GetDuration(); SOLVER_LOG(logger, "File ", (input_is_filename ? input : "stdin"), - " parsed in ", timer.GetInMs(), " ms"); + " parsed in ", absl::ToInt64Milliseconds(*parse_duration), " ms"); SOLVER_LOG(logger, ""); // Print statistics. @@ -205,9 +207,11 @@ int main(int argc, char** argv) { logger.SetLogToStdOut(true); } + absl::Duration parse_duration; operations_research::fz::Model model = operations_research::fz::ParseFlatzincModel( - input, !absl::GetFlag(FLAGS_read_from_stdin), &logger); + input, !absl::GetFlag(FLAGS_read_from_stdin), &logger, + &parse_duration); operations_research::sat::ProcessFloatingPointOVariablesAndObjective(&model); operations_research::fz::FlatzincSatParameters parameters; @@ -219,7 +223,8 @@ int main(int argc, char** argv) { parameters.random_seed = absl::GetFlag(FLAGS_fz_seed); parameters.display_statistics = absl::GetFlag(FLAGS_statistics); parameters.number_of_threads = absl::GetFlag(FLAGS_threads); - parameters.max_time_in_seconds = absl::GetFlag(FLAGS_time_limit); + parameters.max_time_in_seconds = + absl::GetFlag(FLAGS_time_limit) - absl::ToInt64Seconds(parse_duration); parameters.ortools_mode = absl::GetFlag(FLAGS_ortools_mode); operations_research::SolverLogger solution_logger; diff --git a/ortools/java/com/google/ortools/sat/CpModel.java b/ortools/java/com/google/ortools/sat/CpModel.java index 678c70ceaf..78e54140b0 100644 --- a/ortools/java/com/google/ortools/sat/CpModel.java +++ b/ortools/java/com/google/ortools/sat/CpModel.java @@ -448,59 +448,59 @@ public MultipleCircuitConstraint addMultipleCircuit() { } /** - * Adds {@code AllowedAssignments(variables)}. + * Adds {@code AllowedAssignments(expressions)}. * - *

An AllowedAssignments constraint is a constraint on an array of variables that forces, when - * all variables are fixed to a single value, that the corresponding list of values is equal to - * one of the tuples of the tupleList. + *

An AllowedAssignments constraint is a constraint on an array of affine expressions that + * forces, when all expressions are fixed to a single value, that the corresponding list of values + * is equal to one of the tuples of the tupleList. * - * @param variables a list of variables + * @param expressions a list of affine expressions (a * var + b) * @return an instance of the TableConstraint class without any tuples. Tuples can be added * directly to the table constraint. */ - public TableConstraint addAllowedAssignments(IntVar[] variables) { - return addAllowedAssignments(Arrays.asList(variables)); + public TableConstraint addAllowedAssignments(LinearArgument[] expressions) { + return addAllowedAssignments(Arrays.asList(expressions)); } /** - * Adds {@code AllowedAssignments(variables)}. + * Adds {@code AllowedAssignments(expressions)}. * - * @see addAllowedAssignments(IntVar[]) + * @see addAllowedAssignments(LinearArgument[] expressions) */ - public TableConstraint addAllowedAssignments(Iterable variables) { + public TableConstraint addAllowedAssignments(Iterable expressions) { TableConstraint ct = new TableConstraint(modelBuilder); TableConstraintProto.Builder table = ct.getBuilder().getTableBuilder(); - for (IntVar var : variables) { - table.addVars(var.getIndex()); + for (LinearArgument expr : expressions) { + table.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(expr, /* negate= */ false)); } table.setNegated(false); return ct; } /** - * Adds {@code ForbiddenAssignments(variables)}. + * Adds {@code ForbiddenAssignments(expressions)}. * - *

A ForbiddenAssignments constraint is a constraint on an array of variables where the list of - * impossible combinations is provided in the tuples list. + *

A ForbiddenAssignments constraint is a constraint on an array of affine expressions where + * the list of impossible combinations is provided in the tuples list. * - * @param variables a list of variables + * @param expressions a list of affine expressions (a * var + b) * @return an instance of the TableConstraint class without any tuples. Tuples can be added * directly to the table constraint. */ - public TableConstraint addForbiddenAssignments(IntVar[] variables) { - return addForbiddenAssignments(Arrays.asList(variables)); + public TableConstraint addForbiddenAssignments(LinearArgument[] expressions) { + return addForbiddenAssignments(Arrays.asList(expressions)); } /** - * Adds {@code ForbiddenAssignments(variables)}. + * Adds {@code ForbiddenAssignments(expressions)}. * - * @see addForbiddenAssignments(IntVar[]) + * @see addForbiddenAssignments(LinearArgument[] expressions) */ - public TableConstraint addForbiddenAssignments(Iterable variables) { + public TableConstraint addForbiddenAssignments(Iterable expressions) { TableConstraint ct = new TableConstraint(modelBuilder); TableConstraintProto.Builder table = ct.getBuilder().getTableBuilder(); - for (IntVar var : variables) { - table.addVars(var.getIndex()); + for (LinearArgument expr : expressions) { + table.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(expr, /* negate= */ false)); } table.setNegated(true); return ct; diff --git a/ortools/java/com/google/ortools/sat/TableConstraint.java b/ortools/java/com/google/ortools/sat/TableConstraint.java index 09137c3e1c..c6a6145e82 100644 --- a/ortools/java/com/google/ortools/sat/TableConstraint.java +++ b/ortools/java/com/google/ortools/sat/TableConstraint.java @@ -32,13 +32,13 @@ public TableConstraint(CpModelProto.Builder builder) { * * @param tuple the tuple to add to the constraint. * @throws CpModel.WrongLength if the tuple does not have the same length as the array of - * variables of the constraint. + * expressions of the constraint. */ public TableConstraint addTuple(int[] tuple) { TableConstraintProto.Builder table = getBuilder().getTableBuilder(); - if (tuple.length != table.getVarsCount()) { + if (tuple.length != table.getExprsCount()) { throw new CpModel.WrongLength( - "addTuple", "tuple does not have the same length as the variables"); + "addTuple", "tuple does not have the same length as the expressions"); } for (int value : tuple) { table.addValues(value); @@ -51,13 +51,13 @@ public TableConstraint addTuple(int[] tuple) { * * @param tuple the tuple to add to the constraint. * @throws CpModel.WrongLength if the tuple does not have the same length as the array of - * variables of the constraint. + * expressions of the constraint. */ public TableConstraint addTuple(long[] tuple) { TableConstraintProto.Builder table = getBuilder().getTableBuilder(); - if (tuple.length != table.getVarsCount()) { + if (tuple.length != table.getExprsCount()) { throw new CpModel.WrongLength( - "addTuple", "tuple does not have the same length as the variables"); + "addTuple", "tuple does not have the same length as the expressions"); } for (long value : tuple) { table.addValues(value); @@ -75,9 +75,9 @@ public TableConstraint addTuple(long[] tuple) { public TableConstraint addTuples(int[][] tuples) { TableConstraintProto.Builder table = getBuilder().getTableBuilder(); for (int[] tuple : tuples) { - if (tuple.length != table.getVarsCount()) { + if (tuple.length != table.getExprsCount()) { throw new CpModel.WrongLength( - "addTuples", "a tuple does not have the same length as the variables"); + "addTuples", "a tuple does not have the same length as the expressions"); } for (int value : tuple) { table.addValues(value); @@ -91,12 +91,12 @@ public TableConstraint addTuples(int[][] tuples) { * * @param tuples the list of tuples to add to the constraint. * @throws CpModel.WrongLength if one tuple does not have the same length as the array of - * variables of the constraint. + * expressions of the constraint. */ public TableConstraint addTuples(long[][] tuples) { TableConstraintProto.Builder table = getBuilder().getTableBuilder(); for (long[] tuple : tuples) { - if (tuple.length != table.getVarsCount()) { + if (tuple.length != table.getExprsCount()) { throw new CpModel.WrongLength( "addTuples", "a tuple does not have the same length as the variables"); } diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index a8477d00e0..45f428eaa5 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -743,7 +743,7 @@ cc_library( ":util", "//ortools/algorithms:sparse_permutation", "//ortools/base", - "//ortools/base:mathutil", + "//ortools/base:stl_util", "//ortools/port:proto_utils", "//ortools/util:affine_relation", "//ortools/util:bitset", diff --git a/ortools/sat/cp_model.cc b/ortools/sat/cp_model.cc index d73d235689..1b92b5a482 100644 --- a/ortools/sat/cp_model.cc +++ b/ortools/sat/cp_model.cc @@ -524,7 +524,7 @@ void MultipleCircuitConstraint::AddArc(int tail, int head, BoolVar literal) { } void TableConstraint::AddTuple(absl::Span tuple) { - CHECK_EQ(tuple.size(), proto_->table().vars_size()); + CHECK_EQ(tuple.size(), proto_->table().exprs_size()); for (const int64_t t : tuple) { proto_->mutable_table()->add_values(t); } @@ -986,24 +986,55 @@ MultipleCircuitConstraint CpModelBuilder::AddMultipleCircuitConstraint() { } TableConstraint CpModelBuilder::AddAllowedAssignments( - absl::Span vars) { + absl::Span expressions) { ConstraintProto* const proto = cp_model_.add_constraints(); - for (const IntVar& var : vars) { - proto->mutable_table()->add_vars(var.index_); + for (const LinearExpr& expr : expressions) { + *proto->mutable_table()->add_exprs() = LinearExprToProto(expr); } return TableConstraint(proto); } -TableConstraint CpModelBuilder::AddForbiddenAssignments( - absl::Span vars) { +TableConstraint CpModelBuilder::AddAllowedAssignments( + absl::Span variables) { ConstraintProto* const proto = cp_model_.add_constraints(); - for (const IntVar& var : vars) { - proto->mutable_table()->add_vars(var.index_); + for (const IntVar var : variables) { + LinearExpressionProto* expr = proto->mutable_table()->add_exprs(); + expr->add_vars(var.index_); + expr->add_coeffs(1); } - proto->mutable_table()->set_negated(true); return TableConstraint(proto); } +TableConstraint CpModelBuilder::AddAllowedAssignments( + std::initializer_list expressions) { + ConstraintProto* const proto = cp_model_.add_constraints(); + for (const LinearExpr& expr : expressions) { + *proto->mutable_table()->add_exprs() = LinearExprToProto(expr); + } + return TableConstraint(proto); +} + +TableConstraint CpModelBuilder::AddForbiddenAssignments( + absl::Span expressions) { + TableConstraint ct = AddAllowedAssignments(expressions); + ct.MutableProto()->mutable_table()->set_negated(true); + return ct; +} + +TableConstraint CpModelBuilder::AddForbiddenAssignments( + absl::Span variables) { + TableConstraint ct = AddAllowedAssignments(variables); + ct.MutableProto()->mutable_table()->set_negated(true); + return ct; +} + +TableConstraint CpModelBuilder::AddForbiddenAssignments( + std::initializer_list expressions) { + TableConstraint ct = AddAllowedAssignments(expressions); + ct.MutableProto()->mutable_table()->set_negated(true); + return ct; +} + Constraint CpModelBuilder::AddInverseConstraint( absl::Span variables, absl::Span inverse_variables) { diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h index c948750411..3cffecba2d 100644 --- a/ortools/sat/cp_model.h +++ b/ortools/sat/cp_model.h @@ -899,27 +899,51 @@ class CpModelBuilder { /** * Adds an allowed assignments constraint. * - * An AllowedAssignments constraint is a constraint on an array of variables - * that forces, when all variables are fixed to a single value, that the - * corresponding list of values is equal to one of the tuples added to the - * constraint. + * An AllowedAssignments constraint is a constraint on an array of affine + * expressions (a * var + b) that forces, when all expressions are fixed to a + * single value, that the corresponding list of values is equal to one of the + * tuples added to the constraint. * * It returns a table constraint that allows adding tuples incrementally after * construction. */ - TableConstraint AddAllowedAssignments(absl::Span vars); + TableConstraint AddAllowedAssignments( + absl::Span expressions); + + /** + * Adds an allowed assignments constraint. + */ + TableConstraint AddAllowedAssignments(absl::Span variables); + + /** + * Adds an allowed assignments constraint. + */ + TableConstraint AddAllowedAssignments( + std::initializer_list expressions); /** * Adds an forbidden assignments constraint. * - * A ForbiddenAssignments constraint is a constraint on an array of variables - * where the list of impossible combinations is provided in the tuples added - * to the constraint. + * A ForbiddenAssignments constraint is a constraint on an array of affine + * expressions (a * var + b) where the list of impossible combinations is + * provided in the tuples added to the constraint. * * It returns a table constraint that allows adding tuples incrementally after * construction. */ - TableConstraint AddForbiddenAssignments(absl::Span vars); + TableConstraint AddForbiddenAssignments( + absl::Span expression); + + /** + * Adds an forbidden assignments constraint. + */ + TableConstraint AddForbiddenAssignments(absl::Span variables); + + /** + * Adds an forbidden assignments constraint. + */ + TableConstraint AddForbiddenAssignments( + std::initializer_list expressions); /** An inverse constraint. * diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto index 92e61fac35..f3e5f12ef3 100644 --- a/ortools/sat/cp_model.proto +++ b/ortools/sat/cp_model.proto @@ -247,12 +247,14 @@ message RoutesConstraintProto { int64 capacity = 5; } -// The values of the n-tuple formed by the given variables can only be one of +// The values of the n-tuple formed by the given expression can only be one of // the listed n-tuples in values. The n-tuples are encoded in a flattened way: // [tuple0_v0, tuple0_v1, ..., tuple0_v{n-1}, tuple1_v0, ...]. +// Expressions must be affine (a * var + b). message TableConstraintProto { - repeated int32 vars = 1; + repeated int32 vars = 1; // Legacy field. repeated int64 values = 2; + repeated LinearExpressionProto exprs = 4; // If true, the meaning is "negated", that is we forbid any of the given // tuple from a feasible assignment. diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index 576537f0fb..8b6d3e84e3 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/ortools/sat/cp_model_checker.cc @@ -477,11 +477,21 @@ std::string ValidateElementConstraint(const CpModelProto& model, std::string ValidateTableConstraint(const ConstraintProto& ct) { const TableConstraintProto& arg = ct.table(); - if (arg.vars().empty()) return ""; - if (arg.values().size() % arg.vars().size() != 0) { + if (!arg.vars().empty() && !arg.exprs().empty()) { return absl::StrCat( - "The flat encoding of a table constraint must be a multiple of the " - "number of variable: ", + "Inconsistent table with both legacy and new format defined: ", + ProtobufShortDebugString(ct)); + } + if (arg.vars().empty() && arg.exprs().empty() && !arg.values().empty()) { + return absl::StrCat( + "Inconsistent table empty expressions and non-empty tuples: ", + ProtobufShortDebugString(ct)); + } + const int arity = arg.vars().empty() ? arg.exprs().size() : arg.vars().size(); + if (arg.values().size() % arity != 0) { + return absl::StrCat( + "The flat encoding of a table constraint tuples must be a multiple of " + "the number of expressions: ", ProtobufDebugString(ct)); } return ""; @@ -1451,12 +1461,25 @@ class ConstraintChecker { } bool TableConstraintIsFeasible(const ConstraintProto& ct) { - const int size = ct.table().vars_size(); - if (size == 0) return true; + std::vector solution; + if (ct.table().exprs().empty()) { + for (int i = 0; i < ct.table().vars_size(); ++i) { + solution.push_back(Value(ct.table().vars(i))); + } + } else { + for (int i = 0; i < ct.table().exprs_size(); ++i) { + solution.push_back(LinearExpressionValue(ct.table().exprs(i))); + } + } + + // No expression -> always feasible. + if (solution.empty()) return true; + const int size = solution.size(); + for (int row_start = 0; row_start < ct.table().values_size(); row_start += size) { int i = 0; - while (Value(ct.table().vars(i)) == ct.table().values(row_start + i)) { + while (solution[i] == ct.table().values(row_start + i)) { ++i; if (i == size) return !ct.table().negated(); } diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index cd7efad851..ec93570e43 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/ortools/sat/cp_model_expand.cc @@ -1307,14 +1307,35 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) { ct->Clear(); } +bool TableIsInCanonicalForm(ConstraintProto* ct) { + TableConstraintProto& table = *ct->mutable_table(); + if (!table.vars().empty()) { + LOG(ERROR) << "Table is in the legacy format."; + return false; + } + for (const LinearExpressionProto& expr : table.exprs()) { + if (expr.offset() != 0) { + LOG(ERROR) << "Expression contains an non-zero offset."; + return false; + } + if (expr.coeffs().size() == 1 && expr.coeffs(0) != 1) { + LOG(ERROR) << "Expression contains a single variable with a coefficient " + "different from 1."; + return false; + } + } + return true; +} + void ExpandNegativeTable(ConstraintProto* ct, PresolveContext* context) { + DCHECK(TableIsInCanonicalForm(ct)); TableConstraintProto& table = *ct->mutable_table(); - const int num_vars = table.vars_size(); - const int num_original_tuples = table.values_size() / num_vars; + const int num_exprs = table.exprs_size(); + const int num_original_tuples = table.values_size() / num_exprs; std::vector> tuples(num_original_tuples); int count = 0; for (int i = 0; i < num_original_tuples; ++i) { - for (int j = 0; j < num_vars; ++j) { + for (int j = 0; j < num_exprs; ++j) { tuples[i].push_back(table.values(count++)); } } @@ -1327,8 +1348,8 @@ void ExpandNegativeTable(ConstraintProto* ct, PresolveContext* context) { // Compress tuples. std::vector domain_sizes; - for (int i = 0; i < num_vars; ++i) { - domain_sizes.push_back(context->DomainOf(table.vars(i)).Size()); + for (int i = 0; i < num_exprs; ++i) { + domain_sizes.push_back(context->DomainOf(table.exprs(i).vars(0)).Size()); } CompressTuples(domain_sizes, &tuples); @@ -1336,12 +1357,12 @@ void ExpandNegativeTable(ConstraintProto* ct, PresolveContext* context) { std::vector clause; for (const std::vector& tuple : tuples) { clause.clear(); - for (int i = 0; i < num_vars; ++i) { + for (int i = 0; i < num_exprs; ++i) { const int64_t value = tuple[i]; if (value == kTableAnyValue) continue; const int literal = - context->GetOrCreateVarValueEncoding(table.vars(i), value); + context->GetOrCreateVarValueEncoding(table.exprs(i).vars(0), value); clause.push_back(NegatedRef(literal)); } @@ -1853,27 +1874,32 @@ void CompressAndExpandPositiveTable(ConstraintProto* ct, // TODO(user): investigate different encoding for prefix tables. Maybe // we can remove the need to create tuple literals. void ExpandPositiveTable(ConstraintProto* ct, PresolveContext* context) { + DCHECK(TableIsInCanonicalForm(ct)); const TableConstraintProto& table = ct->table(); - const int num_vars = table.vars_size(); - const int num_original_tuples = table.values_size() / num_vars; + const int num_exprs = table.exprs_size(); + const int num_original_tuples = table.values_size() / num_exprs; // Read tuples flat array and recreate the vector of tuples. - std::vector vars(table.vars().begin(), table.vars().end()); + std::vector vars; + vars.reserve(table.exprs_size()); + for (const LinearExpressionProto& expr : table.exprs()) { + vars.push_back(expr.vars(0)); + } std::vector> tuples(num_original_tuples); int count = 0; for (int tuple_index = 0; tuple_index < num_original_tuples; ++tuple_index) { - for (int var_index = 0; var_index < num_vars; ++var_index) { + for (int var_index = 0; var_index < num_exprs; ++var_index) { tuples[tuple_index].push_back(table.values(count++)); } } // Compute the set of possible values for each variable (from the table). // Remove invalid tuples along the way. - std::vector> values_per_var(num_vars); + std::vector> values_per_var(num_exprs); int new_size = 0; for (int tuple_index = 0; tuple_index < num_original_tuples; ++tuple_index) { bool keep = true; - for (int var_index = 0; var_index < num_vars; ++var_index) { + for (int var_index = 0; var_index < num_exprs; ++var_index) { const int64_t value = tuples[tuple_index][var_index]; if (!context->DomainContains(vars[var_index], value)) { keep = false; @@ -1881,7 +1907,7 @@ void ExpandPositiveTable(ConstraintProto* ct, PresolveContext* context) { } } if (keep) { - for (int var_index = 0; var_index < num_vars; ++var_index) { + for (int var_index = 0; var_index < num_exprs; ++var_index) { values_per_var[var_index].insert(tuples[tuple_index][var_index]); } std::swap(tuples[tuple_index], tuples[new_size]); @@ -1911,7 +1937,7 @@ void ExpandPositiveTable(ConstraintProto* ct, PresolveContext* context) { // Also counts the number of fixed variables. if (ct->enforcement_literal().empty()) { int num_fixed_variables = 0; - for (int var_index = 0; var_index < num_vars; ++var_index) { + for (int var_index = 0; var_index < num_exprs; ++var_index) { CHECK(context->IntersectDomainWith( vars[var_index], Domain::FromValues({values_per_var[var_index].begin(), @@ -1921,11 +1947,11 @@ void ExpandPositiveTable(ConstraintProto* ct, PresolveContext* context) { } } - if (num_fixed_variables == num_vars - 1) { + if (num_fixed_variables == num_exprs - 1) { context->UpdateRuleStats("table: one variable not fixed"); ct->Clear(); return; - } else if (num_fixed_variables == num_vars) { + } else if (num_fixed_variables == num_exprs) { context->UpdateRuleStats("table: all variables fixed"); ct->Clear(); return; @@ -1937,7 +1963,7 @@ void ExpandPositiveTable(ConstraintProto* ct, PresolveContext* context) { // TODO(user): If there is an unique variable with cost, it is better to // detect it. But if the detection fail, we should still call // AddSizeTwoTable() unlike what happen here. - if (num_vars == 2 && !context->params().detect_table_with_cost() && + if (num_exprs == 2 && !context->params().detect_table_with_cost() && ct->enforcement_literal().empty()) { AddSizeTwoTable(vars, tuples, values_per_var, context); context->UpdateRuleStats( @@ -2531,6 +2557,9 @@ void ExpandCpModel(PresolveContext* context) { ExpandAutomaton(ct, context); break; case ConstraintProto::kTable: + if (!context->params().cp_model_presolve()) { + CanonicalizeTable(context, ct); + } if (ct->table().negated()) { ExpandNegativeTable(ct, context); } else { diff --git a/ortools/sat/cp_model_expand_test.cc b/ortools/sat/cp_model_expand_test.cc index b3b12dfad9..95fedc4702 100644 --- a/ortools/sat/cp_model_expand_test.cc +++ b/ortools/sat/cp_model_expand_test.cc @@ -910,9 +910,30 @@ TEST(ExpandTableTest, EnumerationAndEncoding) { variables { domain: [ 0, 4 ] } variables { domain: [ 0, 4 ] } variables { domain: [ 0, 4 ] } - constraints { table { vars: 0 vars: 2 values: 0 values: 1 } } - constraints { table { vars: 1 vars: 3 values: 4 values: 0 } } - constraints { table { vars: 2 vars: 1 values: 1 values: 4 } } + constraints { + table { + exprs { vars: 0 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } + values: 0 + values: 1 + } + } + constraints { + table { + exprs { vars: 1 coeffs: 1 } + exprs { vars: 3 coeffs: 1 } + values: 4 + values: 0 + } + } + constraints { + table { + exprs { vars: 2 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + values: 1 + values: 4 + } + } )pb"); Model model; @@ -943,7 +964,8 @@ TEST(ExpandTableTest, EnumerationAndEncodingTwoVars) { } constraints { table { - vars: [ 0, 1 ] + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } values: [ 0, 0, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 4 ] } } @@ -969,7 +991,9 @@ TEST(ExpandTableTest, EnumerationAndEncodingFullPrefix) { variables { domain: [ 0, 2 ] } constraints { table { - vars: [ 0, 1, 2 ] + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } values: [ 0, 0, 0, 0, 1, 1, 0, 2, 2, 1, 0, 1, 1, 1, 2, 1, 2, 0, 2, 0, 2, 2, 1, 0, 2, 2, 1 @@ -999,7 +1023,9 @@ TEST(ExpandTableTest, EnumerationAndEncodingPartialPrefix) { variables { domain: [ 0, 2 ] } constraints { table { - vars: [ 0, 1, 2 ] + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } values: [ 0, 0, 0, 0, 2, 2, 1, 0, 1, 1, 1, 2, 1, 2, 0, 2, 0, 2, 2, 1, 0 ] @@ -1028,7 +1054,9 @@ TEST(ExpandTableTest, EnumerationAndEncodingInvalidTuples) { variables { domain: [ 0, 2 ] } constraints { table { - vars: [ 0, 1, 2 ] + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } values: [ 0, 0, 4, 0, 2, 2, 1, 0, 1, 1, 1, 2, 1, 2, 0, 2, 0, 2, 2, 1, 4 ] @@ -1059,7 +1087,9 @@ TEST(ExpandTableTest, EnumerationAndEncodingOneTupleWithAny) { variables { domain: [ 0, 3 ] } constraints { table { - vars: [ 0, 1, 2 ] + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } values: [ 1, 0, 2, 1, 1, 2, 1, 2, 2 ] } } @@ -1087,7 +1117,9 @@ TEST(ExpandTableTest, EnumerationAndEncodingPrefixWithLargeNegatedPart) { variables { domain: [ 0, 5 ] } constraints { table { - vars: [ 0, 1, 2 ] + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } values: [ 0, 0, 0, 1, 1, 1, 2, 2, 2, 3, 3, 3, 4, 4, 4, 5, 5, 5 ] } } @@ -1117,7 +1149,9 @@ TEST(ExpandTableTest, EnforcedPositiveTable) { constraints { enforcement_literal: [ 3 ] table { - vars: [ 0, 1, 2 ] + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } values: [ 1, 2, 3, 2, 2, 2, 3, 2, 1 ] } } @@ -1147,7 +1181,9 @@ TEST(ExpandTableTest, EnforcedPositiveEmptyTable) { constraints { enforcement_literal: [ 3 ] table { - vars: [ 0, 1, 2 ] + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } values: [] } } @@ -1178,7 +1214,9 @@ TEST(ExpandTableTest, DualEnforcedPositiveTable) { constraints { enforcement_literal: [ 3, 4 ] table { - vars: [ 0, 1, 2 ] + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } values: [ 1, 2, 3, 2, 2, 2, 3, 2, 1 ] } } @@ -1207,7 +1245,9 @@ TEST(ExpandTableTest, EnforcedNegativeTable) { constraints { enforcement_literal: [ 3 ] table { - vars: [ 0, 1, 2 ] + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } values: [ 1, 2, 3, 2, 2, 2, 3, 2, 1 ] negated: true } @@ -1247,7 +1287,7 @@ TEST(ExpandTableTest, UnsatNegatedTable) { variables { domain: [ 0, 1 ] } constraints { table { - vars: 0 + exprs { vars: 0 coeffs: 1 } values: [ 0, 1 ] negated: true } diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 7911fd59b8..4080d435f1 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -1594,8 +1594,8 @@ bool CpModelPresolver::PresolveIntProd(ConstraintProto* ct) { // Reduce coefficients. const int64_t gcd = - MathUtil::GCD64(static_cast(std::abs(constant_factor)), - static_cast(std::abs(target_divisor))); + std::gcd(static_cast(std::abs(constant_factor)), + static_cast(std::abs(target_divisor))); if (gcd != 1) { constant_factor /= gcd; DivideLinearExpression(gcd, target); @@ -2133,7 +2133,7 @@ bool CpModelPresolver::DivideLinearByGcd(ConstraintProto* ct) { const int num_vars = ct->linear().vars().size(); for (int i = 0; i < num_vars; ++i) { const int64_t magnitude = std::abs(ct->linear().coeffs(i)); - gcd = MathUtil::GCD64(gcd, magnitude); + gcd = std::gcd(gcd, magnitude); if (gcd == 1) break; } if (gcd > 1) { @@ -2470,7 +2470,7 @@ bool CpModelPresolver::AddVarAffineRepresentativeFromLinearEquality( for (int i = 0; i < num_variables; ++i) { if (i == target_index) continue; const int64_t magnitude = std::abs(ct->linear().coeffs(i)); - gcd = MathUtil::GCD64(gcd, magnitude); + gcd = std::gcd(gcd, magnitude); if (gcd == 1) return false; } @@ -3173,7 +3173,7 @@ void CpModelPresolver::TryToReduceCoefficientsOfLinearConstraint( rd_divisors_.clear(); for (int i = 0; i < rd_entries_.size(); ++i) { const RdEntry& e = rd_entries_[i]; - gcd = MathUtil::GCD64(gcd, e.magnitude); + gcd = std::gcd(gcd, e.magnitude); max_error -= e.max_variation; // We regroup all term with the same coefficient into one. @@ -4366,8 +4366,9 @@ void CpModelPresolver::ExtractEnforcementLiteralFromLinearConstraint( // TODO(user): If 2 * min_coeff_magnitude >= bound, then the constraint can // be completely rewriten to 2 * (enforcement_part) + sum var >= 2 which is // what happen eventually when bound is even, but not if it is odd currently. - int64_t second_threshold = std::max(CeilOfRatio(threshold, int64_t{2}), - threshold - min_coeff_magnitude); + int64_t second_threshold = + std::max(MathUtil::CeilOfRatio(threshold, int64_t{2}), + threshold - min_coeff_magnitude); // Tricky: The second threshold only work if the domain is simple. If the // domain has holes, changing the coefficient might change whether the @@ -5131,170 +5132,99 @@ bool CpModelPresolver::PresolveElement(int c, ConstraintProto* ct) { bool CpModelPresolver::PresolveTable(ConstraintProto* ct) { if (context_->ModelIsUnsat()) return false; - if (ct->table().vars().empty()) { - context_->UpdateRuleStats("table: empty constraint"); - return MarkConstraintAsFalse(ct); + + bool changed = false; + for (int i = 0; i < ct->table().exprs_size(); ++i) { + changed |= CanonicalizeLinearExpression( + *ct, ct->mutable_table()->mutable_exprs(i)); } - const int initial_num_vars = ct->table().vars_size(); - bool changed = true; + const int initial_num_exprs = ct->table().exprs_size(); + if (initial_num_exprs > 0) CanonicalizeTable(context_, ct); + changed |= (ct->table().exprs_size() != initial_num_exprs); - // Query existing affine relations. - std::vector affine_relations; - std::vector old_var_lb; - std::vector old_var_ub; - { - for (int v = 0; v < initial_num_vars; ++v) { - const int ref = ct->table().vars(v); - AffineRelation::Relation r = context_->GetAffineRelation(ref); - affine_relations.push_back(r); - old_var_lb.push_back(context_->MinOf(ref)); - old_var_ub.push_back(context_->MaxOf(ref)); - if (r.representative != ref) { - changed = true; - ct->mutable_table()->set_vars(v, r.representative); - context_->UpdateRuleStats( - "table: replace variable by canonical affine one"); - } - } + if (ct->table().exprs().empty()) { + context_->UpdateRuleStats("table: no expressions"); + return RemoveConstraint(ct); } - // Check for duplicate occurrences of variables. - // If the ith index is -1, then the variable is not a duplicate of a smaller - // index variable. It if is != from -1, then the values stored is the new - // index of the first occurrence of the variable. - std::vector old_index_of_duplicate_to_new_index_of_first_occurrence( - initial_num_vars, -1); - // If == -1, then the variable is a duplicate of a smaller index variable. - std::vector old_index_to_new_index(initial_num_vars, -1); - int num_vars = 0; - { - absl::flat_hash_map first_visit; - for (int p = 0; p < initial_num_vars; ++p) { - const int ref = ct->table().vars(p); - const int var = PositiveRef(ref); - const auto& it = first_visit.find(var); - if (it != first_visit.end()) { - const int previous = it->second; - old_index_of_duplicate_to_new_index_of_first_occurrence[p] = previous; - context_->UpdateRuleStats("table: duplicate variables"); - changed = true; - } else { - ct->mutable_table()->set_vars(num_vars, ref); - first_visit[var] = num_vars; - old_index_to_new_index[p] = num_vars; - num_vars++; - } - } - - if (num_vars < initial_num_vars) { - ct->mutable_table()->mutable_vars()->Truncate(num_vars); + if (ct->table().values().empty()) { + if (ct->table().negated()) { + context_->UpdateRuleStats("table: negative table without tuples"); + return RemoveConstraint(ct); + } else { + context_->UpdateRuleStats("table: positive table without tuplest"); + return MarkConstraintAsFalse(ct); } } - // Check each tuple for validity w.r.t. affine relations, variable domains, - // and consistency with duplicate variables. Reduce the size of the tuple in - // case of duplicate variables. - std::vector> new_tuples; - const int initial_num_tuples = ct->table().values_size() / initial_num_vars; - std::vector> new_domains(num_vars); - - { - std::vector tuple(num_vars); - new_tuples.reserve(initial_num_tuples); - for (int i = 0; i < initial_num_tuples; ++i) { - bool delete_row = false; - std::string tmp; - for (int j = 0; j < initial_num_vars; ++j) { - const int64_t old_value = ct->table().values(i * initial_num_vars + j); - - // Corner case to avoid overflow, assuming the domain where already - // propagated between a variable and its affine representative. - if (old_value < old_var_lb[j] || old_value > old_var_ub[j]) { - delete_row = true; - break; - } - - // Affine relations are defined on the initial variables. - const AffineRelation::Relation& r = affine_relations[j]; - const int64_t value = (old_value - r.offset) / r.coeff; - if (value * r.coeff + r.offset != old_value) { - // Value not reachable by affine relation. - delete_row = true; - break; - } - const int mapped_position = old_index_to_new_index[j]; - if (mapped_position == -1) { // The current variable is duplicate. - const int new_index_of_first_occurrence = - old_index_of_duplicate_to_new_index_of_first_occurrence[j]; - if (value != tuple[new_index_of_first_occurrence]) { - delete_row = true; - break; - } - } else { - const int ref = ct->table().vars(mapped_position); - if (!context_->DomainContains(ref, value)) { - delete_row = true; - break; - } - tuple[mapped_position] = value; - } - } - if (delete_row) { - changed = true; - continue; - } - new_tuples.push_back(tuple); - for (int j = 0; j < num_vars; ++j) { - new_domains[j].insert(tuple[j]); - } - } - gtl::STLSortAndRemoveDuplicates(&new_tuples); - if (new_tuples.size() < initial_num_tuples) { - context_->UpdateRuleStats("table: removed rows"); + int num_fixed_exprs = 0; + for (const LinearExpressionProto& expr : ct->table().exprs()) { + if (context_->IsFixed(expr)) ++num_fixed_exprs; + } + if (num_fixed_exprs == ct->table().exprs_size()) { + context_->UpdateRuleStats("table: all expressions are fixed"); + DCHECK_LE(ct->table().values_size(), num_fixed_exprs); + if (ct->table().negated() == ct->table().values().empty()) { + context_->UpdateRuleStats("table: always true"); + return RemoveConstraint(ct); + } else { + context_->UpdateRuleStats("table: always false"); + return MarkConstraintAsFalse(ct); } + return RemoveConstraint(ct); } - // Update the list of tuples if needed. - if (changed) { - ct->mutable_table()->clear_values(); - for (const std::vector& t : new_tuples) { - for (const int64_t v : t) { - ct->mutable_table()->add_values(v); - } - } + if (num_fixed_exprs > 0) { + RemoveFixedColumnsFromTable(context_, ct); } // Nothing more to do for negated tables. if (ct->table().negated()) return changed; // And for constraints with enforcement literals. - if (HasEnforcementLiteral(*ct)) return false; + if (HasEnforcementLiteral(*ct)) return changed; + + // Filter the variables domains. + const int num_exprs = ct->table().exprs_size(); + const int num_tuples = ct->table().values_size() / num_exprs; + std::vector> new_domains(num_exprs); + for (int e = 0; e < num_exprs; ++e) { + const LinearExpressionProto& expr = ct->table().exprs(e); + if (context_->IsFixed(expr)) { + new_domains[e].push_back(context_->FixedValue(expr)); + continue; + } - // Filter the variable domains. - for (int j = 0; j < num_vars; ++j) { - const int ref = ct->table().vars(j); - if (!context_->IntersectDomainWith( - PositiveRef(ref), - Domain::FromValues(std::vector(new_domains[j].begin(), - new_domains[j].end())), - &changed)) { + for (int t = 0; t < num_tuples; ++t) { + new_domains[e].push_back(ct->table().values(t * num_exprs + e)); + } + gtl::STLSortAndRemoveDuplicates(&new_domains[e]); + DCHECK_EQ(1, expr.vars_size()); + DCHECK_EQ(1, expr.coeffs(0)); + DCHECK_EQ(0, expr.offset()); + const int var = expr.vars(0); + bool domain_modified = false; + if (!context_->IntersectDomainWith(var, Domain::FromValues(new_domains[e]), + &domain_modified)) { return true; } + if (domain_modified) { + context_->UpdateRuleStats("table: reduce variable domain"); + } } - if (changed) { - context_->UpdateRuleStats("table: reduced variable domains"); - } - if (num_vars == 1) { - // Now that we properly update the domain, we can remove the constraint. + + if (num_exprs == 1) { + // Now that we have properly updated the domain, we can remove the + // constraint. context_->UpdateRuleStats("table: only one column!"); return RemoveConstraint(ct); } // Check that the table is not complete or just here to exclude a few tuples. double prod = 1.0; - for (int j = 0; j < num_vars; ++j) prod *= new_domains[j].size(); - if (prod == new_tuples.size()) { + for (int e = 0; e < num_exprs; ++e) prod *= new_domains[e].size(); + if (prod == static_cast(num_tuples)) { context_->UpdateRuleStats("table: all tuples!"); return RemoveConstraint(ct); } @@ -5302,17 +5232,25 @@ bool CpModelPresolver::PresolveTable(ConstraintProto* ct) { // Convert to the negated table if we gain a lot of entries by doing so. // Note however that currently the negated table do not propagate as much as // it could. - if (new_tuples.size() > 0.7 * prod) { - // Enumerate all tuples. - std::vector> var_to_values(num_vars); - for (int j = 0; j < num_vars; ++j) { - var_to_values[j].assign(new_domains[j].begin(), new_domains[j].end()); + if (static_cast(num_tuples) > 0.7 * prod) { + std::vector> current_tuples(num_tuples); + for (int t = 0; t < num_tuples; ++t) { + current_tuples[t].resize(num_exprs); + for (int e = 0; e < num_exprs; ++e) { + current_tuples[t][e] = ct->table().values(t * num_exprs + e); + } + } + + // Enumerate all possible tuples. + std::vector> var_to_values(num_exprs); + for (int e = 0; e < num_exprs; ++e) { + var_to_values[e].assign(new_domains[e].begin(), new_domains[e].end()); } std::vector> all_tuples(prod); for (int i = 0; i < prod; ++i) { - all_tuples[i].resize(num_vars); + all_tuples[i].resize(num_exprs); int index = i; - for (int j = 0; j < num_vars; ++j) { + for (int j = 0; j < num_exprs; ++j) { all_tuples[i][j] = var_to_values[j][index % var_to_values[j].size()]; index /= var_to_values[j].size(); } @@ -5320,9 +5258,10 @@ bool CpModelPresolver::PresolveTable(ConstraintProto* ct) { gtl::STLSortAndRemoveDuplicates(&all_tuples); // Compute the complement of new_tuples. - std::vector> diff(prod - new_tuples.size()); + std::vector> diff(prod - num_tuples); std::set_difference(all_tuples.begin(), all_tuples.end(), - new_tuples.begin(), new_tuples.end(), diff.begin()); + current_tuples.begin(), current_tuples.end(), + diff.begin()); // Negate the constraint. ct->mutable_table()->set_negated(!ct->table().negated()); @@ -5332,6 +5271,7 @@ bool CpModelPresolver::PresolveTable(ConstraintProto* ct) { } context_->UpdateRuleStats("table: negated"); } + return changed; } @@ -6344,7 +6284,7 @@ bool CpModelPresolver::PresolveCumulative(ConstraintProto* ct) { gcd = 1; break; } - gcd = MathUtil::GCD64(gcd, context_->MinOf(demand_expr)); + gcd = std::gcd(gcd, context_->MinOf(demand_expr)); if (gcd == 1) break; } if (gcd > 1) { @@ -6906,7 +6846,7 @@ bool CpModelPresolver::PresolveReservoir(ConstraintProto* ct) { int64_t min_sum_of_negative_level_changes = 0; for (int i = 0; i < num_events; ++i) { const int64_t demand = context_->FixedValue(proto.level_changes(i)); - gcd = MathUtil::GCD64(gcd, std::abs(demand)); + gcd = std::gcd(gcd, std::abs(demand)); if (demand > 0) { num_positives++; max_sum_of_positive_level_changes += demand; @@ -11200,7 +11140,7 @@ void CpModelPresolver::MaybeTransferLinear1ToAnotherVariable(int var) { context_->UpdateRuleStats("linear1: transferred from abs(X) to X"); const LinearExpressionProto& target = other_ct.lin_max().target(); const LinearExpressionProto& expr = other_ct.lin_max().exprs(0); - transfer_f = [target, expr](const Domain& implied) { + transfer_f = [target = target, expr = expr](const Domain& implied) { Domain target_domain = implied.ContinuousMultiplicationBy(target.coeffs(0)) .AdditionWith(Domain(target.offset())); @@ -11604,7 +11544,7 @@ void CpModelPresolver::TryToSimplifyDomain(int var) { const int64_t shifted_value = i.start - var_min; DCHECK_GT(shifted_value, 0); - gcd = MathUtil::GCD64(gcd, shifted_value); + gcd = std::gcd(gcd, shifted_value); if (gcd == 1) break; } if (gcd == 1) return; @@ -12050,6 +11990,9 @@ bool ModelCopy::ImportAndSimplifyConstraints( case ConstraintProto::kElement: if (!CopyElement(ct)) return CreateUnsatModel(c, ct); break; + case ConstraintProto::kTable: + if (!CopyTable(ct)) return CreateUnsatModel(c, ct); + break; case ConstraintProto::kAtMostOne: if (!CopyAtMostOne(ct)) return CreateUnsatModel(c, ct); break; @@ -12443,6 +12386,34 @@ bool ModelCopy::CopyElement(const ConstraintProto& ct) { return true; } +bool ModelCopy::CopyTable(const ConstraintProto& ct) { + ConstraintProto* new_ct = context_->working_model->add_constraints(); + if (ct.table().vars().empty() && !ct.table().exprs().empty()) { + // New format, just copy. + *new_ct = ct; + return true; + } + + auto fill_expr = [this](int var, LinearExpressionProto* expr) mutable { + if (context_->IsFixed(var)) { + expr->set_offset(context_->FixedValue(var)); + } else { + DCHECK(RefIsPositive(var)); + expr->mutable_vars()->Reserve(1); + expr->mutable_coeffs()->Reserve(1); + expr->add_vars(var); + expr->add_coeffs(1); + } + }; + + for (const int var : ct.table().vars()) { + fill_expr(var, new_ct->mutable_table()->add_exprs()); + } + *new_ct->mutable_table()->mutable_values() = ct.table().values(); + + return true; +} + bool ModelCopy::CopyAtMostOne(const ConstraintProto& ct) { int num_true = 0; temp_literals_.clear(); diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h index 47926f7acf..1b1148c8d9 100644 --- a/ortools/sat/cp_model_presolve.h +++ b/ortools/sat/cp_model_presolve.h @@ -428,14 +428,16 @@ class ModelCopy { bool CopyBoolAnd(const ConstraintProto& ct); bool CopyBoolAndWithDupSupport(const ConstraintProto& ct); - bool CopyLinearExpression(const LinearExpressionProto& expr, - LinearExpressionProto* dst); - bool CopyIntProd(const ConstraintProto& ct, bool ignore_names); - bool CopyLinear(const ConstraintProto& ct); - bool CopyElement(const ConstraintProto& ct); bool CopyAtMostOne(const ConstraintProto& ct); bool CopyExactlyOne(const ConstraintProto& ct); + bool CopyElement(const ConstraintProto& ct); + bool CopyIntProd(const ConstraintProto& ct, bool ignore_names); + bool CopyLinear(const ConstraintProto& ct); + bool CopyLinearExpression(const LinearExpressionProto& expr, + LinearExpressionProto* dst); + bool CopyTable(const ConstraintProto& ct); + // If we "copy" an interval for a first time, we make sure to create the // linear constraint between the start, size and end. This allow to simplify // the input proto and client side code. diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 0b7b448599..525af6ea60 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -787,7 +787,13 @@ std::vector GetFullWorkerParameters( names.push_back("fixed"); names.push_back("core"); names.push_back("no_lp"); - names.push_back("max_lp_sym"); + if (cp_model.has_symmetry()) { + names.push_back("max_lp_sym"); + } else { + // If there is no symmetry, max_lp_sym and max_lp are the same, but + // we prefer the less confusing name. + names.push_back("max_lp"); + } names.push_back("quick_restart"); names.push_back("reduced_costs"); names.push_back("quick_restart_no_lp"); @@ -801,7 +807,9 @@ std::vector GetFullWorkerParameters( names.push_back("probing_no_lp"); names.push_back("objective_lb_search_no_lp"); names.push_back("objective_lb_search_max_lp"); - names.push_back("max_lp"); + if (cp_model.has_symmetry()) { + names.push_back("max_lp"); + } } else { for (const std::string& name : base_params.subsolvers()) { // Hack for flatzinc. At the time of parameter setting, the objective is diff --git a/ortools/sat/cp_model_symmetries.cc b/ortools/sat/cp_model_symmetries.cc index 59d02fb2e7..7713293410 100644 --- a/ortools/sat/cp_model_symmetries.cc +++ b/ortools/sat/cp_model_symmetries.cc @@ -771,7 +771,8 @@ void DetectAndAddSymmetryToProto(const SatParameters& params, std::vector> generators; FindCpModelSymmetries(params, *proto, &generators, - /*deterministic_limit=*/1.0, logger); + params.symmetry_detection_deterministic_time_limit(), + logger); if (generators.empty()) { proto->clear_symmetry(); return; @@ -1006,8 +1007,10 @@ bool DetectAndExploitSymmetriesInPresolve(PresolveContext* context) { } std::vector> generators; - FindCpModelSymmetries(params, proto, &generators, - /*deterministic_limit=*/1.0, context->logger()); + FindCpModelSymmetries( + params, proto, &generators, + context->params().symmetry_detection_deterministic_time_limit(), + context->logger()); // Remove temporary affine relation. context->working_model->mutable_constraints()->DeleteSubrange( @@ -1042,10 +1045,12 @@ bool DetectAndExploitSymmetriesInPresolve(PresolveContext* context) { const std::vector orbits = GetOrbits(num_vars, generators); std::vector orbit_sizes; int max_orbit_size = 0; + int sum_of_orbit_sizes = 0; for (int var = 0; var < num_vars; ++var) { const int rep = orbits[var]; if (rep == -1) continue; if (rep >= orbit_sizes.size()) orbit_sizes.resize(rep + 1, 0); + ++sum_of_orbit_sizes; orbit_sizes[rep]++; if (orbit_sizes[rep] > max_orbit_size) { distinguished_var = var; @@ -1135,17 +1140,6 @@ bool DetectAndExploitSymmetriesInPresolve(PresolveContext* context) { } } - // Fixing just a few variables to break large symmetry can be really bad. - // See for example cdc7-4-3-2.pb.gz where we don't find solution if we do - // that. Especially with max_lp_sym worker. - // - // TODO(user): investigate/tune more. This is worse on - // neos-3083784-nive.pb.gz. It must depends on how much we fix compared to how - // much symmetry we break. - if (10 * can_be_fixed_to_false.size() < max_orbit_size) { - can_be_fixed_to_false.clear(); - } - // Orbitope approach. // // This is basically the same as the generic approach, but because of the @@ -1225,6 +1219,29 @@ bool DetectAndExploitSymmetriesInPresolve(PresolveContext* context) { --size_left; } } + + // Fixing just a few variables to break large symmetry can be really bad. See + // for example cdc7-4-3-2.pb.gz where we don't find solution if we do that. On + // the other hand, enabling this make it worse on neos-3083784-nive.pb.gz. + // + // In general, enabling this works better in single thread with max_lp_sym, + // but worse in multi-thread, where less workers are using symmetries, and so + // it is better to fix more stuff. + // + // TODO(user): Tune more, especially as we handle symmetry better. Also the + // estimate is pretty bad, we should probably compute stabilizer and decide + // when we actually know how much we can fix compared to how many symmetry we + // lose. + const int num_fixable = + std::max(max_num_fixed_in_orbitope, can_be_fixed_to_false.size()); + if (/* DISABLES CODE */ (false) && !can_be_fixed_to_false.empty() && + 100 * num_fixable < sum_of_orbit_sizes) { + SOLVER_LOG(context->logger(), + "[Symmetry] Not fixing anything as gain seems too small."); + return true; + } + + // Fix "can_be_fixed_to_false" instead of the orbitope if it is larger. if (max_num_fixed_in_orbitope < can_be_fixed_to_false.size()) { const int orbit_index = orbits[distinguished_var]; int num_in_orbit = 0; diff --git a/ortools/sat/cp_model_symmetries.h b/ortools/sat/cp_model_symmetries.h index 68b6610af8..6b944334eb 100644 --- a/ortools/sat/cp_model_symmetries.h +++ b/ortools/sat/cp_model_symmetries.h @@ -55,6 +55,15 @@ void DetectAndAddSymmetryToProto(const SatParameters& params, // // Currently this just try to fix variables by detecting symmetries between // Booleans in bool_and, at_most_one or exactly_one constraints. +// +// TODO(user): A bunch of other presolve transformations break the symmetry even +// though they probably shouldn't. Like the find big liner overlap for instance. +// Or when we fix variable but don't propagate to the full orbit. It might not +// be too much work to: +// 1/ Compute the symmetry early +// 2/ Only do transformation that preserve them +// To investigate. It seems disabling find_big_linear_overlap helps on +// mas74.pb.gz, or the square??.mps for instance. But it is less good overall. bool DetectAndExploitSymmetriesInPresolve(PresolveContext* context); } // namespace sat diff --git a/ortools/sat/cp_model_utils.cc b/ortools/sat/cp_model_utils.cc index 6cd32ca6f7..cdfee30103 100644 --- a/ortools/sat/cp_model_utils.cc +++ b/ortools/sat/cp_model_utils.cc @@ -178,7 +178,13 @@ void GetReferencesUsedByConstraint(const ConstraintProto& ct, AddIndices(ct.reservoir().active_literals(), literals); break; case ConstraintProto::ConstraintCase::kTable: - AddIndices(ct.table().vars(), variables); + if (!ct.table().vars().empty()) { + AddIndices(ct.table().vars(), variables); + } else { + for (const LinearExpressionProto& expr : ct.table().exprs()) { + AddIndices(expr.vars(), variables); + } + } break; case ConstraintProto::ConstraintCase::kAutomaton: AddIndices(ct.automaton().vars(), variables); @@ -359,7 +365,13 @@ void ApplyToAllVariableIndices(const std::function& f, } break; case ConstraintProto::ConstraintCase::kTable: - APPLY_TO_REPEATED_FIELD(table, vars); + if (!ct->table().vars().empty()) { + APPLY_TO_REPEATED_FIELD(table, vars); + } else { + for (int i = 0; i < ct->table().exprs_size(); ++i) { + APPLY_TO_REPEATED_FIELD(table, exprs(i)->mutable_vars); + } + } break; case ConstraintProto::ConstraintCase::kAutomaton: APPLY_TO_REPEATED_FIELD(automaton, vars); @@ -764,7 +776,13 @@ uint64_t FingerprintModel(const CpModelProto& model, uint64_t seed) { } break; case ConstraintProto::ConstraintCase::kTable: - fp = FingerprintRepeatedField(ct.table().vars(), fp); + if (!ct.table().vars().empty()) { + fp = FingerprintRepeatedField(ct.table().vars(), fp); + } else { + for (const LinearExpressionProto& expr : ct.table().exprs()) { + fp = FingerprintExpression(expr, fp); + } + } fp = FingerprintRepeatedField(ct.table().values(), fp); fp = FingerprintSingleField(ct.table().negated(), fp); break; diff --git a/ortools/sat/csharp/CpModel.cs b/ortools/sat/csharp/CpModel.cs index f7f92dc10d..fb52881249 100644 --- a/ortools/sat/csharp/CpModel.cs +++ b/ortools/sat/csharp/CpModel.cs @@ -329,28 +329,29 @@ public MultipleCircuitConstraint AddMultipleCircuit() return ct; } - /** - *

- * Adds AllowedAssignments(variables). - * - * - * An AllowedAssignments constraint is a constraint on an array of variables that forces, when - * all variables are fixed to a single value, that the corresponding list of values is equal to - * one of the tuples of the tupleList. - * - * - * a list of variables - * an instance of the TableConstraint class without any tuples. Tuples can be added - * directly to the table constraint - * - */ - public TableConstraint AddAllowedAssignments(IEnumerable vars) + /** + * + * Adds AllowedAssignments(expressions). + * + * + * An AllowedAssignments constraint is a constraint on an array of affine + * expressions (a * var + b) that forces, when all expressions are fixed to a single + * value, that the corresponding list of values is equal to one of the tuples of the + * tupleList. + * + * + * a list of affine expressions (a * var + b) + * an instance of the TableConstraint class without any tuples. Tuples can be added + * directly to the table constraint + * + */ + public TableConstraint AddAllowedAssignments(IEnumerable exprs) { TableConstraintProto table = new TableConstraintProto(); - table.Vars.TrySetCapacity(vars); - foreach (IntVar var in vars) + table.Vars.TrySetCapacity(exprs); + foreach (LinearExpr expr in exprs) { - table.Vars.Add(var.Index); + table.Exprs.Add(GetLinearExpressionProto(expr)); } TableConstraint ct = new TableConstraint(model_); @@ -363,18 +364,19 @@ public TableConstraint AddAllowedAssignments(IEnumerable vars) * Adds ForbiddenAssignments(variables). * * - * A ForbiddenAssignments constraint is a constraint on an array of variables where the list of - * impossible combinations is provided in the tuples list. + * A ForbiddenAssignments constraint is a constraint on an array of affine + * expressions (a * var + b) where the list of impossible combinations is provided + * in the tuples list. * * - * a list of variables + * a list of affine expressions (a * var + b) * an instance of the TableConstraint class without any tuples. Tuples can be added * directly to the table constraint * */ - public TableConstraint AddForbiddenAssignments(IEnumerable vars) + public TableConstraint AddForbiddenAssignments(IEnumerable exprs) { - TableConstraint ct = AddAllowedAssignments(vars); + TableConstraint ct = AddAllowedAssignments(exprs); ct.Proto.Table.Negated = true; return ct; } diff --git a/ortools/sat/csharp/SatSolverTests.cs b/ortools/sat/csharp/SatSolverTests.cs index d1bcf2d227..8b3ede166a 100644 --- a/ortools/sat/csharp/SatSolverTests.cs +++ b/ortools/sat/csharp/SatSolverTests.cs @@ -393,7 +393,7 @@ public void Modulo() } [Fact] - public void ValueElement() + public void ValueElement() { CpModel model = new CpModel(); IntVar v1 = model.NewIntVar(1, 10, "v1"); @@ -402,7 +402,7 @@ public void ValueElement() Assert.Equal(3, model.Model.Constraints[0].Element.Exprs.Count); } - public void ExprElement() + public void ExprElement() { CpModel model = new CpModel(); IntVar v1 = model.NewIntVar(1, 10, "v1"); @@ -412,7 +412,7 @@ public void ExprElement() IntVar z = model.NewIntVar(0, 5, "z"); model.AddElement(v1, new LinearExpr[] {x + 2, -y, LinearExpr.Constant(5), 2 * z}, 5 - v2); Assert.Equal(4, model.Model.Constraints[0].Element.Exprs.Count); - } + } [Fact] public void LargeWeightedSumLong() diff --git a/ortools/sat/java/CpModelTest.java b/ortools/sat/java/CpModelTest.java index a27162e92b..fdc4454ff2 100644 --- a/ortools/sat/java/CpModelTest.java +++ b/ortools/sat/java/CpModelTest.java @@ -39,6 +39,7 @@ public void setUp() { @Test public void testCpModelNewIntVar() throws Exception { + System.out.println("testCpModelNewIntVar"); final CpModel model = new CpModel(); assertNotNull(model); final IntVar x = model.newIntVar(0, 10, "x"); @@ -64,6 +65,7 @@ public void testCpModelNewIntVar() throws Exception { @Test public void testCpModelNewIntervalVar() throws Exception { + System.out.println("testCpModelNewIntervalVar"); final CpModel model = new CpModel(); assertNotNull(model); final int horizon = 100; @@ -91,6 +93,7 @@ public void testCpModelNewIntervalVar() throws Exception { @Test public void testCpModelAddBoolOr() throws Exception { + System.out.println("testCpModelAddBoolOr"); final CpModel model = new CpModel(); assertNotNull(model); final BoolVar x = model.newBoolVar("x"); @@ -105,6 +108,7 @@ public void testCpModelAddBoolOr() throws Exception { @Test public void testCpModelAddAtLeastOne() throws Exception { + System.out.println("testCpModelAddAtLeastOne"); final CpModel model = new CpModel(); assertNotNull(model); final BoolVar x = model.newBoolVar("x"); @@ -119,6 +123,7 @@ public void testCpModelAddAtLeastOne() throws Exception { @Test public void testCpModelAddAtMostOne() throws Exception { + System.out.println("testCpModelAddAtMostOne"); final CpModel model = new CpModel(); assertNotNull(model); final BoolVar x = model.newBoolVar("x"); @@ -133,6 +138,7 @@ public void testCpModelAddAtMostOne() throws Exception { @Test public void testCpModelAddExactlyOne() throws Exception { + System.out.println("testCpModelAddExactlyOne"); final CpModel model = new CpModel(); assertNotNull(model); final BoolVar x = model.newBoolVar("x"); @@ -147,6 +153,7 @@ public void testCpModelAddExactlyOne() throws Exception { @Test public void testCpModelAddBoolAnd() throws Exception { + System.out.println("testCpModelAddBoolAnd"); final CpModel model = new CpModel(); assertNotNull(model); final BoolVar x = model.newBoolVar("x"); @@ -161,6 +168,7 @@ public void testCpModelAddBoolAnd() throws Exception { @Test public void testCpModelAddBoolXor() throws Exception { + System.out.println("testCpModelAddBoolXor"); final CpModel model = new CpModel(); assertNotNull(model); final BoolVar x = model.newBoolVar("x"); @@ -175,6 +183,7 @@ public void testCpModelAddBoolXor() throws Exception { @Test public void testCpModelAddImplication() throws Exception { + System.out.println("testCpModelAddImplication"); final CpModel model = new CpModel(); assertNotNull(model); final BoolVar x = model.newBoolVar("x"); @@ -188,6 +197,7 @@ public void testCpModelAddImplication() throws Exception { @Test public void testCpModelAddLinear() throws Exception { + System.out.println("testCpModelAddLinear"); final CpModel model = new CpModel(); assertNotNull(model); final BoolVar x = model.newBoolVar("x"); @@ -216,6 +226,7 @@ public void testCpModelAddLinear() throws Exception { @Test public void testLinearExprAddEqualityLiteral() { + System.out.println("testLinearExprAddEqualityLiteral"); final CpModel model = new CpModel(); assertNotNull(model); final Literal x = model.newBoolVar("x"); @@ -226,6 +237,7 @@ public void testLinearExprAddEqualityLiteral() { @Test public void testCpModelAddElement() throws Exception { + System.out.println("testCpModelAddElement"); final CpModel model = new CpModel(); assertNotNull(model); final IntVar x = model.newIntVar(0, 10, "x"); @@ -254,6 +266,7 @@ public void testCpModelAddElement() throws Exception { @Test public void testCpModelAddLinearArgumentElement() throws Exception { + System.out.println("testCpModelAddLinearArgumentElement"); final CpModel model = new CpModel(); assertNotNull(model); final IntVar x = model.newIntVar(0, 10, "x"); @@ -282,6 +295,7 @@ public void testCpModelAddLinearArgumentElement() throws Exception { @Test public void testCpModelAddExprElement() throws Exception { + System.out.println("testCpModelExceptionVisibility"); final CpModel model = new CpModel(); assertNotNull(model); final IntVar x = model.newIntVar(0, 10, "x"); @@ -315,6 +329,7 @@ public void testCpModelAddExprElement() throws Exception { @Test public void testCpModelAddConstantElement() throws Exception { + System.out.println("testCpModelAddConstantElement"); final CpModel model = new CpModel(); assertNotNull(model); final IntVar z = model.newIntVar(0, 10, "x"); @@ -345,6 +360,7 @@ public void testCpModelAddConstantElement() throws Exception { @Test public void testCpModelAddMinEquality() throws Exception { + System.out.println("testCpModelAddMinEquality"); final CpModel model = new CpModel(); assertNotNull(model); final BoolVar x = model.newBoolVar("x"); @@ -369,6 +385,7 @@ public void testCpModelAddMinEquality() throws Exception { @Test public void testCpModelAddMaxEquality() throws Exception { + System.out.println("testCpModelAddMaxEquality"); final CpModel model = new CpModel(); assertNotNull(model); final BoolVar x = model.newBoolVar("x"); @@ -393,6 +410,7 @@ public void testCpModelAddMaxEquality() throws Exception { @Test public void testCpModelAddMinExprEquality() throws Exception { + System.out.println("testCpModelAddMinExprEquality"); final CpModel model = new CpModel(); assertNotNull(model); final IntVar x = model.newBoolVar("x"); @@ -418,6 +436,7 @@ public void testCpModelAddMinExprEquality() throws Exception { @Test public void testCpModelAddAbsEquality() throws Exception { + System.out.println("testCpModelAddAbsEquality"); final CpModel model = new CpModel(); assertNotNull(model); final IntVar x = model.newBoolVar("x"); @@ -444,6 +463,7 @@ public void testCpModelAddAbsEquality() throws Exception { @Test public void testCpModelAddCircuit() throws Exception { + System.out.println("testCpModelAddCircuit"); final CpModel model = new CpModel(); assertNotNull(model); @@ -464,6 +484,7 @@ public void testCpModelAddCircuit() throws Exception { @Test public void testCpModelAddMultipleCircuit() throws Exception { + System.out.println("testCpModelAddMultipleCircuit"); final CpModel model = new CpModel(); assertNotNull(model); @@ -484,6 +505,7 @@ public void testCpModelAddMultipleCircuit() throws Exception { @Test public void testCpModelAddAutomaton() throws Exception { + System.out.println("testCpModelAddAutomaton"); final CpModel model = new CpModel(); assertNotNull(model); @@ -506,11 +528,13 @@ public void testCpModelAddAutomaton() throws Exception { assertThat(model.model().getConstraints(0).getAutomaton().getTransitionLabelCount()) .isEqualTo(3); assertThat(model.model().getConstraints(0).getAutomaton().getStartingState()).isEqualTo(0); + assertThat(model.model().getConstraints(0).getAutomaton().getFinalStatesCount()).isEqualTo(2); } @Test public void testCpModelAddNoOverlap() throws Exception { + System.out.println("testCpModelAddNoOverlap"); final CpModel model = new CpModel(); assertNotNull(model); final int horizon = 100; @@ -533,6 +557,7 @@ public void testCpModelAddNoOverlap() throws Exception { @Test public void testCpModelAddCumulative() throws Exception { + System.out.println("testCpModelAddCumulative"); final CpModel model = new CpModel(); assertNotNull(model); final int horizon = 100; @@ -568,6 +593,7 @@ public void testCpModelAddCumulative() throws Exception { @Test public void testCpModelAddNoOverlap2D() throws Exception { + System.out.println("testCpModelAddNoOverlap2D"); final CpModel model = new CpModel(); assertNotNull(model); final int horizon = 100; @@ -587,12 +613,15 @@ public void testCpModelAddNoOverlap2D() throws Exception { assertThat(model.model().getConstraints(0).hasInterval()).isTrue(); assertThat(model.model().getConstraints(1).hasInterval()).isTrue(); assertThat(model.model().getConstraints(2).hasNoOverlap2D()).isTrue(); + assertThat(model.model().getConstraints(2).getNoOverlap2D().getXIntervalsCount()).isEqualTo(2); + assertThat(model.model().getConstraints(2).getNoOverlap2D().getYIntervalsCount()).isEqualTo(2); } @Test public void testCpModelAddDecisionStrategy() throws Exception { + System.out.println("testCpModelAddDecisionStrategy"); final CpModel model = new CpModel(); assertNotNull(model); @@ -608,18 +637,21 @@ public void testCpModelAddDecisionStrategy() throws Exception { assertThat(model.model().getSearchStrategy(0).getExprsCount()).isEqualTo(3); assertThat(model.model().getSearchStrategy(0).getExprs(0).getVarsCount()).isEqualTo(1); assertThat(model.model().getSearchStrategy(0).getExprs(0).getCoeffsCount()).isEqualTo(1); + assertThat(model.model().getSearchStrategy(0).getExprs(0).getVars(0)).isEqualTo(x1.getIndex()); assertThat(model.model().getSearchStrategy(0).getExprs(0).getCoeffs(0)).isEqualTo(1); assertThat(model.model().getSearchStrategy(0).getExprs(0).getOffset()).isEqualTo(0); assertThat(model.model().getSearchStrategy(0).getExprs(1).getVarsCount()).isEqualTo(1); assertThat(model.model().getSearchStrategy(0).getExprs(1).getCoeffsCount()).isEqualTo(1); + assertThat(model.model().getSearchStrategy(0).getExprs(1).getVars(0)).isEqualTo(x2.getIndex()); assertThat(model.model().getSearchStrategy(0).getExprs(1).getCoeffs(0)).isEqualTo(-1); assertThat(model.model().getSearchStrategy(0).getExprs(1).getOffset()).isEqualTo(1); assertThat(model.model().getSearchStrategy(0).getExprs(2).getVarsCount()).isEqualTo(1); assertThat(model.model().getSearchStrategy(0).getExprs(2).getCoeffsCount()).isEqualTo(1); + assertThat(model.model().getSearchStrategy(0).getExprs(2).getVars(0)).isEqualTo(x3.getIndex()); assertThat(model.model().getSearchStrategy(0).getExprs(2).getCoeffs(0)).isEqualTo(1); assertThat(model.model().getSearchStrategy(0).getExprs(2).getOffset()).isEqualTo(0); @@ -627,6 +659,7 @@ public void testCpModelAddDecisionStrategy() throws Exception { @Test public void testCpModelModelStats() throws Exception { + System.out.println("testCpModelModelStats"); final CpModel model = new CpModel(); assertNotNull(model); final BoolVar x = model.newBoolVar("x"); @@ -639,6 +672,7 @@ public void testCpModelModelStats() throws Exception { @Test public void testCpModelValidateOk() throws Exception { + System.out.println("testCpModelValidateOk"); final CpModel model = new CpModel(); assertNotNull(model); final BoolVar x = model.newBoolVar("x"); @@ -651,6 +685,7 @@ public void testCpModelValidateOk() throws Exception { @Test public void testCpModelValidateNotOk() throws Exception { + System.out.println("testCpModelValidateNotOk"); final CpModel model = new CpModel(); assertNotNull(model); final IntVar x = model.newIntVar(0, 9223372036854775807L, "x"); @@ -664,6 +699,7 @@ public void testCpModelValidateNotOk() throws Exception { @Test public void testCpModelExceptionVisibility() throws Exception { + System.out.println("testCpModelExceptionVisibility"); CpModel.MismatchedArrayLengths ex1 = new CpModel.MismatchedArrayLengths("test1", "ar1", "ar2"); CpModel.WrongLength ex2 = new CpModel.WrongLength("test2", "ar"); assertThat(ex1).hasMessageThat().isEqualTo("test1: ar1 and ar2 have mismatched lengths"); @@ -672,6 +708,7 @@ public void testCpModelExceptionVisibility() throws Exception { @Test public void testCpModelClearConstraint() throws Exception { + System.out.println("testCpModelClearConstraint"); final CpModel model = new CpModel(); assertNotNull(model); final IntVar x = model.newIntVar(0, 92, "x"); @@ -707,6 +744,7 @@ public void testCpModelClearConstraint() throws Exception { @Test public void testCpModelMinimize() throws Exception { + System.out.println("testCpModelMinimize"); final CpModel model = new CpModel(); assertNotNull(model); @@ -727,10 +765,12 @@ public void testCpModelMinimize() throws Exception { assertThat(model.getBuilder().hasFloatingPointObjective()).isFalse(); model.minimize(DoubleLinearExpr.weightedSum(new IntVar[] {x1, x2}, new double[] {2.5, 3.5})); + assertThat(model.getBuilder().getFloatingPointObjectiveBuilder().getVarsCount()).isEqualTo(2); assertThat(model.getBuilder().hasObjective()).isFalse(); model.minimize(DoubleLinearExpr.affine(x3, 1.4, 1.2)); + assertThat(model.getBuilder().getFloatingPointObjectiveBuilder().getVarsCount()).isEqualTo(1); assertThat(model.getBuilder().hasObjective()).isFalse(); @@ -743,10 +783,12 @@ public void testCpModelMinimize() throws Exception { assertThat(model.getBuilder().hasFloatingPointObjective()).isFalse(); model.maximize(DoubleLinearExpr.weightedSum(new IntVar[] {x1, x2}, new double[] {2.5, 3.5})); + assertThat(model.getBuilder().getFloatingPointObjectiveBuilder().getVarsCount()).isEqualTo(2); assertThat(model.getBuilder().hasObjective()).isFalse(); model.maximize(DoubleLinearExpr.affine(x3, 1.4, 1.2)); + assertThat(model.getBuilder().getFloatingPointObjectiveBuilder().getVarsCount()).isEqualTo(1); assertThat(model.getBuilder().hasObjective()).isFalse(); } @@ -834,7 +876,7 @@ public void testCrashInSolveWithAllowedAssignment() { @Test public void testCrashEquality() { - System.out.println("testCrashInSolveWithAllowedAssignment"); + System.out.println("testCrashEquality"); final CpModel model = new CpModel(); final IntVar[] entities = new IntVar[20]; @@ -877,7 +919,9 @@ public void testCrashEquality() { } final CpSolver solver = new CpSolver(); + solver.getParameters().setLogToStdout(true); CpSolverStatus unused = solver.solve(model); + System.out.println(unused); } @Test diff --git a/ortools/sat/lb_tree_search.cc b/ortools/sat/lb_tree_search.cc index 394d5d09fa..d294bec6c3 100644 --- a/ortools/sat/lb_tree_search.cc +++ b/ortools/sat/lb_tree_search.cc @@ -527,6 +527,7 @@ SatSolver::Status LbTreeSearch::Search( // - when we go to a new branch. lp_constraint_->EnablePropagation(false); } + if (sat_solver_->ModelIsUnsat()) return sat_solver_->UnsatStatus(); // This will import other workers bound if we are back to level zero. // It might also decide to restart. diff --git a/ortools/sat/parameters_validation.cc b/ortools/sat/parameters_validation.cc index 4ee24917e0..5839cdf166 100644 --- a/ortools/sat/parameters_validation.cc +++ b/ortools/sat/parameters_validation.cc @@ -15,7 +15,6 @@ #include -#include #include #include #include @@ -55,44 +54,45 @@ namespace sat { std::string ValidateParameters(const SatParameters& params) { // Test that all floating point parameters are not NaN or +/- infinity. - TEST_IS_FINITE(random_polarity_ratio); - TEST_IS_FINITE(random_branches_ratio); - TEST_IS_FINITE(initial_variables_activity); + TEST_IS_FINITE(absolute_gap_limit); + TEST_IS_FINITE(blocking_restart_multiplier); + TEST_IS_FINITE(clause_activity_decay); TEST_IS_FINITE(clause_cleanup_ratio); - TEST_IS_FINITE(pb_cleanup_ratio); - TEST_IS_FINITE(variable_activity_decay); - TEST_IS_FINITE(max_variable_activity_value); - TEST_IS_FINITE(glucose_max_decay); + TEST_IS_FINITE(cut_active_count_decay); + TEST_IS_FINITE(cut_max_active_count_value); + TEST_IS_FINITE(feasibility_jump_batch_dtime); TEST_IS_FINITE(glucose_decay_increment); - TEST_IS_FINITE(clause_activity_decay); + TEST_IS_FINITE(glucose_max_decay); + TEST_IS_FINITE(initial_variables_activity); + TEST_IS_FINITE(inprocessing_dtime_ratio); + TEST_IS_FINITE(inprocessing_minimization_dtime); + TEST_IS_FINITE(inprocessing_probing_dtime); TEST_IS_FINITE(max_clause_activity_value); - TEST_IS_FINITE(restart_dl_average_ratio); - TEST_IS_FINITE(restart_lbd_average_ratio); - TEST_IS_FINITE(blocking_restart_multiplier); - TEST_IS_FINITE(strategy_change_increase_ratio); - TEST_IS_FINITE(absolute_gap_limit); - TEST_IS_FINITE(relative_gap_limit); - TEST_IS_FINITE(probing_deterministic_time_limit); - TEST_IS_FINITE(presolve_probing_deterministic_time_limit); - TEST_IS_FINITE(propagation_loop_detection_factor); - TEST_IS_FINITE(merge_no_overlap_work_limit); + TEST_IS_FINITE(max_variable_activity_value); TEST_IS_FINITE(merge_at_most_one_work_limit); + TEST_IS_FINITE(merge_no_overlap_work_limit); TEST_IS_FINITE(min_orthogonality_for_lp_constraints); - TEST_IS_FINITE(mip_var_scaling); - TEST_IS_FINITE(cut_max_active_count_value); - TEST_IS_FINITE(cut_active_count_decay); - TEST_IS_FINITE(shaving_search_deterministic_time); - TEST_IS_FINITE(inprocessing_dtime_ratio); - TEST_IS_FINITE(inprocessing_probing_dtime); - TEST_IS_FINITE(inprocessing_minimization_dtime); - TEST_IS_FINITE(mip_max_bound); - TEST_IS_FINITE(mip_wanted_precision); TEST_IS_FINITE(mip_check_precision); - TEST_IS_FINITE(mip_max_valid_magnitude); TEST_IS_FINITE(mip_drop_tolerance); - TEST_IS_FINITE(shared_tree_worker_objective_split_probability); + TEST_IS_FINITE(mip_max_bound); + TEST_IS_FINITE(mip_max_valid_magnitude); + TEST_IS_FINITE(mip_var_scaling); + TEST_IS_FINITE(mip_wanted_precision); + TEST_IS_FINITE(pb_cleanup_ratio); + TEST_IS_FINITE(presolve_probing_deterministic_time_limit); + TEST_IS_FINITE(probing_deterministic_time_limit); + TEST_IS_FINITE(propagation_loop_detection_factor); + TEST_IS_FINITE(random_branches_ratio); + TEST_IS_FINITE(random_polarity_ratio); + TEST_IS_FINITE(relative_gap_limit); + TEST_IS_FINITE(restart_dl_average_ratio); + TEST_IS_FINITE(restart_lbd_average_ratio); TEST_IS_FINITE(shared_tree_open_leaves_per_worker); - TEST_IS_FINITE(feasibility_jump_batch_dtime); + TEST_IS_FINITE(shared_tree_worker_objective_split_probability); + TEST_IS_FINITE(shaving_search_deterministic_time); + TEST_IS_FINITE(strategy_change_increase_ratio); + TEST_IS_FINITE(symmetry_detection_deterministic_time_limit); + TEST_IS_FINITE(variable_activity_decay); TEST_POSITIVE(at_most_one_max_expansion_size); @@ -140,13 +140,14 @@ std::string ValidateParameters(const SatParameters& params) { TEST_NON_NEGATIVE(lp_primal_tolerance); TEST_NON_NEGATIVE(lp_dual_tolerance); - TEST_NON_NEGATIVE(mip_wanted_precision); - TEST_NON_NEGATIVE(max_time_in_seconds); + TEST_NON_NEGATIVE(linearization_level); TEST_NON_NEGATIVE(max_deterministic_time); + TEST_NON_NEGATIVE(max_time_in_seconds); + TEST_NON_NEGATIVE(mip_wanted_precision); TEST_NON_NEGATIVE(new_constraints_batch_size); - TEST_NON_NEGATIVE(probing_deterministic_time_limit); TEST_NON_NEGATIVE(presolve_probing_deterministic_time_limit); - TEST_NON_NEGATIVE(linearization_level); + TEST_NON_NEGATIVE(probing_deterministic_time_limit); + TEST_NON_NEGATIVE(symmetry_detection_deterministic_time_limit); if (params.enumerate_all_solutions() && (params.num_search_workers() > 1 || params.num_workers() > 1)) { diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index 738297267d..9c8bccbd86 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -18,6 +18,7 @@ #include #include #include +#include #include #include #include @@ -32,10 +33,11 @@ #include "absl/meta/type_traits.h" #include "absl/numeric/int128.h" #include "absl/strings/str_cat.h" +#include "absl/strings/string_view.h" #include "absl/types/span.h" #include "ortools/algorithms/sparse_permutation.h" #include "ortools/base/logging.h" -#include "ortools/base/mathutil.h" +#include "ortools/base/stl_util.h" #include "ortools/port/proto_utils.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_loader.h" @@ -1156,7 +1158,7 @@ bool PresolveContext::StoreAffineRelation(int var_x, int var_y, int64_t coeff, CHECK_NE(a, 0); CHECK_NE(b, 0); { - const int64_t gcd = MathUtil::GCD64(std::abs(a), std::abs(b)); + const int64_t gcd = std::gcd(std::abs(a), std::abs(b)); if (gcd != 1) { a /= gcd; b /= gcd; @@ -1891,7 +1893,7 @@ bool PresolveContext::CanonicalizeObjective(bool simplify_domain) { for (const auto& entry : tmp_entries_) { const int var = entry.first; const int64_t coeff = entry.second; - gcd = MathUtil::GCD64(gcd, std::abs(coeff)); + gcd = std::gcd(gcd, std::abs(coeff)); implied_domain = implied_domain.AdditionWith(DomainOf(var).MultiplicationBy(coeff)) .RelaxIfTooComplex(); @@ -2567,5 +2569,145 @@ ConstraintProto* PresolveContext::NewMappingConstraint( return new_ct; } +void CanonicalizeTable(PresolveContext* context, ConstraintProto* ct) { + if (context->ModelIsUnsat()) return; + + const int num_exprs = ct->table().exprs_size(); + const int num_tuples = ct->table().values_size() / num_exprs; + + // Detect expressions sharing the same variable as a previous expression. + absl::flat_hash_map var_to_position; + + // The mapping between the position in the original list of expressions, and + // the position in the reduced list of expressions. + std::vector> position_mapping(num_exprs, std::nullopt); + int num_shared_vars = 0; + for (int i = 0; i < num_exprs; ++i) { + const LinearExpressionProto& expr = ct->table().exprs(i); + if (context->IsFixed(expr)) continue; + + const int var = expr.vars(0); + const auto [it, inserted] = + var_to_position.insert({var, var_to_position.size()}); + if (!inserted) { + ++num_shared_vars; + position_mapping[i] = it->second; + } + } + + const int num_kept_exprs = num_exprs - num_shared_vars; + + std::vector> new_tuples; + new_tuples.reserve(num_tuples); + + std::vector new_scaled_values; + new_scaled_values.reserve(num_kept_exprs); + + for (int t = 0; t < num_tuples; ++t) { + bool tuple_is_valid = true; + new_scaled_values.clear(); + + for (int e = 0; e < num_exprs; ++e) { + const int64_t value = ct->table().values(t * num_exprs + e); + const LinearExpressionProto& expr = ct->table().exprs(e); + if (context->IsFixed(expr)) { + if (value != context->FixedValue(expr)) { + tuple_is_valid = false; + break; + } + new_scaled_values.push_back(value); + } else if (position_mapping[e].has_value()) { + const int var_first_position = position_mapping[e].value(); + const int64_t var_value = new_scaled_values[var_first_position]; + const int64_t forced_value = AffineExpressionValueAt(expr, var_value); + if (value != forced_value) { + tuple_is_valid = false; + break; + } + } else { + if (!context->DomainContains(expr, value)) { + tuple_is_valid = false; + break; + } + new_scaled_values.push_back(GetInnerVarValue(expr, value)); + } + } + + if (tuple_is_valid) { + DCHECK_EQ(new_scaled_values.size(), num_kept_exprs); + new_tuples.push_back(new_scaled_values); + } + } + + // Remove all scaling on expressions as we have stored the inner values. + for (int e = 0; e < num_exprs; ++e) { + if (position_mapping[e].has_value()) continue; + if (context->IsFixed(ct->table().exprs(e))) continue; + DCHECK_EQ(ct->table().exprs(e).coeffs_size(), 1); + ct->mutable_table()->mutable_exprs(e)->set_offset(0); + ct->mutable_table()->mutable_exprs(e)->set_coeffs(0, 1); + } + + if (num_kept_exprs < num_exprs) { + int index = 0; + for (int e = 0; e < num_exprs; ++e) { + if (position_mapping[e].has_value()) continue; + ct->mutable_table()->mutable_exprs()->SwapElements(index++, e); + } + CHECK_EQ(index, num_kept_exprs); + ct->mutable_table()->mutable_exprs()->DeleteSubrange(index, + num_exprs - index); + context->UpdateRuleStats("table: remove expressions"); + } + + gtl::STLSortAndRemoveDuplicates(&new_tuples); + if (new_tuples.size() < num_tuples) { + context->UpdateRuleStats("table: remove tuples"); + } + + // Write sorted tuples. + ct->mutable_table()->clear_values(); + for (const std::vector& tuple : new_tuples) { + ct->mutable_table()->mutable_values()->Add(tuple.begin(), tuple.end()); + } +} + +void RemoveFixedColumnsFromTable(PresolveContext* context, + ConstraintProto* ct) { + if (context->ModelIsUnsat()) return; + const int num_exprs = ct->table().exprs_size(); + const int num_tuples = ct->table().values_size() / num_exprs; + std::vector is_fixed(num_exprs, false); + int num_fixed_exprs = 0; + for (int e = 0; e < num_exprs; ++e) { + is_fixed[e] = context->IsFixed(ct->table().exprs(e)); + num_fixed_exprs += is_fixed[e]; + } + if (num_fixed_exprs == 0) return; + + int num_kept_exprs = num_exprs - num_fixed_exprs; + + int index = 0; + for (int e = 0; e < num_exprs; ++e) { + if (is_fixed[e]) continue; + ct->mutable_table()->mutable_exprs()->SwapElements(index++, e); + } + CHECK_EQ(index, num_kept_exprs); + ct->mutable_table()->mutable_exprs()->DeleteSubrange(index, + num_exprs - index); + index = 0; + for (int t = 0; t < num_tuples; ++t) { + for (int e = 0; e < num_exprs; ++e) { + if (is_fixed[e]) continue; + ct->mutable_table()->set_values(index++, + ct->table().values(t * num_exprs + e)); + } + } + CHECK_EQ(index, num_tuples * num_kept_exprs); + ct->mutable_table()->mutable_values()->Truncate(index); + + context->UpdateRuleStats("table: remove fixed columns"); +} + } // namespace sat } // namespace operations_research diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index 318cc895e0..98bbaa0fc7 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -39,6 +39,7 @@ #include "ortools/util/affine_relation.h" #include "ortools/util/bitset.h" #include "ortools/util/logging.h" +#include "ortools/util/saturated_arithmetic.h" #include "ortools/util/sorted_interval_list.h" #include "ortools/util/time_limit.h" @@ -611,7 +612,7 @@ class PresolveContext { // Indicate if we are allowed to remove irrelevant feasible solution from the // set of feasible solution. For example, if a variable is unused, can we fix - // it to an arbitrary value (or its mimimum objective one)? This must be true + // it to an arbitrary value (or its minimum objective one)? This must be true // if the client wants to enumerate all solutions or wants correct tightened // bounds in the response. bool keep_all_feasible_solutions = false; @@ -703,7 +704,7 @@ class PresolveContext { // Internal representation of the objective. During presolve, we first load // the objective in this format in order to have more efficient substitution // on large problems (also because the objective is often dense). At the end - // we re-convert it to its proto form. + // we convert it back to its proto form. mutable bool objective_proto_is_up_to_date_ = false; absl::flat_hash_map objective_map_; int64_t objective_overflow_detection_; @@ -773,6 +774,15 @@ class PresolveContext { // that will be used for probing. Returns false if UNSAT. bool LoadModelForProbing(PresolveContext* context, Model* local_model); +// Canonicalizes the table constraint by removing all unreachable tuples, and +// all columns which have the same variable of a previous column. +// +// This also sort all the tuples. +void CanonicalizeTable(PresolveContext* context, ConstraintProto* ct); + +// Removed all fixed columns from the table. +void RemoveFixedColumnsFromTable(PresolveContext* context, ConstraintProto* ct); + } // namespace sat } // namespace operations_research diff --git a/ortools/sat/python/cp_model.py b/ortools/sat/python/cp_model.py index 720ec4bfd8..786aef5b9e 100644 --- a/ortools/sat/python/cp_model.py +++ b/ortools/sat/python/cp_model.py @@ -1587,10 +1587,10 @@ def add_element( Args: index: The index of the selected expression in the array. It must be an - affine variable (a * var + b). + affine expression (a * var + b). expressions: A list of affine expressions. target: The expression constrained to be equal to the selected expression. - It must be an affine variable (a * var + b). + It must be an affine expression (a * var + b). Returns: An instance of the `Constraint` class. @@ -1680,39 +1680,42 @@ def add_multiple_circuit(self, arcs: Sequence[ArcT]) -> Constraint: def add_allowed_assignments( self, - variables: Sequence[VariableT], + expressions: Sequence[LinearExprT], tuples_list: Iterable[Sequence[IntegralT]], ) -> Constraint: - """Adds AllowedAssignments(variables, tuples_list). + """Adds AllowedAssignments(expressions, tuples_list). - An AllowedAssignments constraint is a constraint on an array of variables, - which requires that when all variables are assigned values, the resulting - array equals one of the tuples in `tuple_list`. + An AllowedAssignments constraint is a constraint on an array of affine + expressions, which requires that when all expressions are assigned values, + the + resulting array equals one of the tuples in `tuple_list`. Args: - variables: A list of variables. + expressions: A list of affine expressions (a * var + b). tuples_list: A list of admissible tuples. Each tuple must have the same - length as the variables, and the ith value of a tuple corresponds to the - ith variable. + length as the expressions, and the ith value of a tuple corresponds to + the ith expression. Returns: An instance of the `Constraint` class. Raises: TypeError: If a tuple does not have the same size as the list of - variables. - ValueError: If the array of variables is empty. + expressions. + ValueError: If the array of expressions is empty. """ - if not variables: + if not expressions: raise ValueError( - "add_allowed_assignments expects a non-empty variables array" + "add_allowed_assignments expects a non-empty expressions array" ) ct: Constraint = Constraint(self) model_ct = self.__model.constraints[ct.index] - model_ct.table.vars.extend([self.get_or_make_index(x) for x in variables]) - arity: int = len(variables) + model_ct.table.exprs.extend( + [self.parse_linear_expression(e) for e in expressions] + ) + arity: int = len(expressions) for one_tuple in tuples_list: if len(one_tuple) != arity: raise TypeError("Tuple " + str(one_tuple) + " has the wrong arity") @@ -1731,36 +1734,37 @@ def add_allowed_assignments( def add_forbidden_assignments( self, - variables: Sequence[VariableT], + expressions: Sequence[LinearExprT], tuples_list: Iterable[Sequence[IntegralT]], ) -> Constraint: - """Adds add_forbidden_assignments(variables, [tuples_list]). + """Adds add_forbidden_assignments(expressions, [tuples_list]). - A ForbiddenAssignments constraint is a constraint on an array of variables - where the list of impossible combinations is provided in the tuples list. + A ForbiddenAssignments constraint is a constraint on an array of affine + expressions where the list of impossible combinations is provided in the + tuples list. Args: - variables: A list of variables. + expressions: A list of affine expressions (a * var + b). tuples_list: A list of forbidden tuples. Each tuple must have the same - length as the variables, and the *i*th value of a tuple corresponds to - the *i*th variable. + length as the expressions, and the *i*th value of a tuple corresponds to + the *i*th expression. Returns: An instance of the `Constraint` class. Raises: TypeError: If a tuple does not have the same size as the list of - variables. - ValueError: If the array of variables is empty. + expressions. + ValueError: If the array of expressions is empty. """ - if not variables: + if not expressions: raise ValueError( - "add_forbidden_assignments expects a non-empty variables array" + "add_forbidden_assignments expects a non-empty expressions array" ) index: int = len(self.__model.constraints) - ct: Constraint = self.add_allowed_assignments(variables, tuples_list) + ct: Constraint = self.add_allowed_assignments(expressions, tuples_list) self.__model.constraints[index].table.negated = True return ct diff --git a/ortools/sat/python/cp_model_test.py b/ortools/sat/python/cp_model_test.py index cf1ccb6d11..61e1aea2f5 100644 --- a/ortools/sat/python/cp_model_test.py +++ b/ortools/sat/python/cp_model_test.py @@ -676,7 +676,7 @@ def testAllowedAssignments(self) -> None: ) self.assertLen(model.proto.variables, 5) self.assertLen(model.proto.constraints, 1) - self.assertLen(model.proto.constraints[0].table.vars, 5) + self.assertLen(model.proto.constraints[0].table.exprs, 5) self.assertLen(model.proto.constraints[0].table.values, 15) self.assertRaises( TypeError, @@ -700,7 +700,7 @@ def testForbiddenAssignments(self) -> None: ) self.assertLen(model.proto.variables, 5) self.assertLen(model.proto.constraints, 1) - self.assertLen(model.proto.constraints[0].table.vars, 5) + self.assertLen(model.proto.constraints[0].table.exprs, 5) self.assertLen(model.proto.constraints[0].table.values, 15) self.assertTrue(model.proto.constraints[0].table.negated) self.assertRaises( diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 6e03c28e2d..bbc74c9d6f 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -23,7 +23,7 @@ option java_multiple_files = true; // Contains the definitions for all the sat algorithm parameters and their // default values. // -// NEXT TAG: 302 +// NEXT TAG: 303 message SatParameters { // In some context, like in a portfolio of search, it makes sense to name a // given parameters set for logging purpose. @@ -1334,6 +1334,10 @@ message SatParameters { // translation between the folded LP and the rest of the problem. optional bool use_symmetry_in_lp = 301 [default = false]; + // Deterministic time limit for symmetry detection. + optional double symmetry_detection_deterministic_time_limit = 302 + [default = 1.0]; + // The new linear propagation code treat all constraints at once and use // an adaptation of Bellman-Ford-Tarjan to propagate constraint in a smarter // order and potentially detect propagation cycle earlier.