diff --git a/src/builder.rs b/src/builder.rs index d5dbd3e..4b3b811 100644 --- a/src/builder.rs +++ b/src/builder.rs @@ -349,9 +349,9 @@ impl CpModelBuilder { /// assert!(x_val != z_val); /// assert!(y_val != z_val); /// ``` - pub fn add_all_different(&mut self, vars: impl IntoIterator) -> Constraint { + pub fn add_all_different(&mut self, exprs: impl IntoIterator>) -> Constraint { self.add_cst(CstEnum::AllDiff(proto::AllDifferentConstraintProto { - vars: vars.into_iter().map(|v| v.0).collect(), + exprs: exprs.into_iter().map(|e| e.into().into()).collect(), })) } @@ -548,6 +548,36 @@ impl CpModelBuilder { self.add_linear_constraint(lhs.into() - rhs.into(), [(i64::MIN, -1), (1, i64::MAX)]) } + /// Adds a constraint that force the `target` to be equal to the + /// product of the given `exprs`. + /// + /// # Example + /// + /// ``` + /// # use cp_sat::builder::{CpModelBuilder, LinearExpr}; + /// # use cp_sat::proto::CpSolverStatus; + /// let mut model = CpModelBuilder::default(); + /// let x = model.new_int_var([(0, 10)]); + /// let y = model.new_int_var([(5, 15)]); + /// let m = model.new_int_var([(-200, 200)]); + /// model.add_mult_eq(m, [x, y]); + /// model.maximize(m); + /// let response = model.solve(); + /// assert_eq!(response.status(), CpSolverStatus::Optimal); + /// assert_eq!(150., response.objective_value); + /// assert_eq!(150, m.solution_value(&response)); + /// ``` + pub fn add_mult_eq( + &mut self, + target: impl Into, + exprs: impl IntoIterator>, + ) -> Constraint { + self.add_cst(CstEnum::IntProd(proto::LinearArgumentProto { + target: Some(target.into().into()), + exprs: exprs.into_iter().map(|e| e.into().into()).collect(), + })) + } + /// Adds a constraint that force the `target` to be equal to the /// minimum of the given `exprs`. /// @@ -572,9 +602,9 @@ impl CpModelBuilder { target: impl Into, exprs: impl IntoIterator>, ) -> Constraint { - self.add_cst(CstEnum::LinMin(proto::LinearArgumentProto { - target: Some(target.into().into()), - exprs: exprs.into_iter().map(|e| e.into().into()).collect(), + self.add_cst(CstEnum::LinMax(proto::LinearArgumentProto { + target: Some((-target.into()).into()), + exprs: exprs.into_iter().map(|e| (-e.into()).into()).collect(), })) } @@ -607,6 +637,7 @@ impl CpModelBuilder { exprs: exprs.into_iter().map(|e| e.into().into()).collect(), })) } + fn add_cst(&mut self, cst: CstEnum) -> Constraint { let index = self.proto.constraints.len(); self.proto.constraints.push(proto::ConstraintProto { @@ -690,6 +721,10 @@ impl CpModelBuilder { coeffs: expr.coeffs.into_vec(), offset: expr.constant as f64, scaling_factor: 1., + integer_before_offset: 0, + integer_after_offset: 0, + integer_scaling_factor: 0, + scaling_was_exact: true, domain: vec![], }); } @@ -719,6 +754,10 @@ impl CpModelBuilder { coeffs: expr.coeffs.into_vec(), offset: -expr.constant as f64, scaling_factor: -1., + integer_before_offset: 0, + integer_after_offset: 0, + integer_scaling_factor: 0, + scaling_was_exact: true, domain: vec![], }); } diff --git a/src/cp_model.proto b/src/cp_model.proto index 3852e06..77d9af3 100644 --- a/src/cp_model.proto +++ b/src/cp_model.proto @@ -1,4 +1,4 @@ -// Copyright 2010-2021 Google LLC +// Copyright 2010-2022 Google LLC // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at @@ -70,12 +70,6 @@ message BoolArgumentProto { repeated int32 literals = 1; } -// Argument of the constraints of the form target_var = OP(vars). -message IntegerArgumentProto { - int32 target = 1; - repeated int32 vars = 2; -} - // Some constraints supports linear expression instead of just using a reference // to a variable. This is especially useful during presolve to reduce the model // size. @@ -90,9 +84,9 @@ message LinearArgumentProto { repeated LinearExpressionProto exprs = 2; } -// All variables must take different values. +// All affine expressions must take different values. message AllDifferentConstraintProto { - repeated int32 vars = 1; + repeated LinearExpressionProto exprs = 1; } // The linear sum vars[i] * coeffs[i] must fall in the given domain. The domain @@ -115,33 +109,21 @@ message ElementConstraintProto { repeated int32 vars = 3; } -// This "special" constraint not only enforces (start + size == end) and (size -// >= 0) but can also be referred by other constraints using this "interval" -// concept. +// This is not really a constraint. It is there so it can be referred by other +// constraints using this "interval" concept. +// +// IMPORTANT: For now, this constraint do not enforce any relations on the +// components, and it is up to the client to add in the model: +// - enforcement => start + size == end. +// - enforcement => size >= 0 // Only needed if size is not already >= 0. +// +// IMPORTANT: For now, we just support affine relation. We could easily +// create an intermediate variable to support full linear expression, but this +// isn't done currently. message IntervalConstraintProto { - int32 start = 1; - int32 end = 2; - int32 size = 3; - - // EXPERIMENTAL: This will become the new way to specify an interval. - // Depending on the parameters, the presolve will convert the old way to the - // new way. Do not forget to add an associated linear constraint if you use - // this directly. - // - // If any of this field is set, then all must be set and the ones above will - // be ignored. - // - // IMPORTANT: For now, this constraint do not enforce any relations on the - // view, and a linear constraint must be added together with this to enforce - // enforcement => start_view + size_view == end_view. An enforcement => - // size_view >=0 might also be needed. - // - // IMPORTANT: For now, we just support affine relation. We could easily - // create an intermediate variable to support full linear expression, but this - // isn't done currently. - LinearExpressionProto start_view = 4; - LinearExpressionProto end_view = 5; - LinearExpressionProto size_view = 6; + LinearExpressionProto start = 4; + LinearExpressionProto end = 5; + LinearExpressionProto size = 6; } // All the intervals (index of IntervalConstraintProto) must be disjoint. More @@ -154,32 +136,41 @@ message NoOverlapConstraintProto { } // The boxes defined by [start_x, end_x) * [start_y, end_y) cannot overlap. +// Furthermore, one box is optional if at least one of the x or y interval is +// optional. message NoOverlap2DConstraintProto { repeated int32 x_intervals = 1; repeated int32 y_intervals = 2; // Same size as x_intervals. bool boxes_with_null_area_can_overlap = 3; + // TODO(user): Add optional areas as repeated LinearExpressionProto. } // The sum of the demands of the intervals at each interval point cannot exceed // a capacity. Note that intervals are interpreted as [start, end) and as // such intervals like [2,3) and [3,4) do not overlap for the point of view of // this constraint. Moreover, intervals of size zero are ignored. +// +// All demands must not contain any negative value in their domains. This is +// checked at validation. The capacity can currently contains negative values, +// but it will be propagated to >= 0 right away. message CumulativeConstraintProto { - int32 capacity = 1; + LinearExpressionProto capacity = 1; repeated int32 intervals = 2; - repeated int32 demands = 3; // Same size as intervals. + repeated LinearExpressionProto demands = 3; // Same size as intervals. } // Maintain a reservoir level within bounds. The water level starts at 0, and at // any time, it must be within [min_level, max_level]. // -// If the variable actives[i] is true, and if the variable times[i] is assigned -// a value t, then the current level changes by demands[i] (which is constant) -// at the time t. Therefore, at any time t: -// sum(demands[i] * actives[i] if times[i] <= t) in [min_level, max_level] +// If the variable active_literals[i] is true, and if the expression +// time_exprs[i] is assigned a value t, then the current level changes by +// level_changes[i] at the time t. Therefore, at any time t: +// +// sum(level_changes[i] * active_literals[i] if time_exprs[i] <= t) +// in [min_level, max_level] // // Note that min level must be <= 0, and the max level must be >= 0. Please use -// fixed demands to simulate initial state. +// fixed level_changes to simulate initial state. // // The array of boolean variables 'actives', if defined, indicates which actions // are actually performed. If this array is not defined, then it is assumed that @@ -187,9 +178,11 @@ message CumulativeConstraintProto { message ReservoirConstraintProto { int64 min_level = 1; int64 max_level = 2; - repeated int32 times = 3; // variables. - repeated int64 demands = 4; // constants, can be negative. - repeated int32 actives = 5; // literals. + repeated LinearExpressionProto time_exprs = 3; // affine expressions. + // Currently, we only support constant level changes. + repeated LinearExpressionProto level_changes = 6; // affine expressions. + repeated int32 active_literals = 5; + reserved 4; } // The circuit constraint is defined on a graph where the arc presence are @@ -218,6 +211,11 @@ message CircuitConstraintProto { // - Self-arcs are allowed except for node 0. // - There is no cycle in this graph, except through node 0. // +// Note: Currently this constraint expect all the nodes in [0, num_nodes) to +// have at least one incident arc. The model will be considered invalid if it +// is not the case. You can add self-arc fixed to one to ignore some nodes if +// needed. +// // TODO(user): It is probably possible to generalize this constraint to a // no-cycle in a general graph, or a no-cycle with sum incoming <= 1 and sum // outgoing <= 1 (more efficient implementation). On the other hand, having this @@ -227,7 +225,7 @@ message RoutesConstraintProto { repeated int32 heads = 2; repeated int32 literals = 3; - // Experimental. The demands for each node, and the maximum capacity for each + // EXPERIMENTAL. The demands for each node, and the maximum capacity for each // route. Note that this is currently only used for the LP relaxation and one // need to add the corresponding constraint to enforce this outside of the LP. // @@ -280,7 +278,12 @@ message AutomatonConstraintProto { repeated int32 vars = 7; } -// Next id: 30 +// A list of variables, without any semantics. +message ListOfVariablesProto { + repeated int32 vars = 1; +} + +// Next id: 31 message ConstraintProto { // For debug/logging only. Can be empty. string name = 1; @@ -343,40 +346,31 @@ message ConstraintProto { // The bool_xor constraint forces an odd number of the literals to be true. BoolArgumentProto bool_xor = 5; - // The int_div constraint forces the target to equal vars[0] / vars[1]. - // In particular, vars[1] can never take the value 0. - IntegerArgumentProto int_div = 7; + // The int_div constraint forces the target to equal exprs[0] / exprs[1]. + // In particular, exprs[1] can never take the value 0. Also, as for now, we + // do not support exprs[1] spanning across 0. + LinearArgumentProto int_div = 7; - // The int_mod constraint forces the target to equal vars[0] % vars[1]. - // The domain of vars[1] must be strictly positive. - IntegerArgumentProto int_mod = 8; - - // The int_max constraint forces the target to equal the maximum of all - // variables. - // - // The lin_max constraint forces the target to equal the maximum of all - // linear expressions. - // - // TODO(user): Remove int_max in favor of lin_max. - IntegerArgumentProto int_max = 9; - LinearArgumentProto lin_max = 27; - - // The int_min constraint forces the target to equal the minimum of all - // variables. - // - // The lin_min constraint forces the target to equal the minimum of all - // linear expressions. - // - // TODO(user): Remove int_min in favor of lin_min. - IntegerArgumentProto int_min = 10; - LinearArgumentProto lin_min = 28; + // The int_mod constraint forces the target to equal exprs[0] % exprs[1]. + // The domain of exprs[1] must be strictly positive. The sign of the target + // is the same as the sign of exprs[0]. + LinearArgumentProto int_mod = 8; // The int_prod constraint forces the target to equal the product of all // variables. By convention, because we can just remove term equal to one, // the empty product forces the target to be one. // + // Note that the solver checks for potential integer overflow. So it is + // recommended to limit the domain of the variables such that the product + // fits in [INT_MIN + 1..INT_MAX - 1]. + // // TODO(user): Support more than two terms in the product. - IntegerArgumentProto int_prod = 11; + LinearArgumentProto int_prod = 11; + + // The lin_max constraint forces the target to equal the maximum of all + // linear expressions. + // Note that this can model a minimum simply by negating all expressions. + LinearArgumentProto lin_max = 27; // The linear constraint enforces a linear inequality among the variables, // such as 0 <= x + 2y <= 10. @@ -438,16 +432,18 @@ message ConstraintProto { // of the demands of the intervals containing that point does not exceed // the capacity. CumulativeConstraintProto cumulative = 22; + + // This constraint is not meant to be used and will be rejected by the + // solver. It is meant to mark variable when testing the presolve code. + ListOfVariablesProto dummy_constraint = 30; } } // Optimization objective. -// -// This is in a message because decision problems don't have any objective. message CpObjectiveProto { // The linear terms of the objective to minimize. // For a maximization problem, one can negate all coefficients in the - // objective and set a scaling_factor to -1. + // objective and set scaling_factor to -1. repeated int32 vars = 1; repeated int64 coeffs = 4; @@ -465,6 +461,40 @@ message CpObjectiveProto { // Note that this does not depend on the offset or scaling factor, it is a // domain on the sum of the objective terms only. repeated int64 domain = 5; + + // Internal field. Do not set. When we scale a FloatObjectiveProto to a + // integer version, we set this to true if the scaling was exact (i.e. all + // original coeff were integer for instance). + // + // TODO(user): Put the error bounds we computed instead? + bool scaling_was_exact = 6; + + // Internal fields to recover a bound on the original integer objective from + // the presolved one. Basically, initially the integer objective fit on an + // int64 and is in [Initial_lb, Initial_ub]. During presolve, we might change + // the linear expression to have a new domain [Presolved_lb, Presolved_ub] + // that will also always fit on an int64. + // + // The two domain will always be linked with an affine transformation between + // the two of the form: + // old = (new + before_offset) * integer_scaling_factor + after_offset. + // Note that we use both offsets to always be able to do the computation while + // staying in the int64 domain. In particular, the after_offset will always + // be in (-integer_scaling_factor, integer_scaling_factor). + int64 integer_before_offset = 7; + int64 integer_after_offset = 9; + int64 integer_scaling_factor = 8; +} + +// A linear floating point objective: sum coeffs[i] * vars[i] + offset. +// Note that the variable can only still take integer value. +message FloatObjectiveProto { + repeated int32 vars = 1; + repeated double coeffs = 2; + double offset = 3; + + // The optimization direction. The default is to minimize + bool maximize = 4; } // Define the strategy to follow when the solver needs to take a new decision. @@ -538,7 +568,7 @@ message DenseMatrixProto { repeated int32 entries = 3; } -// Experimental. For now, this is meant to be used by the solver and not filled +// EXPERIMENTAL. For now, this is meant to be used by the solver and not filled // by clients. // // Hold symmetry information about the set of feasible solutions. If we permute @@ -580,6 +610,21 @@ message CpModelProto { // The objective to minimize. Can be empty for pure decision problems. CpObjectiveProto objective = 4; + // Advanced usage. + // It is invalid to have both an objective and a floating point objective. + // + // The objective of the model, in floating point format. The solver will + // automatically scale this to integer during expansion and thus convert it to + // a normal CpObjectiveProto. See the mip* parameters to control how this is + // scaled. In most situation the precision will be good enough, but you can + // see the logs to see what are the precision guaranteed when this is + // converted to a fixed point representation. + // + // Note that even if the precision is bad, the returned objective_value and + // best_objective_bound will be computed correctly. So at the end of the solve + // you can check the gap if you only want precise optimal. + FloatObjectiveProto floating_point_objective = 9; + // Defines the strategy that the solver should follow when the // search_branching parameter is set to FIXED_SEARCH. Note that this strategy // is also used as a heuristic when we are not in fixed search. @@ -587,9 +632,8 @@ message CpModelProto { // Advanced Usage: if not all variables appears and the parameter // "instantiate_all_variables" is set to false, then the solver will not try // to instantiate the variables that do not appear. Thus, at the end of the - // search, not all variables may be fixed and this is why we have the - // solution_lower_bounds and solution_upper_bounds fields in the - // CpSolverResponse. + // search, not all variables may be fixed. Currently, we will set them to + // their lower bound in the solution. repeated DecisionStrategyProto search_strategy = 5; // Solution hint. @@ -612,7 +656,7 @@ message CpModelProto { // infeasibility. // // Think (IIS), except when you are only concerned by the provided - // assumptions. This is powerful as it allows to group a set of logicially + // assumptions. This is powerful as it allows to group a set of logically // related constraint under only one enforcement literal which can potentially // give you a good and interpretable explanation for infeasiblity. // @@ -657,11 +701,17 @@ enum CpSolverStatus { OPTIMAL = 4; } +// Just a message used to store dense solution. +// This is used by the additional_solutions field. +message CpSolverSolution { + repeated int64 values = 1; +} + // The response returned by a solver trying to solve a CpModelProto. // // TODO(user): support returning multiple solutions. Look at the Stubby // streaming API as we probably wants to get them as they are found. -// Next id: 27 +// Next id: 30 message CpSolverResponse { // The status of the solve. CpSolverStatus status = 1; @@ -683,15 +733,13 @@ message CpSolverResponse { // maximization problem. double best_objective_bound = 4; - // Advanced usage. + // If the parameter fill_additional_solutions_in_response is set, then we + // copy all the solutions from our internal solution pool here. // - // If the problem has some variables that are not fixed at the end of the - // search (because of a particular search strategy in the CpModelProto) then - // this will be used instead of filling the solution above. The two fields - // will then contains the lower and upper bounds of each variable as they were - // when the best "solution" was found. - repeated int64 solution_lower_bounds = 18; - repeated int64 solution_upper_bounds = 19; + // Note that the one returned in the solution field will likely appear here + // too. Do not rely on the solutions order as it depends on our internal + // representation (after postsolve). + repeated CpSolverSolution additional_solutions = 27; // Advanced usage. // @@ -721,17 +769,28 @@ message CpSolverResponse { // changing your model to minimize the number of assumptions at false, but // this is likely an harder problem to solve. // + // Important: Currently, this is minimized only in single-thread and if the + // problem is not an optimization problem, otherwise, it will always include + // all the assumptions. + // // TODO(user): Allows for returning multiple core at once. repeated int32 sufficient_assumptions_for_infeasibility = 23; - // This will be true iff the solver was asked to find all solutions to a - // satisfiability problem (or all optimal solutions to an optimization - // problem), and it was successful in doing so. + // Contains the integer objective optimized internally. This is only filled if + // the problem had a floating point objective, and on the final response, not + // the ones given to callbacks. + CpObjectiveProto integer_objective = 28; + + // Advanced usage. // - // TODO(user): Remove as we also use the OPTIMAL vs FEASIBLE status for that. - bool all_solutions_were_found = 5; + // A lower bound on the inner integer expression of the objective. This is + // either a bound on the expression in the returned integer_objective or on + // the integer expression of the original objective if the problem already has + // an integer objective. + int64 inner_objective_lower_bound = 29; // Some statistics about the solve. + // TODO(user): These are broken in multi-thread. int64 num_booleans = 10; int64 num_conflicts = 11; int64 num_branches = 12; @@ -740,12 +799,16 @@ message CpSolverResponse { int64 num_restarts = 24; int64 num_lp_iterations = 25; + // The time counted from the beginning of the Solve() call. double wall_time = 15; double user_time = 16; double deterministic_time = 17; - double primal_integral = 22; - // Additional information about how the solution was found. + // The integral of log(1 + absolute_objective_gap) over time. + double gap_integral = 22; + + // Additional information about how the solution was found. It also stores + // model or parameters errors that caused the model to be invalid. string solution_info = 20; // The solve log will be filled if the parameter log_to_response is set to