cp_model.proto

// Copyright 2010-2018 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

// Proto describing a general Constraint Programming (CP) problem.

syntax = "proto3";

package operations_research.sat;

option csharp_namespace = "Google.OrTools.Sat";
option java_package = "com.google.ortools.sat";
option java_multiple_files = true;
option java_outer_classname = "CpModelProtobuf";

// An integer variable.
//
// It will be referred to by an int32 corresponding to its index in a
// CpModelProto variables field.
//
// Depending on the context, a reference to a variable whose domain is in [0, 1]
// can also be seen as a Boolean that will be true if the variable value is 1
// and false if it is 0. When used in this context, the field name will always
// contain the word "literal".
//
// Negative reference (advanced usage): to simplify the creation of a model and
// for efficiency reasons, all the "literal" or "variable" fields can also
// contain a negative index. A negative index i will refer to the negation of
// the integer variable at index -i -1 or to NOT the literal at the same index.
//
// Ex: A variable index 4 will refer to the integer variable model.variables(4)
// and an index of -5 will refer to the negation of the same variable. A literal
// index 4 will refer to the logical fact that model.variable(4) == 1 and a
// literal index of -5 will refer to the logical fact model.variable(4) == 0.
message IntegerVariableProto {
  // For debug/logging only. Can be empty.
  string name = 1;

  // The variable domain given as a sorted list of n disjoint intervals
  // [min, max] and encoded as [min_0, max_0,  ..., min_{n-1}, max_{n-1}].
  //
  // The most common example being just [min, max].
  // If min == max, then this is a constant variable.
  //
  // We have:
  //  - domain_size() is always even.
  //  - min == domain.front();
  //  - max == domain.back();
  //  - for all i < n   :      min_i <= max_i
  //  - for all i < n-1 :  max_i + 1 < min_{i+1}.
  //
  // Note that we check at validation that a variable domain is small enough so
  // that we don't run into integer overflow in our algorithms. Because of that,
  // you cannot just have "unbounded" variable like [0, kint64max] and should
  // try to specify tighter domains.
  repeated int64 domain = 2;
}

// Argument of the constraints of the form OP(literals).
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;
}

message LinearExpressionProto {
  repeated int32 vars = 1;
  repeated int32 coeffs = 2;
  int64 offset = 3;
}

message LinearArgumentProto {
  LinearExpressionProto target = 1;
  repeated LinearExpressionProto exprs = 2;
}

// All variables must take different values.
message AllDifferentConstraintProto {
  repeated int32 vars = 1;
}

// The linear sum vars[i] * coeffs[i] must fall in the given domain. The domain
// has the same format as the one in IntegerVariableProto.
//
// Note that the validation code currently checks using the domain of the
// involved variables that the sum can always be computed without integer
// overflow and throws an error otherwise.
message LinearConstraintProto {
  repeated int32 vars = 1;
  repeated int64 coeffs = 2;  // Same size as vars.
  repeated int64 domain = 3;
}

// The constraint target = vars[index].
// This enforces that index takes one of the value in [0, vars_size()).
message ElementConstraintProto {
  int32 index = 1;
  int32 target = 2;
  repeated int32 vars = 3;
}

// This "special" constraint not only enforces (start + size == end) but can
// also be referred by other constraints using this "interval" concept.
message IntervalConstraintProto {
  int32 start = 1;
  int32 end = 2;
  int32 size = 3;
}

// All the intervals (index of IntervalConstraintProto) must be disjoint. More
// formally, there must exist a sequence so that for each consecutive intervals,
// we have end_i <= start_{i+1}. In particular, intervals of size zero do matter
// for this constraint. This is also known as a disjunctive constraint in
// scheduling.
message NoOverlapConstraintProto {
  repeated int32 intervals = 1;
}

// The boxes defined by [start_x, end_x) * [start_y, end_y) cannot overlap.
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;
}

// 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.
message CumulativeConstraintProto {
  int32 capacity = 1;
  repeated int32 intervals = 2;
  repeated int32 demands = 3;  // Same size as intervals.
}

