OR-Tools  8.2
cp_model_fz_solver.cc
Go to the documentation of this file.
1// Copyright 2010-2018 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include <atomic>
17#include <cmath>
18#include <limits>
19#include <tuple>
20
21#include "absl/container/flat_hash_map.h"
22#include "absl/strings/str_cat.h"
23#include "absl/strings/str_format.h"
24#include "absl/strings/str_split.h"
25#include "absl/synchronization/mutex.h"
26#include "google/protobuf/text_format.h"
30#include "ortools/base/timer.h"
35#include "ortools/sat/cp_model.pb.h"
42#include "ortools/sat/integer.h"
45#include "ortools/sat/model.h"
48#include "ortools/sat/table.h"
49
50ABSL_FLAG(bool, use_flatzinc_format, true, "Output uses the flatzinc format");
51ABSL_FLAG(int64, fz_int_max, int64{1} << 50,
52 "Default max value for unbounded integer variables.");
53
54namespace operations_research {
55namespace sat {
56
57namespace {
58
59// Returns the true/false literal corresponding to a CpModelProto variable.
60int TrueLiteral(int var) { return var; }
61int FalseLiteral(int var) { return -var - 1; }
62int NegatedCpModelVariable(int var) { return -var - 1; }
63
64// Helper class to convert a flatzinc model to a CpModelProto.
65struct CpModelProtoWithMapping {
66 // Returns a constant CpModelProto variable created on-demand.
67 int LookupConstant(int64 value);
68
69 // Convert a flatzinc argument to a variable or a list of variable.
70 // Note that we always encode a constant argument with a constant variable.
71 int LookupVar(const fz::Argument& argument);
72 std::vector<int> LookupVars(const fz::Argument& argument);
73
74 // Create and return the indices of the IntervalConstraint corresponding
75 // to the flatzinc "interval" specified by a start var and a duration var.
76 // This method will cache intervals with the key <start, duration>.
77 std::vector<int> CreateIntervals(const std::vector<int>& starts,
78 const std::vector<int>& durations);
79
80 // Create and return the index of the IntervalConstraint corresponding
81 // to the flatzinc "interval" specified by a start var and a size var.
82 // This method will cache intervals with the key <start_var, size_var>.
83 int GetOrCreateInterval(int start_var, int size_var);
84
85 // Create and return the index of the optional IntervalConstraint
86 // corresponding to the flatzinc "interval" specified by a start var, the
87 // size_var, and the Boolean opt_var. This method will cache intervals with
88 // the key <start, duration, opt_var>.
89 int GetOrCreateOptionalInterval(int start_var, int size_var, int opt_var);
90
91 // Helpers to fill a ConstraintProto.
92 void FillAMinusBInDomain(const std::vector<int64>& domain,
93 const fz::Constraint& fz_ct, ConstraintProto* ct);
94 void FillLinearConstraintWithGivenDomain(const std::vector<int64>& domain,
95 const fz::Constraint& fz_ct,
96 ConstraintProto* ct);
97 void FillConstraint(const fz::Constraint& fz_ct, ConstraintProto* ct);
98 void FillReifOrImpliedConstraint(const fz::Constraint& fz_ct,
99 ConstraintProto* ct);
100
101 // Translates the flatzinc search annotations into the CpModelProto
102 // search_order field.
103 void TranslateSearchAnnotations(
104 const std::vector<fz::Annotation>& search_annotations);
105
106 // The output proto.
107 CpModelProto proto;
108 SatParameters parameters;
109
110 // Mapping from flatzinc variables to CpModelProto variables.
111 absl::flat_hash_map<fz::IntegerVariable*, int> fz_var_to_index;
112 absl::flat_hash_map<int64, int> constant_value_to_index;
113 absl::flat_hash_map<std::tuple<int, int, int>, int>
115};
116
117int CpModelProtoWithMapping::LookupConstant(int64 value) {
120 }
121
122 // Create the constant on the fly.
123 const int index = proto.variables_size();
124 IntegerVariableProto* var_proto = proto.add_variables();
125 var_proto->add_domain(value);
126 var_proto->add_domain(value);
128 return index;
129}
130
131int CpModelProtoWithMapping::LookupVar(const fz::Argument& argument) {
132 if (argument.HasOneValue()) return LookupConstant(argument.Value());
133 CHECK_EQ(argument.type, fz::Argument::INT_VAR_REF);
134 return fz_var_to_index[argument.Var()];
135}
136
137std::vector<int> CpModelProtoWithMapping::LookupVars(
138 const fz::Argument& argument) {
139 std::vector<int> result;
140 if (argument.type == fz::Argument::VOID_ARGUMENT) return result;
141 if (argument.type == fz::Argument::INT_LIST) {
142 for (int64 value : argument.values) {
143 result.push_back(LookupConstant(value));
144 }
145 } else if (argument.type == fz::Argument::INT_VALUE) {
146 result.push_back(LookupConstant(argument.Value()));
147 } else {
149 for (fz::IntegerVariable* var : argument.variables) {
150 CHECK(var != nullptr);
151 result.push_back(fz_var_to_index[var]);
152 }
153 }
154 return result;
155}
156
157int CpModelProtoWithMapping::GetOrCreateInterval(int start_var, int size_var) {
158 return GetOrCreateOptionalInterval(start_var, size_var, kint32max);
159}
160
161int CpModelProtoWithMapping::GetOrCreateOptionalInterval(int start_var,
162 int size_var,
163 int opt_var) {
164 const std::tuple<int, int, int> key =
165 std::make_tuple(start_var, size_var, opt_var);
168 }
169 const int interval_index = proto.constraints_size();
170
171 auto* ct = proto.add_constraints();
172 if (opt_var != kint32max) {
173 ct->add_enforcement_literal(opt_var);
174 }
175 auto* interval = ct->mutable_interval();
176 interval->set_start(start_var);
177 interval->set_size(size_var);
178
179 interval->set_end(proto.variables_size());
180 auto* end_var = proto.add_variables();
181 const auto start_proto = proto.variables(start_var);
182 const auto size_proto = proto.variables(size_var);
183 end_var->add_domain(start_proto.domain(0) + size_proto.domain(0));
184 end_var->add_domain(start_proto.domain(start_proto.domain_size() - 1) +
185 size_proto.domain(size_proto.domain_size() - 1));
186 start_size_opt_tuple_to_interval[key] = interval_index;
187 return interval_index;
188}
189
190std::vector<int> CpModelProtoWithMapping::CreateIntervals(
191 const std::vector<int>& starts, const std::vector<int>& durations) {
192 std::vector<int> intervals;
193 for (int i = 0; i < starts.size(); ++i) {
194 intervals.push_back(GetOrCreateInterval(starts[i], durations[i]));
195 }
196 return intervals;
197}
198
199void CpModelProtoWithMapping::FillAMinusBInDomain(
200 const std::vector<int64>& domain, const fz::Constraint& fz_ct,
201 ConstraintProto* ct) {
202 auto* arg = ct->mutable_linear();
203 if (fz_ct.arguments[1].type == fz::Argument::INT_VALUE) {
204 const int64 value = fz_ct.arguments[1].Value();
205 const int var_a = LookupVar(fz_ct.arguments[0]);
206 for (const int64 domain_bound : domain) {
207 if (domain_bound == kint64min || domain_bound == kint64max) {
208 arg->add_domain(domain_bound);
209 } else {
210 arg->add_domain(domain_bound + value);
211 }
212 }
213 arg->add_vars(var_a);
214 arg->add_coeffs(1);
215 } else if (fz_ct.arguments[0].type == fz::Argument::INT_VALUE) {
216 const int64 value = fz_ct.arguments[0].Value();
217 const int var_b = LookupVar(fz_ct.arguments[1]);
218 for (int64 domain_bound : gtl::reversed_view(domain)) {
219 if (domain_bound == kint64min) {
220 arg->add_domain(kint64max);
221 } else if (domain_bound == kint64max) {
222 arg->add_domain(kint64min);
223 } else {
224 arg->add_domain(value - domain_bound);
225 }
226 }
227 arg->add_vars(var_b);
228 arg->add_coeffs(1);
229 } else {
230 for (const int64 domain_bound : domain) arg->add_domain(domain_bound);
231 arg->add_vars(LookupVar(fz_ct.arguments[0]));
232 arg->add_coeffs(1);
233 arg->add_vars(LookupVar(fz_ct.arguments[1]));
234 arg->add_coeffs(-1);
235 }
236}
237
238void CpModelProtoWithMapping::FillLinearConstraintWithGivenDomain(
239 const std::vector<int64>& domain, const fz::Constraint& fz_ct,
240 ConstraintProto* ct) {
241 auto* arg = ct->mutable_linear();
242 for (const int64 domain_bound : domain) arg->add_domain(domain_bound);
243 std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
244 for (int i = 0; i < vars.size(); ++i) {
245 arg->add_vars(vars[i]);
246 arg->add_coeffs(fz_ct.arguments[0].values[i]);
247 }
248}
249
250void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
251 ConstraintProto* ct) {
252 if (fz_ct.type == "false_constraint") {
253 // An empty clause is always false.
254 ct->mutable_bool_or();
255 } else if (fz_ct.type == "bool_clause") {
256 auto* arg = ct->mutable_bool_or();
257 for (const int var : LookupVars(fz_ct.arguments[0])) {
258 arg->add_literals(TrueLiteral(var));
259 }
260 for (const int var : LookupVars(fz_ct.arguments[1])) {
261 arg->add_literals(FalseLiteral(var));
262 }
263 } else if (fz_ct.type == "bool_xor") {
264 // This is not the same semantics as the array_bool_xor as this constraint
265 // is actually a fully reified xor(a, b) <==> x.
266 const int a = LookupVar(fz_ct.arguments[0]);
267 const int b = LookupVar(fz_ct.arguments[1]);
268 const int x = LookupVar(fz_ct.arguments[2]);
269
270 // not(x) => a == b
271 ct->add_enforcement_literal(NegatedRef(x));
272 auto* const refute = ct->mutable_linear();
273 refute->add_vars(a);
274 refute->add_coeffs(1);
275 refute->add_vars(b);
276 refute->add_coeffs(-1);
277 refute->add_domain(0);
278 refute->add_domain(0);
279
280 // x => a + b == 1
281 auto* ct2 = proto.add_constraints();
282 ct2->add_enforcement_literal(x);
283 auto* const enforce = ct2->mutable_linear();
284 enforce->add_vars(a);
285 enforce->add_coeffs(1);
286 enforce->add_vars(b);
287 enforce->add_coeffs(1);
288 enforce->add_domain(1);
289 enforce->add_domain(1);
290 } else if (fz_ct.type == "array_bool_or") {
291 auto* arg = ct->mutable_bool_or();
292 for (const int var : LookupVars(fz_ct.arguments[0])) {
293 arg->add_literals(TrueLiteral(var));
294 }
295 } else if (fz_ct.type == "array_bool_or_negated") {
296 auto* arg = ct->mutable_bool_and();
297 for (const int var : LookupVars(fz_ct.arguments[0])) {
298 arg->add_literals(FalseLiteral(var));
299 }
300 } else if (fz_ct.type == "array_bool_and") {
301 auto* arg = ct->mutable_bool_and();
302 for (const int var : LookupVars(fz_ct.arguments[0])) {
303 arg->add_literals(TrueLiteral(var));
304 }
305 } else if (fz_ct.type == "array_bool_and_negated") {
306 auto* arg = ct->mutable_bool_or();
307 for (const int var : LookupVars(fz_ct.arguments[0])) {
308 arg->add_literals(FalseLiteral(var));
309 }
310 } else if (fz_ct.type == "array_bool_xor") {
311 auto* arg = ct->mutable_bool_xor();
312 for (const int var : LookupVars(fz_ct.arguments[0])) {
313 arg->add_literals(TrueLiteral(var));
314 }
315 } else if (fz_ct.type == "bool_le" || fz_ct.type == "int_le") {
316 FillAMinusBInDomain({kint64min, 0}, fz_ct, ct);
317 } else if (fz_ct.type == "bool_ge" || fz_ct.type == "int_ge") {
318 FillAMinusBInDomain({0, kint64max}, fz_ct, ct);
319 } else if (fz_ct.type == "bool_lt" || fz_ct.type == "int_lt") {
320 FillAMinusBInDomain({kint64min, -1}, fz_ct, ct);
321 } else if (fz_ct.type == "bool_gt" || fz_ct.type == "int_gt") {
322 FillAMinusBInDomain({1, kint64max}, fz_ct, ct);
323 } else if (fz_ct.type == "bool_eq" || fz_ct.type == "int_eq" ||
324 fz_ct.type == "bool2int") {
325 FillAMinusBInDomain({0, 0}, fz_ct, ct);
326 } else if (fz_ct.type == "bool_ne" || fz_ct.type == "bool_not") {
327 auto* arg = ct->mutable_linear();
328 arg->add_vars(LookupVar(fz_ct.arguments[0]));
329 arg->add_coeffs(1);
330 arg->add_vars(LookupVar(fz_ct.arguments[1]));
331 arg->add_coeffs(1);
332 arg->add_domain(1);
333 arg->add_domain(1);
334 } else if (fz_ct.type == "int_ne") {
335 FillAMinusBInDomain({kint64min, -1, 1, kint64max}, fz_ct, ct);
336 } else if (fz_ct.type == "int_lin_eq") {
337 const int64 rhs = fz_ct.arguments[2].values[0];
338 FillLinearConstraintWithGivenDomain({rhs, rhs}, fz_ct, ct);
339 } else if (fz_ct.type == "bool_lin_eq") {
340 auto* arg = ct->mutable_linear();
341 const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
342 for (int i = 0; i < vars.size(); ++i) {
343 arg->add_vars(vars[i]);
344 arg->add_coeffs(fz_ct.arguments[0].values[i]);
345 }
346 if (fz_ct.arguments[2].IsVariable()) {
347 arg->add_vars(LookupVar(fz_ct.arguments[2]));
348 arg->add_coeffs(-1);
349 arg->add_domain(0);
350 arg->add_domain(0);
351 } else {
352 const int64 v = fz_ct.arguments[2].Value();
353 arg->add_domain(v);
354 arg->add_domain(v);
355 }
356 } else if (fz_ct.type == "int_lin_le" || fz_ct.type == "bool_lin_le") {
357 const int64 rhs = fz_ct.arguments[2].values[0];
358 FillLinearConstraintWithGivenDomain({kint64min, rhs}, fz_ct, ct);
359 } else if (fz_ct.type == "int_lin_lt") {
360 const int64 rhs = fz_ct.arguments[2].values[0];
361 FillLinearConstraintWithGivenDomain({kint64min, rhs - 1}, fz_ct, ct);
362 } else if (fz_ct.type == "int_lin_ge") {
363 const int64 rhs = fz_ct.arguments[2].values[0];
364 FillLinearConstraintWithGivenDomain({rhs, kint64max}, fz_ct, ct);
365 } else if (fz_ct.type == "int_lin_gt") {
366 const int64 rhs = fz_ct.arguments[2].values[0];
367 FillLinearConstraintWithGivenDomain({rhs + 1, kint64max}, fz_ct, ct);
368 } else if (fz_ct.type == "int_lin_ne") {
369 const int64 rhs = fz_ct.arguments[2].values[0];
370 FillLinearConstraintWithGivenDomain(
371 {kint64min, rhs - 1, rhs + 1, kint64max}, fz_ct, ct);
372 } else if (fz_ct.type == "set_in") {
373 auto* arg = ct->mutable_linear();
374 arg->add_vars(LookupVar(fz_ct.arguments[0]));
375 arg->add_coeffs(1);
376 if (fz_ct.arguments[1].type == fz::Argument::INT_LIST) {
377 FillDomainInProto(Domain::FromValues(std::vector<int64>{
378 fz_ct.arguments[1].values.begin(),
379 fz_ct.arguments[1].values.end()}),
380 arg);
381 } else if (fz_ct.arguments[1].type == fz::Argument::INT_INTERVAL) {
383 Domain(fz_ct.arguments[1].values[0], fz_ct.arguments[1].values[1]),
384 arg);
385 } else {
386 LOG(FATAL) << "Wrong format";
387 }
388 } else if (fz_ct.type == "set_in_negated") {
389 auto* arg = ct->mutable_linear();
390 arg->add_vars(LookupVar(fz_ct.arguments[0]));
391 arg->add_coeffs(1);
392 if (fz_ct.arguments[1].type == fz::Argument::INT_LIST) {
395 std::vector<int64>{fz_ct.arguments[1].values.begin(),
396 fz_ct.arguments[1].values.end()})
397 .Complement(),
398 arg);
399 } else if (fz_ct.arguments[1].type == fz::Argument::INT_INTERVAL) {
401 Domain(fz_ct.arguments[1].values[0], fz_ct.arguments[1].values[1])
402 .Complement(),
403 arg);
404 } else {
405 LOG(FATAL) << "Wrong format";
406 }
407 } else if (fz_ct.type == "int_min") {
408 auto* arg = ct->mutable_int_min();
409 arg->set_target(LookupVar(fz_ct.arguments[2]));
410 arg->add_vars(LookupVar(fz_ct.arguments[0]));
411 arg->add_vars(LookupVar(fz_ct.arguments[1]));
412 } else if (fz_ct.type == "array_int_minimum" || fz_ct.type == "minimum_int") {
413 auto* arg = ct->mutable_int_min();
414 arg->set_target(LookupVar(fz_ct.arguments[0]));
415 for (const int var : LookupVars(fz_ct.arguments[1])) arg->add_vars(var);
416 } else if (fz_ct.type == "int_max") {
417 auto* arg = ct->mutable_int_max();
418 arg->set_target(LookupVar(fz_ct.arguments[2]));
419 arg->add_vars(LookupVar(fz_ct.arguments[0]));
420 arg->add_vars(LookupVar(fz_ct.arguments[1]));
421 } else if (fz_ct.type == "array_int_maximum" || fz_ct.type == "maximum_int") {
422 auto* arg = ct->mutable_int_max();
423 arg->set_target(LookupVar(fz_ct.arguments[0]));
424 for (const int var : LookupVars(fz_ct.arguments[1])) arg->add_vars(var);
425 } else if (fz_ct.type == "int_times") {
426 auto* arg = ct->mutable_int_prod();
427 arg->set_target(LookupVar(fz_ct.arguments[2]));
428 arg->add_vars(LookupVar(fz_ct.arguments[0]));
429 arg->add_vars(LookupVar(fz_ct.arguments[1]));
430 } else if (fz_ct.type == "int_abs") {
431 auto* arg = ct->mutable_int_max();
432 arg->set_target(LookupVar(fz_ct.arguments[1]));
433 arg->add_vars(LookupVar(fz_ct.arguments[0]));
434 arg->add_vars(-LookupVar(fz_ct.arguments[0]) - 1);
435 } else if (fz_ct.type == "int_plus") {
436 auto* arg = ct->mutable_linear();
437 FillDomainInProto(Domain(0, 0), arg);
438 arg->add_vars(LookupVar(fz_ct.arguments[0]));
439 arg->add_coeffs(1);
440 arg->add_vars(LookupVar(fz_ct.arguments[1]));
441 arg->add_coeffs(1);
442 arg->add_vars(LookupVar(fz_ct.arguments[2]));
443 arg->add_coeffs(-1);
444 } else if (fz_ct.type == "int_div") {
445 auto* arg = ct->mutable_int_div();
446 arg->add_vars(LookupVar(fz_ct.arguments[0]));
447 arg->add_vars(LookupVar(fz_ct.arguments[1]));
448 arg->set_target(LookupVar(fz_ct.arguments[2]));
449 } else if (fz_ct.type == "int_mod") {
450 auto* arg = ct->mutable_int_mod();
451 arg->set_target(LookupVar(fz_ct.arguments[2]));
452 arg->add_vars(LookupVar(fz_ct.arguments[0]));
453 arg->add_vars(LookupVar(fz_ct.arguments[1]));
454 } else if (fz_ct.type == "array_int_element" ||
455 fz_ct.type == "array_bool_element" ||
456 fz_ct.type == "array_var_int_element" ||
457 fz_ct.type == "array_var_bool_element" ||
458 fz_ct.type == "array_int_element_nonshifted") {
459 if (fz_ct.arguments[0].type == fz::Argument::INT_VAR_REF ||
460 fz_ct.arguments[0].type == fz::Argument::INT_VALUE) {
461 auto* arg = ct->mutable_element();
462 arg->set_index(LookupVar(fz_ct.arguments[0]));
463 arg->set_target(LookupVar(fz_ct.arguments[2]));
464
465 if (!absl::EndsWith(fz_ct.type, "_nonshifted")) {
466 // Add a dummy variable at position zero because flatzinc index start
467 // at 1.
468 // TODO(user): Make sure that zero is not in the index domain...
469 arg->add_vars(arg->target());
470 }
471 for (const int var : LookupVars(fz_ct.arguments[1])) arg->add_vars(var);
472 } else {
473 // Special case added by the presolve or in flatzinc. We encode this
474 // as a table constraint.
475 CHECK(!absl::EndsWith(fz_ct.type, "_nonshifted"));
476 auto* arg = ct->mutable_table();
477
478 // the constraint is:
479 // values[coeff1 * vars[0] + coeff2 * vars[1] + offset] == target.
480 for (const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(var);
481 arg->add_vars(LookupVar(fz_ct.arguments[2])); // the target
482
483 const std::vector<int64>& values = fz_ct.arguments[1].values;
484 const int64 coeff1 = fz_ct.arguments[3].values[0];
485 const int64 coeff2 = fz_ct.arguments[3].values[1];
486 const int64 offset = fz_ct.arguments[4].values[0] - 1;
487
488 for (const int64 a : AllValuesInDomain(proto.variables(arg->vars(0)))) {
489 for (const int64 b : AllValuesInDomain(proto.variables(arg->vars(1)))) {
490 const int index = coeff1 * a + coeff2 * b + offset;
491 CHECK_GE(index, 0);
492 CHECK_LT(index, values.size());
493 arg->add_values(a);
494 arg->add_values(b);
495 arg->add_values(values[index]);
496 }
497 }
498 }
499 } else if (fz_ct.type == "ortools_table_int") {
500 auto* arg = ct->mutable_table();
501 for (const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(var);
502 for (const int64 value : fz_ct.arguments[1].values) arg->add_values(value);
503 } else if (fz_ct.type == "ortools_regular") {
504 auto* arg = ct->mutable_automaton();
505 for (const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(var);
506
507 int count = 0;
508 const int num_states = fz_ct.arguments[1].Value();
509 const int num_values = fz_ct.arguments[2].Value();
510 for (int i = 1; i <= num_states; ++i) {
511 for (int j = 1; j <= num_values; ++j) {
512 CHECK_LT(count, fz_ct.arguments[3].values.size());
513 const int next = fz_ct.arguments[3].values[count++];
514 if (next == 0) continue; // 0 is a failing state.
515 arg->add_transition_tail(i);
516 arg->add_transition_label(j);
517 arg->add_transition_head(next);
518 }
519 }
520
521 arg->set_starting_state(fz_ct.arguments[4].Value());
522 switch (fz_ct.arguments[5].type) {
524 arg->add_final_states(fz_ct.arguments[5].values[0]);
525 break;
526 }
528 for (int v = fz_ct.arguments[5].values[0];
529 v <= fz_ct.arguments[5].values[1]; ++v) {
530 arg->add_final_states(v);
531 }
532 break;
533 }
535 for (const int v : fz_ct.arguments[5].values) {
536 arg->add_final_states(v);
537 }
538 break;
539 }
540 default: {
541 LOG(FATAL) << "Wrong constraint " << fz_ct.DebugString();
542 }
543 }
544 } else if (fz_ct.type == "fzn_all_different_int") {
545 auto* arg = ct->mutable_all_diff();
546 for (const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(var);
547 } else if (fz_ct.type == "fzn_circuit" || fz_ct.type == "fzn_subcircuit") {
548 // Try to auto-detect if it is zero or one based.
549 bool found_zero = false;
550 bool found_size = false;
551 int64 size = 0;
552 if (fz_ct.arguments[0].variables.empty() &&
553 !fz_ct.arguments[0].values.empty()) {
554 // Fully instantiated (sub)circuit constraints.
555 size = fz_ct.arguments[0].values.size();
556 for (const int64 value : fz_ct.arguments[0].values) {
557 if (value == 0) found_zero = true;
558 if (value == size) found_size = true;
559 }
560 } else {
561 size = fz_ct.arguments[0].variables.size();
562 for (fz::IntegerVariable* const var : fz_ct.arguments[0].variables) {
563 if (var->domain.Min() == 0) found_zero = true;
564 if (var->domain.Max() == size) found_size = true;
565 }
566 }
567
568 const bool is_one_based = !found_zero || found_size;
569 const int64 min_index = is_one_based ? 1 : 0;
570 const int64 max_index = min_index + size - 1;
571 // The arc-based mutable circuit.
572 auto* circuit_arg = ct->mutable_circuit();
573
574 // We fully encode all variables so we can use the literal based circuit.
575 // TODO(user): avoid fully encoding more than once?
576 int64 index = min_index;
577 const bool is_circuit = (fz_ct.type == "fzn_circuit");
578 for (const int var : LookupVars(fz_ct.arguments[0])) {
579 Domain domain = ReadDomainFromProto(proto.variables(var));
580
581 // Restrict the domain of var to [min_index, max_index]
582 domain = domain.IntersectionWith(Domain(min_index, max_index));
583 if (is_circuit) {
584 // We simply make sure that the variable cannot take the value index.
585 domain = domain.IntersectionWith(Domain::FromIntervals(
586 {{kint64min, index - 1}, {index + 1, kint64max}}));
587 }
588 FillDomainInProto(domain, proto.mutable_variables(var));
589
590 for (const ClosedInterval interval : domain.intervals()) {
591 for (int64 value = interval.start; value <= interval.end; ++value) {
592 // Create one Boolean variable for this arc.
593 const int literal = proto.variables_size();
594 {
595 auto* new_var = proto.add_variables();
596 new_var->add_domain(0);
597 new_var->add_domain(1);
598 }
599
600 // Add the arc.
601 circuit_arg->add_tails(index);
602 circuit_arg->add_heads(value);
603 circuit_arg->add_literals(literal);
604
605 // literal => var == value.
606 {
607 auto* ct = proto.add_constraints();
608 ct->add_enforcement_literal(literal);
609 ct->mutable_linear()->add_coeffs(1);
610 ct->mutable_linear()->add_vars(var);
611 ct->mutable_linear()->add_domain(value);
612 ct->mutable_linear()->add_domain(value);
613 }
614
615 // not(literal) => var != value
616 {
617 auto* ct = proto.add_constraints();
618 ct->add_enforcement_literal(NegatedRef(literal));
619 ct->mutable_linear()->add_coeffs(1);
620 ct->mutable_linear()->add_vars(var);
621 ct->mutable_linear()->add_domain(kint64min);
622 ct->mutable_linear()->add_domain(value - 1);
623 ct->mutable_linear()->add_domain(value + 1);
624 ct->mutable_linear()->add_domain(kint64max);
625 }
626 }
627 }
628
629 ++index;
630 }
631 } else if (fz_ct.type == "fzn_inverse") {
632 auto* arg = ct->mutable_inverse();
633
634 const auto direct_variables = LookupVars(fz_ct.arguments[0]);
635 const auto inverse_variables = LookupVars(fz_ct.arguments[1]);
636
637 const int num_variables =
638 std::min(direct_variables.size(), inverse_variables.size());
639
640 // Try to auto-detect if it is zero or one based.
641 bool found_zero = false;
642 bool found_size = false;
643 for (fz::IntegerVariable* const var : fz_ct.arguments[0].variables) {
644 if (var->domain.Min() == 0) found_zero = true;
645 if (var->domain.Max() == num_variables) found_size = true;
646 }
647 for (fz::IntegerVariable* const var : fz_ct.arguments[1].variables) {
648 if (var->domain.Min() == 0) found_zero = true;
649 if (var->domain.Max() == num_variables) found_size = true;
650 }
651
652 // Add a dummy constant variable at zero if the indexing is one based.
653 const bool is_one_based = !found_zero || found_size;
654 const int offset = is_one_based ? 1 : 0;
655
656 if (is_one_based) arg->add_f_direct(LookupConstant(0));
657 for (const int var : direct_variables) {
658 arg->add_f_direct(var);
659 // Intersect domains with offset + [0, num_variables).
661 ReadDomainFromProto(proto.variables(var))
662 .IntersectionWith(Domain(offset, num_variables - 1 + offset)),
663 proto.mutable_variables(var));
664 }
665
666 if (is_one_based) arg->add_f_inverse(LookupConstant(0));
667 for (const int var : inverse_variables) {
668 arg->add_f_inverse(var);
669 // Intersect domains with offset + [0, num_variables).
671 ReadDomainFromProto(proto.variables(var))
672 .IntersectionWith(Domain(offset, num_variables - 1 + offset)),
673 proto.mutable_variables(var));
674 }
675 } else if (fz_ct.type == "fzn_cumulative") {
676 const std::vector<int> starts = LookupVars(fz_ct.arguments[0]);
677 const std::vector<int> durations = LookupVars(fz_ct.arguments[1]);
678 const std::vector<int> demands = LookupVars(fz_ct.arguments[2]);
679 const int capacity = LookupVar(fz_ct.arguments[3]);
680
681 auto* arg = ct->mutable_cumulative();
682 arg->set_capacity(capacity);
683 for (int i = 0; i < starts.size(); ++i) {
684 // Special case for a 0-1 demand, we mark the interval as optional
685 // instead and fix the demand to 1.
686 if (proto.variables(demands[i]).domain().size() == 2 &&
687 proto.variables(demands[i]).domain(0) == 0 &&
688 proto.variables(demands[i]).domain(1) == 1 &&
689 proto.variables(capacity).domain(1) == 1) {
690 arg->add_intervals(
691 GetOrCreateOptionalInterval(starts[i], durations[i], demands[i]));
692 arg->add_demands(LookupConstant(1));
693 } else {
694 arg->add_intervals(GetOrCreateInterval(starts[i], durations[i]));
695 arg->add_demands(demands[i]);
696 }
697 }
698 } else if (fz_ct.type == "fzn_diffn" || fz_ct.type == "fzn_diffn_nonstrict") {
699 const std::vector<int> x = LookupVars(fz_ct.arguments[0]);
700 const std::vector<int> y = LookupVars(fz_ct.arguments[1]);
701 const std::vector<int> dx = LookupVars(fz_ct.arguments[2]);
702 const std::vector<int> dy = LookupVars(fz_ct.arguments[3]);
703 const std::vector<int> x_intervals = CreateIntervals(x, dx);
704 const std::vector<int> y_intervals = CreateIntervals(y, dy);
705 auto* arg = ct->mutable_no_overlap_2d();
706 for (int i = 0; i < x.size(); ++i) {
707 arg->add_x_intervals(x_intervals[i]);
708 arg->add_y_intervals(y_intervals[i]);
709 }
710 arg->set_boxes_with_null_area_can_overlap(fz_ct.type ==
711 "fzn_diffn_nonstrict");
712 } else if (fz_ct.type == "ortools_network_flow" ||
713 fz_ct.type == "ortools_network_flow_cost") {
714 // Note that we leave ct empty here (with just the name set).
715 // We simply do a linear encoding of this constraint.
716 const bool has_cost = fz_ct.type == "ortools_network_flow_cost";
717 const std::vector<int> flow = LookupVars(fz_ct.arguments[has_cost ? 3 : 2]);
718
719 // Flow conservation constraints.
720 const int num_nodes = fz_ct.arguments[1].values.size();
721 std::vector<std::vector<int>> flows_per_node(num_nodes);
722 std::vector<std::vector<int>> coeffs_per_node(num_nodes);
723 const int num_arcs = fz_ct.arguments[0].values.size() / 2;
724 for (int arc = 0; arc < num_arcs; arc++) {
725 const int tail = fz_ct.arguments[0].values[2 * arc] - 1;
726 const int head = fz_ct.arguments[0].values[2 * arc + 1] - 1;
727 if (tail == head) continue;
728
729 flows_per_node[tail].push_back(flow[arc]);
730 coeffs_per_node[tail].push_back(1);
731 flows_per_node[head].push_back(flow[arc]);
732 coeffs_per_node[head].push_back(-1);
733 }
734 for (int node = 0; node < num_nodes; node++) {
735 auto* arg = proto.add_constraints()->mutable_linear();
736 arg->add_domain(fz_ct.arguments[1].values[node]);
737 arg->add_domain(fz_ct.arguments[1].values[node]);
738 for (int i = 0; i < flows_per_node[node].size(); ++i) {
739 arg->add_vars(flows_per_node[node][i]);
740 arg->add_coeffs(coeffs_per_node[node][i]);
741 }
742 }
743
744 if (has_cost) {
745 auto* arg = proto.add_constraints()->mutable_linear();
746 arg->add_domain(0);
747 arg->add_domain(0);
748 for (int arc = 0; arc < num_arcs; arc++) {
749 const int64 weight = fz_ct.arguments[2].values[arc];
750 if (weight != 0) {
751 arg->add_vars(flow[arc]);
752 arg->add_coeffs(weight);
753 }
754 }
755 arg->add_vars(LookupVar(fz_ct.arguments[4]));
756 arg->add_coeffs(-1);
757 }
758 } else {
759 LOG(FATAL) << " Not supported " << fz_ct.type;
760 }
761}
762
763void CpModelProtoWithMapping::FillReifOrImpliedConstraint(
764 const fz::Constraint& fz_ct, ConstraintProto* ct) {
765 // Start by adding a non-reified version of the same constraint.
766 std::string simplified_type;
767 if (absl::EndsWith(fz_ct.type, "_reif")) {
768 // Remove _reif.
769 simplified_type = fz_ct.type.substr(0, fz_ct.type.size() - 5);
770 } else if (absl::EndsWith(fz_ct.type, "_imp")) {
771 // Remove _imp.
772 simplified_type = fz_ct.type.substr(0, fz_ct.type.size() - 4);
773 } else {
774 // Keep name as it is an implicit reified constraint.
775 simplified_type = fz_ct.type;
776 }
777
778 // We need a copy to be able to change the type of the constraint.
779 fz::Constraint copy = fz_ct;
780 copy.type = simplified_type;
781
782 // Create the CP-SAT constraint.
783 FillConstraint(copy, ct);
784
785 // In case of reified constraints, the type of the opposite constraint.
786 std::string negated_type;
787
788 // Fill enforcement_literal and set copy.type to the negated constraint.
789 if (simplified_type == "array_bool_or") {
790 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[1])));
791 negated_type = "array_bool_or_negated";
792 } else if (simplified_type == "array_bool_and") {
793 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[1])));
794 negated_type = "array_bool_and_negated";
795 } else if (simplified_type == "set_in") {
796 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
797 negated_type = "set_in_negated";
798 } else if (simplified_type == "bool_eq" || simplified_type == "int_eq") {
799 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
800 negated_type = "int_ne";
801 } else if (simplified_type == "bool_ne" || simplified_type == "int_ne") {
802 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
803 negated_type = "int_eq";
804 } else if (simplified_type == "bool_le" || simplified_type == "int_le") {
805 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
806 negated_type = "int_gt";
807 } else if (simplified_type == "bool_lt" || simplified_type == "int_lt") {
808 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
809 negated_type = "int_ge";
810 } else if (simplified_type == "bool_ge" || simplified_type == "int_ge") {
811 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
812 negated_type = "int_lt";
813 } else if (simplified_type == "bool_gt" || simplified_type == "int_gt") {
814 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
815 negated_type = "int_le";
816 } else if (simplified_type == "int_lin_eq") {
817 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
818 negated_type = "int_lin_ne";
819 } else if (simplified_type == "int_lin_ne") {
820 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
821 negated_type = "int_lin_eq";
822 } else if (simplified_type == "int_lin_le") {
823 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
824 negated_type = "int_lin_gt";
825 } else if (simplified_type == "int_lin_ge") {
826 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
827 negated_type = "int_lin_lt";
828 } else if (simplified_type == "int_lin_lt") {
829 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
830 negated_type = "int_lin_ge";
831 } else if (simplified_type == "int_lin_gt") {
832 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
833 negated_type = "int_lin_le";
834 } else {
835 LOG(FATAL) << "Unsupported " << simplified_type;
836 }
837
838 // One way implication. We can stop here.
839 if (absl::EndsWith(fz_ct.type, "_imp")) return;
840
841 // Add the other side of the reification because CpModelProto only support
842 // half reification.
843 ConstraintProto* negated_ct = proto.add_constraints();
844 negated_ct->set_name(fz_ct.type + " (negated)");
845 negated_ct->add_enforcement_literal(
846 sat::NegatedRef(ct->enforcement_literal(0)));
847 copy.type = negated_type;
848 FillConstraint(copy, negated_ct);
849}
850
851void CpModelProtoWithMapping::TranslateSearchAnnotations(
852 const std::vector<fz::Annotation>& search_annotations) {
853 std::vector<fz::Annotation> flat_annotations;
854 for (const fz::Annotation& annotation : search_annotations) {
855 fz::FlattenAnnotations(annotation, &flat_annotations);
856 }
857
858 for (const fz::Annotation& annotation : flat_annotations) {
859 if (annotation.IsFunctionCallWithIdentifier("int_search") ||
860 annotation.IsFunctionCallWithIdentifier("bool_search")) {
861 const std::vector<fz::Annotation>& args = annotation.annotations;
862 std::vector<fz::IntegerVariable*> vars;
863 args[0].AppendAllIntegerVariables(&vars);
864
865 DecisionStrategyProto* strategy = proto.add_search_strategy();
866 for (fz::IntegerVariable* v : vars) {
867 strategy->add_variables(gtl::FindOrDie(fz_var_to_index, v));
868 }
869
870 const fz::Annotation& choose = args[1];
871 if (choose.id == "input_order") {
872 strategy->set_variable_selection_strategy(
873 DecisionStrategyProto::CHOOSE_FIRST);
874 } else if (choose.id == "first_fail") {
875 strategy->set_variable_selection_strategy(
876 DecisionStrategyProto::CHOOSE_MIN_DOMAIN_SIZE);
877 } else if (choose.id == "anti_first_fail") {
878 strategy->set_variable_selection_strategy(
879 DecisionStrategyProto::CHOOSE_MAX_DOMAIN_SIZE);
880 } else if (choose.id == "smallest") {
881 strategy->set_variable_selection_strategy(
882 DecisionStrategyProto::CHOOSE_LOWEST_MIN);
883 } else if (choose.id == "largest") {
884 strategy->set_variable_selection_strategy(
885 DecisionStrategyProto::CHOOSE_HIGHEST_MAX);
886 } else {
887 LOG(FATAL) << "Unsupported order: " << choose.id;
888 }
889
890 const fz::Annotation& select = args[2];
891 if (select.id == "indomain_min" || select.id == "indomain") {
892 strategy->set_domain_reduction_strategy(
893 DecisionStrategyProto::SELECT_MIN_VALUE);
894 } else if (select.id == "indomain_max") {
895 strategy->set_domain_reduction_strategy(
896 DecisionStrategyProto::SELECT_MAX_VALUE);
897 } else if (select.id == "indomain_split") {
898 strategy->set_domain_reduction_strategy(
899 DecisionStrategyProto::SELECT_LOWER_HALF);
900 } else if (select.id == "indomain_reverse_split") {
901 strategy->set_domain_reduction_strategy(
902 DecisionStrategyProto::SELECT_UPPER_HALF);
903 } else if (select.id == "indomain_median") {
904 strategy->set_domain_reduction_strategy(
905 DecisionStrategyProto::SELECT_MEDIAN_VALUE);
906 } else {
907 LOG(FATAL) << "Unsupported select: " << select.id;
908 }
909 }
910 }
911}
912
913// The format is fixed in the flatzinc specification.
914std::string SolutionString(
915 const fz::SolutionOutputSpecs& output,
916 const std::function<int64(fz::IntegerVariable*)>& value_func) {
917 if (output.variable != nullptr) {
918 const int64 value = value_func(output.variable);
919 if (output.display_as_boolean) {
920 return absl::StrCat(output.name, " = ", value == 1 ? "true" : "false",
921 ";");
922 } else {
923 return absl::StrCat(output.name, " = ", value, ";");
924 }
925 } else {
926 const int bound_size = output.bounds.size();
927 std::string result =
928 absl::StrCat(output.name, " = array", bound_size, "d(");
929 for (int i = 0; i < bound_size; ++i) {
930 if (output.bounds[i].max_value >= output.bounds[i].min_value) {
931 absl::StrAppend(&result, output.bounds[i].min_value, "..",
932 output.bounds[i].max_value, ", ");
933 } else {
934 result.append("{},");
935 }
936 }
937 result.append("[");
938 for (int i = 0; i < output.flat_variables.size(); ++i) {
939 const int64 value = value_func(output.flat_variables[i]);
940 if (output.display_as_boolean) {
941 result.append(value ? "true" : "false");
942 } else {
943 absl::StrAppend(&result, value);
944 }
945 if (i != output.flat_variables.size() - 1) {
946 result.append(", ");
947 }
948 }
949 result.append("]);");
950 return result;
951 }
952 return "";
953}
954
955std::string SolutionString(
956 const fz::Model& model,
957 const std::function<int64(fz::IntegerVariable*)>& value_func) {
958 std::string solution_string;
959 for (const auto& output_spec : model.output()) {
960 solution_string.append(SolutionString(output_spec, value_func));
961 solution_string.append("\n");
962 }
963 return solution_string;
964}
965
966void LogInFlatzincFormat(const std::string& multi_line_input) {
967 std::vector<std::string> lines =
968 absl::StrSplit(multi_line_input, '\n', absl::SkipEmpty());
969 for (const std::string& line : lines) {
970 FZLOG << line << FZENDL;
971 }
972}
973
974void OutputFlatzincStats(const CpSolverResponse& response) {
975 std::cout << "%%%mzn-stat: objective=" << response.objective_value()
976 << std::endl;
977 std::cout << "%%%mzn-stat: objectiveBound=" << response.best_objective_bound()
978 << std::endl;
979 std::cout << "%%%mzn-stat: boolVariables=" << response.num_booleans()
980 << std::endl;
981 std::cout << "%%%mzn-stat: failures=" << response.num_conflicts()
982 << std::endl;
983 std::cout << "%%%mzn-stat: propagations="
984 << response.num_binary_propagations() +
985 response.num_integer_propagations()
986 << std::endl;
987 std::cout << "%%%mzn-stat: solveTime=" << response.wall_time() << std::endl;
988}
989
990} // namespace
991
994 const std::string& sat_params) {
995 if (!absl::GetFlag(FLAGS_use_flatzinc_format)) {
996 LOG(INFO) << "*** Starting translation to CP-SAT";
997 } else if (p.verbose_logging) {
998 FZLOG << "*** Starting translation to CP-SAT" << FZENDL;
999 }
1000
1001 CpModelProtoWithMapping m;
1002 m.proto.set_name(fz_model.name());
1003
1004 // The translation is easy, we create one variable per flatzinc variable,
1005 // plus eventually a bunch of constant variables that will be created
1006 // lazily.
1007 int num_variables = 0;
1008 for (fz::IntegerVariable* fz_var : fz_model.variables()) {
1009 if (!fz_var->active) continue;
1010 m.fz_var_to_index[fz_var] = num_variables++;
1011 IntegerVariableProto* var = m.proto.add_variables();
1012 var->set_name(fz_var->name);
1013 if (fz_var->domain.is_interval) {
1014 if (fz_var->domain.values.empty()) {
1015 // The CP-SAT solver checks that constraints cannot overflow during
1016 // their propagation. Because of that, we trim undefined variable
1017 // domains (i.e. int in minizinc) to something hopefully large enough.
1019 << "Using flag --fz_int_max for unbounded integer variables.";
1021 << " actual domain is [" << -absl::GetFlag(FLAGS_fz_int_max)
1022 << ".." << absl::GetFlag(FLAGS_fz_int_max) << "]";
1023 var->add_domain(-absl::GetFlag(FLAGS_fz_int_max));
1024 var->add_domain(absl::GetFlag(FLAGS_fz_int_max));
1025 } else {
1026 var->add_domain(fz_var->domain.values[0]);
1027 var->add_domain(fz_var->domain.values[1]);
1028 }
1029 } else {
1030 FillDomainInProto(Domain::FromValues(fz_var->domain.values), var);
1031 }
1032 }
1033
1034 // Translate the constraints.
1035 for (fz::Constraint* fz_ct : fz_model.constraints()) {
1036 if (fz_ct == nullptr || !fz_ct->active) continue;
1037 ConstraintProto* ct = m.proto.add_constraints();
1038 ct->set_name(fz_ct->type);
1039 if (absl::EndsWith(fz_ct->type, "_reif") ||
1040 absl::EndsWith(fz_ct->type, "_imp") || fz_ct->type == "array_bool_or" ||
1041 fz_ct->type == "array_bool_and") {
1042 m.FillReifOrImpliedConstraint(*fz_ct, ct);
1043 } else {
1044 m.FillConstraint(*fz_ct, ct);
1045 }
1046 }
1047
1048 // Fill the objective.
1049 if (fz_model.objective() != nullptr) {
1050 CpObjectiveProto* objective = m.proto.mutable_objective();
1051 objective->add_coeffs(1);
1052 if (fz_model.maximize()) {
1053 objective->set_scaling_factor(-1);
1054 objective->add_vars(
1055 NegatedCpModelVariable(m.fz_var_to_index[fz_model.objective()]));
1056 } else {
1057 objective->add_vars(m.fz_var_to_index[fz_model.objective()]);
1058 }
1059 }
1060
1061 // Fill the search order.
1062 m.TranslateSearchAnnotations(fz_model.search_annotations());
1063
1064 // Print model statistics.
1065 if (absl::GetFlag(FLAGS_use_flatzinc_format) && p.verbose_logging) {
1066 LogInFlatzincFormat(CpModelStats(m.proto));
1067 }
1068
1069 if (p.display_all_solutions && !m.proto.has_objective()) {
1070 // Enumerate all sat solutions.
1071 m.parameters.set_enumerate_all_solutions(true);
1072 }
1073 if (p.use_free_search) {
1074 m.parameters.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
1075 if (p.number_of_threads <= 1) {
1076 m.parameters.set_interleave_search(true);
1077 m.parameters.set_reduce_memory_usage_in_interleave_mode(true);
1078 }
1079 } else {
1080 m.parameters.set_search_branching(SatParameters::FIXED_SEARCH);
1081 }
1082 if (p.max_time_in_seconds > 0) {
1083 m.parameters.set_max_time_in_seconds(p.max_time_in_seconds);
1084 }
1085
1086 // We don't support enumerating all solution in parallel for a SAT problem.
1087 // But note that we do support it for an optimization problem since the
1088 // meaning of p.all_solutions is not the same in this case.
1089 if (p.display_all_solutions && fz_model.objective() == nullptr) {
1090 m.parameters.set_num_search_workers(1);
1091 } else {
1092 m.parameters.set_num_search_workers(std::max(1, p.number_of_threads));
1093 }
1094
1095 // The order is important, we want the flag parameters to overwrite anything
1096 // set in m.parameters.
1097 sat::SatParameters flag_parameters;
1098 CHECK(google::protobuf::TextFormat::ParseFromString(sat_params,
1099 &flag_parameters))
1100 << sat_params;
1101 m.parameters.MergeFrom(flag_parameters);
1102
1103 // We only need an observer if 'p.all_solutions' is true.
1104 std::function<void(const CpSolverResponse&)> solution_observer = nullptr;
1105 if (p.display_all_solutions && absl::GetFlag(FLAGS_use_flatzinc_format)) {
1106 solution_observer = [&fz_model, &m, &p](const CpSolverResponse& r) {
1107 const std::string solution_string =
1108 SolutionString(fz_model, [&m, &r](fz::IntegerVariable* v) {
1109 return r.solution(gtl::FindOrDie(m.fz_var_to_index, v));
1110 });
1111 std::cout << solution_string << std::endl;
1112 if (p.display_statistics && absl::GetFlag(FLAGS_use_flatzinc_format)) {
1113 OutputFlatzincStats(r);
1114 }
1115 std::cout << "----------" << std::endl;
1116 };
1117 }
1118
1119 Model sat_model;
1120 sat_model.Add(NewSatParameters(m.parameters));
1121 if (solution_observer != nullptr) {
1122 sat_model.Add(NewFeasibleSolutionObserver(solution_observer));
1123 }
1124 const CpSolverResponse response = SolveCpModel(m.proto, &sat_model);
1125
1126 // Check the returned solution with the fz model checker.
1127 if (response.status() == CpSolverStatus::FEASIBLE ||
1128 response.status() == CpSolverStatus::OPTIMAL) {
1129 CHECK(CheckSolution(fz_model, [&response, &m](fz::IntegerVariable* v) {
1130 return response.solution(gtl::FindOrDie(m.fz_var_to_index, v));
1131 }));
1132 }
1133
1134 // Output the solution in the flatzinc official format.
1135 if (absl::GetFlag(FLAGS_use_flatzinc_format)) {
1136 if (response.status() == CpSolverStatus::FEASIBLE ||
1137 response.status() == CpSolverStatus::OPTIMAL) {
1138 if (!p.display_all_solutions) { // Already printed otherwise.
1139 const std::string solution_string =
1140 SolutionString(fz_model, [&response, &m](fz::IntegerVariable* v) {
1141 return response.solution(gtl::FindOrDie(m.fz_var_to_index, v));
1142 });
1143 std::cout << solution_string << std::endl;
1144 std::cout << "----------" << std::endl;
1145 }
1146 if (response.status() == CpSolverStatus::OPTIMAL) {
1147 std::cout << "==========" << std::endl;
1148 }
1149 } else if (response.status() == CpSolverStatus::INFEASIBLE) {
1150 std::cout << "=====UNSATISFIABLE=====" << std::endl;
1151 } else if (response.status() == CpSolverStatus::MODEL_INVALID) {
1152 const std::string error_message = ValidateCpModel(m.proto);
1153 VLOG(1) << "%% Error message = '" << error_message << "'";
1154 if (absl::StrContains(error_message, "overflow")) {
1155 std::cout << "=====OVERFLOW=====" << std::endl;
1156 } else {
1157 std::cout << "=====MODEL INVALID=====" << std::endl;
1158 }
1159 } else {
1160 std::cout << "%% TIMEOUT" << std::endl;
1161 }
1162 if (p.display_statistics && absl::GetFlag(FLAGS_use_flatzinc_format)) {
1163 OutputFlatzincStats(response);
1164 }
1165 }
1166}
1167
1168} // namespace sat
1169} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define LOG_FIRST_N(severity, n)
Definition: base/logging.h:849
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_LT(val1, val2)
Definition: base/logging.h:700
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define LOG(severity)
Definition: base/logging.h:420
#define VLOG(verboselevel)
Definition: base/logging.h:978
static Domain FromValues(std::vector< int64 > values)
Creates a domain from the union of an unsorted list of integer values.
Domain IntersectionWith(const Domain &domain) const
Returns the intersection of D and domain.
static Domain FromIntervals(absl::Span< const ClosedInterval > intervals)
Creates a domain from the union of an unsorted list of intervals.
const std::string & name() const
const std::vector< Annotation > & search_annotations() const
const std::vector< IntegerVariable * > & variables() const
IntegerVariable * objective() const
const std::vector< Constraint * > & constraints() const
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
T Add(std::function< T(Model *)> f)
This makes it possible to have a nicer API on the client side, and it allows both of these forms:
Definition: sat/model.h:81
Block * next
SatParameters parameters
absl::flat_hash_map< fz::IntegerVariable *, int > fz_var_to_index
absl::flat_hash_map< std::tuple< int, int, int >, int > start_size_opt_tuple_to_interval
ABSL_FLAG(bool, use_flatzinc_format, true, "Output uses the flatzinc format")
absl::flat_hash_map< int64, int > constant_value_to_index
CpModelProto proto
SharedResponseManager * response
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
#define FZLOG
#define FZENDL
GRBmodel * model
static const int64 kint64max
int64_t int64
static const int32 kint32max
static const int64 kint64min
const int WARNING
Definition: log_severity.h:31
const int INFO
Definition: log_severity.h:31
const int FATAL
Definition: log_severity.h:32
ReverseView< Container > reversed_view(const Container &c)
const Collection::value_type::second_type & FindOrDie(const Collection &collection, const typename Collection::value_type::first_type &key)
Definition: map_util.h:176
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
void FlattenAnnotations(const Annotation &ann, std::vector< Annotation > *out)
Definition: model.cc:953
bool CheckSolution(const Model &model, const std::function< int64(IntegerVariable *)> &evaluator)
Definition: checker.cc:1263
std::function< void(Model *)> NewFeasibleSolutionObserver(const std::function< void(const CpSolverResponse &response)> &observer)
Creates a solution observer with the model with model.Add(NewFeasibleSolutionObserver([](response){....
std::function< SatParameters(Model *)> NewSatParameters(const std::string &params)
Creates parameters for the solver, which you can add to the model with.
std::vector< int64 > AllValuesInDomain(const ProtoWithDomain &proto)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
std::string CpModelStats(const CpModelProto &model_proto)
Returns a string with some statistics on the given CpModelProto.
CpSolverResponse SolveCpModel(const CpModelProto &model_proto, Model *model)
Solves the given CpModelProto.
void SolveFzWithCpModelProto(const fz::Model &fz_model, const fz::FlatzincSatParameters &p, const std::string &sat_params)
std::string ValidateCpModel(const CpModelProto &model)
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
int64 weight
Definition: pack.cc:509
IntervalVar * interval
Definition: resource.cc:98
int64 tail
int64 head
int64 capacity