forked from google/or-tools
-
Notifications
You must be signed in to change notification settings - Fork 0
/
cp_model.proto
646 lines (561 loc) · 25.8 KB
/
cp_model.proto
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
// 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;
}