// Maintain a reservoir level within bounds. The water level starts at 0, and at
// any time >= 0, it must be within min_level, and max_level. Furthermore, this
// constraints expect all times variables to be >= 0.
// 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.
//
// Note that level min can be > 0, or level max can be < 0. It just forces
// some demands to be executed at time 0 to make sure that we are within those
// bounds with the executed demands. Therefore, at any time t >= 0:
//      sum(demands[i] * actives[i] if times[i] <= t) in [min_level, max_level]
// 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
// all actions will be performed.
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.
}

// The circuit constraint is defined on a graph where the arc presence are
// controlled by literals. Each arc is given by an index in the
// tails/heads/literals lists that must have the same size.
//
// For now, we ignore node indices with no incident arc. All the other nodes
// must have exactly one incoming and one outgoing selected arc (i.e. literal at
// true). All the selected arcs that are not self-loops must form a single
// circuit. Note that multi-arcs are allowed, but only one of them will be true
// at the same time. Multi-self loop are disallowed though.
message CircuitConstraintProto {
  repeated int32 tails = 3;
  repeated int32 heads = 4;
  repeated int32 literals = 5;
}

// The "VRP" (Vehicle Routing Problem) constraint.
//
// The direct graph where arc #i (from tails[i] to head[i]) is present iff
// literals[i] is true must satisfy this set of properties:
// - #incoming arcs == 1 except for node 0.
// - #outgoing arcs == 1 except for node 0.
// - for node zero, #incoming arcs == #outgoing arcs.
// - There are no duplicate arcs.
// - Self-arcs are allowed except for node 0.
// - There is no cycle in this graph, except through node 0.
//
// 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
// specific constraint allow us to add specific "cuts" to a VRP problem.
message RoutesConstraintProto {
  repeated int32 tails = 1;
  repeated int32 heads = 2;
  repeated int32 literals = 3;

  // 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.
  repeated int32 demands = 4;
  int64 capacity = 5;
}

// Another routing constraint. This one forces the nexts variables to form a
// permutation, and cycles of this permutation of length more than 1 (nonloops)
// to contain exactly one of the distinguished nodes.
message CircuitCoveringConstraintProto {
  repeated int32 nexts = 1;
  repeated int64 distinguished_nodes = 2;
}

// The values of the n-tuple formed by the given variables 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, ...].
message TableConstraintProto {
  repeated int32 vars = 1;
  repeated int64 values = 2;

  // If true, the meaning is "negated", that is we forbid any of the given
  // tuple from a feasible assignment.
  bool negated = 3;
}

// The two arrays of variable each represent a function, the second is the
// inverse of the first: f_direct[i] == j <=> f_inverse[j] == i.
message InverseConstraintProto {
  repeated int32 f_direct = 1;
  repeated int32 f_inverse = 2;
}

// This constraint forces a sequence of variables to be accepted by an
// automaton.
message AutomatonConstraintProto {
  // A state is identified by a non-negative number. It is preferable to keep
  // all the states dense in says [0, num_states). The automaton starts at
  // starting_state and must finish in any of the final states.
  int64 starting_state = 2;
  repeated int64 final_states = 3;

  // List of transitions (all 3 vectors have the same size). Both tail and head
  // are states, label is any variable value. No two outgoing transitions from
  // the same state can have the same label.
  repeated int64 transition_tail = 4;
  repeated int64 transition_head = 5;
  repeated int64 transition_label = 6;

  // The sequence of variables. The automaton is ran for vars_size() "steps" and
  // the value of vars[i] corresponds to the transition label at step i.
  repeated int32 vars = 7;
}

