Dark-Alex-17/cp_sat
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

v0.1.0

Browse Source
This commit is contained in:
Guillaume Pinot
2021-09-07 20:12:12 +02:00
parent a799d481c6
commit adcc1d638b
9 changed files with 2055 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/cp_model.proto
+754
View File
@@ -0,0 +1,754 @@
// Copyright 2010-2021 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;
}
// 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.
message LinearExpressionProto {
repeated int32 vars = 1;
repeated int64 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) and (size
// >= 0) but can also be referred by other constraints using this "interval"
// concept.
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;
}
// 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, 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]
//
// Note that min level must be <= 0, and the max level must be >= 0. Please use
// fixed demands 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
// 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.
//
// TODO(user): Ideally, we should be able to extract any dimension like these
// (i.e. capacity, route_length, etc..) automatically from the encoding. The
// classical way to encode that is to have "current_capacity" variables along
// the route and linear equations of the form:
// arc_literal => (current_capacity_tail + demand <= current_capacity_head)
repeated int32 demands = 4;
int64 capacity = 5;
}
// 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: 30
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 or at_most_one. 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.
//
// This constraint does not support enforcement_literal. Just use a linear
// constraint if you need to enforce it. You also do not need to use it
// directly, we will extract it from the model in most situations.
BoolArgumentProto at_most_one = 26;
// The exactly_one constraint force exactly one literal to true and no more.
//
// Anytime a bool_or (it could have been called at_least_one) is included
// into an at_most_one, then the bool_or is actually an exactly one
// constraint, and the extra literal in the at_most_one can be set to false.
// So in this sense, this constraint is not really needed. it is just here
// for a better description of the problem structure and to facilitate some
// algorithm.
//
// This constraint does not support enforcement_literal. Just use a linear
// constraint if you need to enforce it. You also do not need to use it
// directly, we will extract it from the model in most situations.
BoolArgumentProto exactly_one = 29;
// 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_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_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.
//
// TODO(user): Support more than two terms in the product.
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 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 for variables[index], we will use
// positive_coeff * X + offset instead.
message AffineTransformation {
int32 index = 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 permutation of integers encoded as a list of cycles, hence the "sparse"
// format. The image of an element cycle[i] is cycle[(i + 1) % cycle_length].
message SparsePermutationProto {
// Each cycle is listed one after the other in the support field.
// The size of each cycle is given (in order) in the cycle_sizes field.
repeated int32 support = 1;
repeated int32 cycle_sizes = 2;
}
// A dense matrix of numbers encoded in a flat way, row by row.
// That is matrix[i][j] = entries[i * num_cols + j];
message DenseMatrixProto {
int32 num_rows = 1;
int32 num_cols = 2;
repeated int32 entries = 3;
}
// 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
// the variable values of any feasible solution using one of the permutation
// described here, we should always get another feasible solution.
//
// We usually also enforce that the objective of the new solution is the same.
//
// The group of permutations encoded here is usually computed from the encoding
// of the model, so it is not meant to be a complete representation of the
// feasible solution symmetries, just a valid subgroup.
message SymmetryProto {
// A list of variable indices permutations that leave the feasible space of
// solution invariant. Usually, we only encode a set of generators of the
// group.
repeated SparsePermutationProto permutations = 1;
// An orbitope is a special symmetry structure of the solution space. If the
// variable indices are arranged in a matrix (with no duplicates), then any
// permutation of the columns will be a valid permutation of the feasible
// space.
//
// This arise quite often. The typical example is a graph coloring problem
// where for each node i, you have j booleans to indicate its color. If the
// variables color_of_i_is_j are arranged in a matrix[i][j], then any columns
// permutations leave the problem invariant.
repeated DenseMatrixProto orbitopes = 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;
// For now, this is not meant to be filled by a client writing a model, but
// by our preprocessing step.
//
// Information about the symmetries of the feasible solution space.
// These usually leaves the objective invariant.
SymmetryProto symmetry = 8;
}
// 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 has 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: 27
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.
//
// 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.
//
// 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;
int64 num_restarts = 24;
int64 num_lp_iterations = 25;
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;
// The solve log will be filled if the parameter log_to_response is set to
// true.
string solve_log = 26;
}
src/cp_sat_wrapper.cpp
+75
View File
@@ -0,0 +1,75 @@
#include <iostream>
#include <ortools/sat/cp_model.h>
namespace sat = operations_research::sat;
extern "C" unsigned char*
cp_sat_wrapper_solve(
unsigned char* model_buf,
size_t model_size,
size_t* out_size)
{
sat::CpModelProto model;
bool res = model.ParseFromArray(model_buf, model_size);
assert(res);
sat::CpSolverResponse response = sat::Solve(model);
*out_size = response.ByteSizeLong();
unsigned char* out_buf = (unsigned char*) malloc(*out_size);
res = response.SerializeToArray(out_buf, *out_size);
assert(res);
return out_buf;
}
extern "C" unsigned char*
cp_sat_wrapper_solve_with_parameters(
unsigned char* model_buf,
size_t model_size,
unsigned char* params_buf,
size_t params_size,
size_t* out_size)
{
sat::CpModelProto model;
bool res = model.ParseFromArray(model_buf, model_size);
assert(res);
sat::SatParameters params;
res = model.ParseFromArray(params_buf, params_size);
assert(res);
sat::CpSolverResponse response = sat::SolveWithParameters(model, params);
*out_size = response.ByteSizeLong();
unsigned char* out_buf = (unsigned char*) malloc(*out_size);
res = response.SerializeToArray(out_buf, *out_size);
assert(res);
return out_buf;
}
extern "C" char*
cp_sat_wrapper_cp_model_stats(unsigned char* model_buf, size_t model_size) {
sat::CpModelProto model;
const bool res = model.ParseFromArray(model_buf, model_size);
assert(res);
const std::string stats = sat::CpModelStats(model);
return strdup(stats.c_str());
}
extern "C" char*
cp_sat_wrapper_cp_solver_response_stats(
unsigned char* response_buf,
size_t response_size,
bool has_objective)
{
sat::CpSolverResponse response;
const bool res = response.ParseFromArray(response_buf, response_size);
assert(res);
const std::string stats = sat::CpSolverResponseStats(response, has_objective);
return strdup(stats.c_str());
}
src/lib.rs
+94
View File
@@ -0,0 +1,94 @@
use libc::c_char;
use prost::Message;
use std::ffi::CStr;
pub mod proto {
include!(concat!(env!("OUT_DIR"), "/operations_research.sat.rs"));
}
extern "C" {
fn cp_sat_wrapper_solve(
model_buf: *const u8,
model_size: usize,
out_size: &mut usize,
) -> *mut u8;
fn cp_sat_wrapper_solve_with_parameters(
model_buf: *const u8,
model_size: usize,
params_buf: *const u8,
params_size: usize,
out_size: &mut usize,
) -> *mut u8;
fn cp_sat_wrapper_cp_model_stats(model_buf: *const u8, model_size: usize) -> *mut c_char;
fn cp_sat_wrapper_cp_solver_response_stats(
response_buf: *const u8,
response_size: usize,
has_objective: bool,
) -> *mut c_char;
}
pub fn solve(model: &proto::CpModelProto) -> proto::CpSolverResponse {
let mut buf = Vec::default();
model.encode(&mut buf).unwrap();
let mut out_size = 0;
let res = unsafe { cp_sat_wrapper_solve(buf.as_ptr(), buf.len(), &mut out_size) };
let out_slice = unsafe { std::slice::from_raw_parts(res, out_size) };
let response = proto::CpSolverResponse::decode(out_slice).unwrap();
unsafe { libc::free(res as _) };
response
}
pub fn solve_with_parameters(
model: &proto::CpModelProto,
params: &proto::SatParameters,
) -> proto::CpSolverResponse {
let mut model_buf = Vec::default();
model.encode(&mut model_buf).unwrap();
let mut params_buf = Vec::default();
params.encode(&mut params_buf).unwrap();
let mut out_size = 0;
let res = unsafe {
cp_sat_wrapper_solve_with_parameters(
model_buf.as_ptr(),
model_buf.len(),
params_buf.as_ptr(),
params_buf.len(),
&mut out_size,
)
};
let out_slice = unsafe { std::slice::from_raw_parts(res, out_size) };
let response = proto::CpSolverResponse::decode(out_slice).unwrap();
unsafe { libc::free(res as _) };
response
}
pub fn cp_model_stats(model: &proto::CpModelProto) -> String {
let mut model_buf = Vec::default();
model.encode(&mut model_buf).unwrap();
let char_ptr = unsafe { cp_sat_wrapper_cp_model_stats(model_buf.as_ptr(), model_buf.len()) };
let res = unsafe { CStr::from_ptr(char_ptr) }
.to_str()
.unwrap()
.to_owned();
unsafe { libc::free(char_ptr as _) };
res
}
pub fn cp_solver_response_stats(response: &proto::CpSolverResponse, has_objective: bool) -> String {
let mut response_buf = Vec::default();
response.encode(&mut response_buf).unwrap();
let char_ptr = unsafe {
cp_sat_wrapper_cp_solver_response_stats(
response_buf.as_ptr(),
response_buf.len(),
has_objective,
)
};
let res = unsafe { CStr::from_ptr(char_ptr) }
.to_str()
.unwrap()
.to_owned();
unsafe { libc::free(char_ptr as _) };
res
}
src/sat_parameters.proto
+1038
View File
File diff suppressed because it is too large Load Diff