// Next id: 29
message ConstraintProto {
  // For debug/logging only. Can be empty.
  string name = 1;

  // The constraint will be enforced iff all literals listed here are true. If
  // this is empty, then the constraint will always be enforced. An enforced
  // constraint must be satisfied, and an un-enforced one will simply be
  // ignored.
  //
  // This is also called half-reification. To have an equivalence between a
  // literal and a constraint (full reification), one must add both a constraint
  // (controlled by a literal l) and its negation (controlled by the negation of
  // l).
  //
  // Important: as of September 2018, only a few constraint support enforcement:
  // - bool_or, bool_and, linear: fully supported.
  // - interval: only support a single enforcement literal.
  // - other: no support (but can be added on a per-demand basis).
  repeated int32 enforcement_literal = 2;

  // The actual constraint with its arguments.
  oneof constraint {
    // The bool_or constraint forces at least one literal to be true.
    BoolArgumentProto bool_or = 3;

    // The bool_and constraint forces all of the literals to be true.
    //
    // This is a "redundant" constraint in the sense that this can easily be
    // encoded with many bool_or. It is just more space efficient and handled
    // slightly differently internally.
    BoolArgumentProto bool_and = 4;

    // The at_most_one constraint enforces that no more than one literal is
    // true at the same time. Note that an at most one constraint of length n
    // could be encoded with n bool_and constraint with n-1 term on the right
    // hand side. So in a sense, this constraint contribute directly to the
    // "implication-graph" or the 2-SAT part of the model.
    BoolArgumentProto at_most_one = 26;

    // 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].
    IntegerArgumentProto int_div = 7;

    // The int_mod constraint forces the target to equal vars[0] % vars[1].
    IntegerArgumentProto int_mod = 8;

    // The int_max constraint forces the target to equal the maximum of all
    // variables.
    // TODO(user): Remove int_max in favor of lin_max.
    IntegerArgumentProto int_max = 9;

    // The lin_max constraint forces the target to equal the maximum of all
    // linear expressions.
    LinearArgumentProto lin_max = 27;

    // The int_min constraint forces the target to equal the minimum of all
    // variables.
    // TODO(user): Remove int_min in favor of lin_min.
    IntegerArgumentProto int_min = 10;

    // The lin_min constraint forces the target to equal the minimum of all
    // linear expressions.
    LinearArgumentProto lin_min = 28;

    // The int_prod constraint forces the target to equal the product of all
    // variables.
    IntegerArgumentProto int_prod = 11;

    // The linear constraint enforces a linear inequality among the variables,
    // such as 0 <= x + 2y <= 10.
    LinearConstraintProto linear = 12;

    // The all_diff constraint forces all variables to take different values.
    AllDifferentConstraintProto all_diff = 13;

    // The element constraint forces the variable with the given index
    // to be equal to the target.
    ElementConstraintProto element = 14;

    // The circuit constraint takes a graph and forces the arcs present
    // (with arc presence indicated by a literal) to form a unique cycle.
    CircuitConstraintProto circuit = 15;

    // The routes constraint implements the vehicle routing problem.
    RoutesConstraintProto routes = 23;

    // The circuit_covering constraint is similar to the circuit constraint,
    // but allows multiple non-overlapping cycles instead of just one.
    CircuitCoveringConstraintProto circuit_covering = 25;

    // The table constraint enforces what values a tuple of variables may
    // take.
    TableConstraintProto table = 16;

    // The automaton constraint forces a sequence of variables to be accepted
    // by an automaton.
    AutomatonConstraintProto automaton = 17;

    // The inverse constraint forces two arrays to be inverses of each other:
    // the values of one are the indices of the other, and vice versa.
    InverseConstraintProto inverse = 18;

    // The reservoir constraint forces the sum of a set of active demands
    // to always be between a specified minimum and maximum value during
    // specific times.
    ReservoirConstraintProto reservoir = 24;

    // Constraints on intervals.
    //
    // The first constraint defines what an "interval" is and the other
    // constraints use references to it. All the intervals that have an
    // enforcement_literal set to false are ignored by these constraints.
    //
    // TODO(user): Explain what happen for intervals of size zero. Some
    // constraints ignore them; others do take them into account.

    // The interval constraint takes a start, end, and size, and forces
    // start + size == end.
    IntervalConstraintProto interval = 19;

    // The no_overlap constraint prevents a set of intervals from
    // overlapping; in scheduling, this is called a disjunctive
    // constraint.
    NoOverlapConstraintProto no_overlap = 20;

    // The no_overlap_2d constraint prevents a set of boxes from overlapping.
    NoOverlap2DConstraintProto no_overlap_2d = 21;

    // The cumulative constraint ensures that for any integer point, the sum
    // of the demands of the intervals containing that point does not exceed
    // the capacity.
    CumulativeConstraintProto cumulative = 22;
  }
}

// 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.
  repeated int32 vars = 1;
  repeated int64 coeffs = 4;

  // The displayed objective is always:
  //   scaling_factor * (sum(coefficients[i] * objective_vars[i]) + offset).
  // This is needed to have a consistent objective after presolve or when
  // scaling a double problem to express it with integers.
  //
  // Note that if scaling_factor is zero, then it is assumed to be 1, so that by
  // default these fields have no effect.
  double offset = 2;
  double scaling_factor = 3;

  // If non-empty, only look for an objective value in the given domain.
  // 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;
}

// Define the strategy to follow when the solver needs to take a new decision.
// Note that this strategy is only defined on a subset of variables.
message DecisionStrategyProto {
  // The variables to be considered for the next decision. The order matter and
  // is always used as a tie-breaker after the variable selection strategy
  // criteria defined below.
  repeated int32 variables = 1;

  // The order in which the variables above should be considered. Note that only
  // variables that are not already fixed are considered.
  //
  // TODO(user): extend as needed.
  enum VariableSelectionStrategy {
    CHOOSE_FIRST = 0;
    CHOOSE_LOWEST_MIN = 1;
    CHOOSE_HIGHEST_MAX = 2;
    CHOOSE_MIN_DOMAIN_SIZE = 3;
    CHOOSE_MAX_DOMAIN_SIZE = 4;
  }
  VariableSelectionStrategy variable_selection_strategy = 2;

  // Once a variable has been chosen, this enum describe what decision is taken
  // on its domain.
  //
  // TODO(user): extend as needed.
  enum DomainReductionStrategy {
    SELECT_MIN_VALUE = 0;
    SELECT_MAX_VALUE = 1;
    SELECT_LOWER_HALF = 2;
    SELECT_UPPER_HALF = 3;
    SELECT_MEDIAN_VALUE = 4;
  }
  DomainReductionStrategy domain_reduction_strategy = 3;

  // Advanced usage. Some of the variable listed above may have been transformed
  // by the presolve so this is needed to properly follow the given selection
  // strategy. Instead of using a value X from one of the variable listed here,
  // we will use positive_coeff * X + offset instead.
  message AffineTransformation {
    int32 var = 1;
    int64 offset = 2;
    int64 positive_coeff = 3;
  }
  repeated AffineTransformation transformations = 4;
}

// This message encodes a partial (or full) assignment of the variables of a
// CpModelProto. The variable indices should be unique and valid variable
// indices.
message PartialVariableAssignment {
  repeated int32 vars = 1;
  repeated int64 values = 2;
}

// A constraint programming problem.
message CpModelProto {
  // For debug/logging only. Can be empty.
  string name = 1;

  // The associated Protos should be referred by their index in these fields.
  repeated IntegerVariableProto variables = 2;
  repeated ConstraintProto constraints = 3;

  // The objective to minimize. Can be empty for pure decision problems.
  CpObjectiveProto objective = 4;

  // 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.
  //
  // 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.
  repeated DecisionStrategyProto search_strategy = 5;

  // Solution hint.
  //
  // If a feasible or almost-feasible solution to the problem is already known,
  // it may be helpful to pass it to the solver so that it can be used. The
  // solver will try to use this information to create its initial feasible
  // solution.
  //
  // Note that it may not always be faster to give a hint like this to the
  // solver. There is also no guarantee that the solver will use this hint or
  // try to return a solution "close" to this assignment in case of multiple
  // optimal solutions.
  PartialVariableAssignment solution_hint = 6;

  // A list of literals. The model will be solved assuming all these literals
  // are true. Compared to just fixing the domain of these literals, using this
  // mechanism is slower but allows in case the model is INFEASIBLE to get a
  // potentially small subset of them that can be used to explain the
  // 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
  // related constraint under only one enforcement literal which can potentially
  // give you a good and interpretable explanation for infeasiblity.
  //
  // Such infeasibility explanation will be available in the
  // sufficient_assumptions_for_infeasibility response field.
  repeated int32 assumptions = 7;
}

// The status returned by a solver trying to solve a CpModelProto.
enum CpSolverStatus {
  // The status of the model is still unknown. A search limit has been reached
  // before any of the statuses below could be determined.
  UNKNOWN = 0;

  // The given CpModelProto didn't pass the validation step. You can get a
  // detailed error by calling ValidateCpModel(model_proto).
  MODEL_INVALID = 1;

  // A feasible solution as been found. But the search was stopped before we
  // could prove optimality or before we enumerated all solutions of a
  // feasibility problem (if asked).
  FEASIBLE = 2;

  // The problem has been proven infeasible.
  INFEASIBLE = 3;

  // An optimal feasible solution has been found.
  //
  // More generally, this status represent a success. So we also return OPTIMAL
  // if we find a solution for a pure feasiblity problem or if a gap limit has
  // been specified and we return a solution within this limit. In the case
  // where we need to return all the feasible solution, this status will only be
  // returned if we enumerated all of them; If we stopped before, we will return
  // FEASIBLE.
  OPTIMAL = 4;
}

// 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: 24
message CpSolverResponse {
  // The status of the solve.
  CpSolverStatus status = 1;

  // A feasible solution to the given problem. Depending on the returned status
  // it may be optimal or just feasible. This is in one-to-one correspondence
  // with a CpModelProto::variables repeated field and list the values of all
  // the variables.
  repeated int64 solution = 2;

  // Only make sense for an optimization problem. The objective value of the
  // returned solution if it is non-empty. If there is no solution, then for a
  // minimization problem, this will be an upper-bound of the objective of any
  // feasible solution, and a lower-bound for a maximization problem.
  double objective_value = 3;

  // Only make sense for an optimization problem. A proven lower-bound on the
  // objective for a minimization problem, or a proven upper-bound for a
  // maximization problem.
  double best_objective_bound = 4;

  // Advanced usage.
  //
  // 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;

  // Advanced usage.
  //
  // If the option fill_tightened_domains_in_response is set, then this field
  // will be a copy of the CpModelProto.variables where each domain has been
  // reduced using the information the solver was able to derive. Note that this
  // is only filled with the info derived during a normal search and we do not
  // have any dedicated algorithm to improve it.
  //
  // If the problem is a feasibility problem, then these bounds will be valid
  // for any feasible solution. If the problem is an optimization problem, then
  // these bounds will only be valid for any OPTIMAL solutions, it can exclude
  // sub-optimal feasible ones.
  repeated IntegerVariableProto tightened_variables = 21;

  // A subset of the model "assumptions" field. This will only be filled if the
  // status is INFEASIBLE. This subset of assumption will be enough to still get
  // an infeasible problem.
  //
  // This is related to what is called the irreducible inconsistent subsystem or
  // IIS. Except one is only concerned by the provided assumptions. There is
  // also no guarantee that we return an irreducible (aka minimal subset).
  // However, this is based on SAT explanation and there is a good chance it is
  // not too large.
  //
  // If you really want a minimal subset, a possible way to get one is by
  // changing your model to minimize the number of assumptions at false, but
  // this is likely an harder problem to solve.
  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.
  //
  // TODO(user): Remove as we also use the OPTIMAL vs FEASIBLE status for that.
  bool all_solutions_were_found = 5;

  // Some statistics about the solve.
  int64 num_booleans = 10;
  int64 num_conflicts = 11;
  int64 num_branches = 12;
  int64 num_binary_propagations = 13;
  int64 num_integer_propagations = 14;
  double wall_time = 15;
  double user_time = 16;
  double deterministic_time = 17;
  double primal_integral = 22;

  // Additional information about how the solution was found.
  string solution_info = 20;
}