Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
cp_model_fz_solver.cc
Go to the documentation of this file.
1// Copyright 2010-2025 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 <algorithm>
17#include <cstdint>
18#include <functional>
19#include <limits>
20#include <memory>
21#include <string>
22#include <tuple>
23#include <utility>
24#include <vector>
25
26#include "absl/container/flat_hash_map.h"
27#include "absl/container/flat_hash_set.h"
28#include "absl/flags/flag.h"
29#include "absl/log/check.h"
30#include "absl/log/log.h"
31#include "absl/strings/match.h"
32#include "absl/strings/str_cat.h"
33#include "absl/types/span.h"
34#include "google/protobuf/arena.h"
35#include "google/protobuf/text_format.h"
43#include "ortools/sat/model.h"
47
48ABSL_FLAG(int64_t, fz_int_max, int64_t{1} << 40,
49 "Default max value for unbounded integer variables.");
50ABSL_FLAG(bool, force_interleave_search, false,
51 "If true, enable interleaved workers when num_workers is 1.");
52
53namespace operations_research {
54namespace sat {
55
56namespace {
57
58static const int kNoVar = std::numeric_limits<int>::min();
59
60struct VarOrValue {
61 int var = kNoVar;
62 int64_t value = 0;
63};
64
65// Returns the true/false literal corresponding to a CpModelProto variable.
66int TrueLiteral(int var) { return var; }
67int FalseLiteral(int var) { return -var - 1; }
68
69// Helper class to convert a flatzinc model to a CpModelProto.
70struct CpModelProtoWithMapping {
71 CpModelProtoWithMapping()
72 : arena(std::make_unique<google::protobuf::Arena>()),
73 proto(*google::protobuf::Arena::Create<CpModelProto>(arena.get())) {}
74
75 // Returns a constant CpModelProto variable created on-demand.
76 int LookupConstant(int64_t value);
77
78 // Convert a flatzinc argument to a variable or a list of variable.
79 // Note that we always encode a constant argument with a constant variable.
80 int LookupVar(const fz::Argument& argument);
81 LinearExpressionProto LookupExpr(const fz::Argument& argument,
82 bool negate = false);
83 LinearExpressionProto LookupExprAt(const fz::Argument& argument, int pos,
84 bool negate = false);
85 std::vector<int> LookupVars(const fz::Argument& argument);
86 VarOrValue LookupVarOrValue(const fz::Argument& argument);
87 std::vector<VarOrValue> LookupVarsOrValues(const fz::Argument& argument);
88
89 // Get or create a literal that is equivalent tovar == value.
90 int GetOrCreateLiteralForVarEqValue(int var, int64_t value);
91
92 // Get or create a literal that is equivalent to var1 == var2.
93 int GetOrCreateLiteralForVarEqVar(int var1, int var2);
94
95 // Create and return the indices of the IntervalConstraint corresponding
96 // to the flatzinc "interval" specified by a start var and a size var.
97 // This method will cache intervals with the key <start, size>.
98 std::vector<int> CreateIntervals(absl::Span<const VarOrValue> starts,
99 absl::Span<const VarOrValue> sizes);
100
101 // Create and return the indices of the IntervalConstraint corresponding
102 // to the flatzinc "interval" specified by a start var and a size var.
103 // This method will cache intervals with the key <start, size>.
104 // This interval will be optional if the size can be 0.
105 // It also adds a constraint linking the enforcement literal with the size,
106 // stating that the interval will be performed if and only if the size is
107 // greater than 0.
108 std::vector<int> CreateNonZeroOrOptionalIntervals(
109 absl::Span<const VarOrValue> starts, absl::Span<const VarOrValue> sizes);
110
111 // Create and return the index of the optional IntervalConstraint
112 // corresponding to the flatzinc "interval" specified by a start var, the
113 // size_var, and the Boolean opt_var. This method will cache intervals with
114 // the key <start, size, opt_var>. If opt_var == kNoVar, the interval will not
115 // be optional.
116 int GetOrCreateOptionalInterval(VarOrValue start_var, VarOrValue size,
117 int opt_var);
118
119 // Get or Create a literal that implies the variable is > 0.
120 // Its negation implies the variable is == 0.
121 int NonZeroLiteralFrom(VarOrValue size);
122
123 // Adds a constraint to the model, add the enforcement literal if it is
124 // different from kNoVar, and returns a ptr to the ConstraintProto.
125 ConstraintProto* AddEnforcedConstraint(int literal);
126
127 // Helpers to fill a ConstraintProto.
128 void FillAMinusBInDomain(const std::vector<int64_t>& domain,
129 const fz::Constraint& fz_ct, ConstraintProto* ct);
130 void FillLinearConstraintWithGivenDomain(absl::Span<const int64_t> domain,
131 const fz::Constraint& fz_ct,
132 ConstraintProto* ct);
133 void FillConstraint(const fz::Constraint& fz_ct, ConstraintProto* ct);
134 void FillReifOrImpliedConstraint(const fz::Constraint& fz_ct,
135 ConstraintProto* ct);
136 void BuildTableFromDomainIntLinEq(const fz::Constraint& fz_ct,
137 ConstraintProto* ct);
138
139 // Translates the flatzinc search annotations into the CpModelProto
140 // search_order field.
141 void TranslateSearchAnnotations(
142 absl::Span<const fz::Annotation> search_annotations,
143 SolverLogger* logger);
144
145 // The output proto.
146 std::unique_ptr<google::protobuf::Arena> arena;
147 CpModelProto& proto;
148 SatParameters parameters;
149
150 // Mapping from flatzinc variables to CpModelProto variables.
151 absl::flat_hash_map<fz::Variable*, int> fz_var_to_index;
152 absl::flat_hash_map<int64_t, int> constant_value_to_index;
153 absl::flat_hash_map<std::tuple<int, int64_t, int, int64_t, int>, int>
154 interval_key_to_index;
155 absl::flat_hash_map<int, int> var_to_lit_implies_greater_than_zero;
156 absl::flat_hash_map<std::pair<int, int64_t>, int> var_eq_value_to_literal;
157 absl::flat_hash_map<std::pair<int, int>, int> var_eq_var_to_literal;
158};
159
160int CpModelProtoWithMapping::LookupConstant(int64_t value) {
161 if (constant_value_to_index.contains(value)) {
162 return constant_value_to_index[value];
163 }
164
165 // Create the constant on the fly.
166 const int index = proto.variables_size();
167 IntegerVariableProto* var_proto = proto.add_variables();
168 var_proto->add_domain(value);
169 var_proto->add_domain(value);
170 constant_value_to_index[value] = index;
171 return index;
172}
173
174int CpModelProtoWithMapping::LookupVar(const fz::Argument& argument) {
175 if (argument.HasOneValue()) return LookupConstant(argument.Value());
176 CHECK_EQ(argument.type, fz::Argument::VAR_REF);
177 return fz_var_to_index[argument.Var()];
178}
179
180LinearExpressionProto CpModelProtoWithMapping::LookupExpr(
181 const fz::Argument& argument, bool negate) {
182 LinearExpressionProto expr;
183 if (argument.HasOneValue()) {
184 const int64_t value = argument.Value();
185 expr.set_offset(negate ? -value : value);
186 } else {
187 expr.add_vars(LookupVar(argument));
188 expr.add_coeffs(negate ? -1 : 1);
189 }
190 return expr;
191}
192
193LinearExpressionProto CpModelProtoWithMapping::LookupExprAt(
194 const fz::Argument& argument, int pos, bool negate) {
195 LinearExpressionProto expr;
196 if (argument.HasOneValueAt(pos)) {
197 const int64_t value = argument.ValueAt(pos);
198 expr.set_offset(negate ? -value : value);
199 } else {
200 expr.add_vars(fz_var_to_index[argument.VarAt(pos)]);
201 expr.add_coeffs(negate ? -1 : 1);
202 }
203 return expr;
204}
205
206std::vector<int> CpModelProtoWithMapping::LookupVars(
207 const fz::Argument& argument) {
208 std::vector<int> result;
209 if (argument.type == fz::Argument::VOID_ARGUMENT) return result;
210 if (argument.type == fz::Argument::INT_LIST) {
211 for (int64_t value : argument.values) {
212 result.push_back(LookupConstant(value));
213 }
214 } else if (argument.type == fz::Argument::INT_VALUE) {
215 result.push_back(LookupConstant(argument.Value()));
216 } else {
217 CHECK_EQ(argument.type, fz::Argument::VAR_REF_ARRAY);
218 for (fz::Variable* var : argument.variables) {
219 CHECK(var != nullptr);
220 result.push_back(fz_var_to_index[var]);
221 }
222 }
223 return result;
224}
225
226VarOrValue CpModelProtoWithMapping::LookupVarOrValue(
227 const fz::Argument& argument) {
228 if (argument.type == fz::Argument::INT_VALUE) {
229 return {kNoVar, argument.Value()};
230 } else {
231 CHECK_EQ(argument.type, fz::Argument::VAR_REF);
232 fz::Variable* var = argument.Var();
233 CHECK(var != nullptr);
234 if (var->domain.HasOneValue()) {
235 return {kNoVar, var->domain.Value()};
236 } else {
237 return {fz_var_to_index[var], 0};
238 }
239 }
240}
241
242std::vector<VarOrValue> CpModelProtoWithMapping::LookupVarsOrValues(
243 const fz::Argument& argument) {
244 std::vector<VarOrValue> result;
245 const int no_var = kNoVar;
246 if (argument.type == fz::Argument::VOID_ARGUMENT) return result;
247 if (argument.type == fz::Argument::INT_LIST) {
248 for (int64_t value : argument.values) {
249 result.push_back({no_var, value});
250 }
251 } else if (argument.type == fz::Argument::INT_VALUE) {
252 result.push_back({no_var, argument.Value()});
253 } else {
254 CHECK_EQ(argument.type, fz::Argument::VAR_REF_ARRAY);
255 for (fz::Variable* var : argument.variables) {
256 CHECK(var != nullptr);
257 if (var->domain.HasOneValue()) {
258 result.push_back({no_var, var->domain.Value()});
259 } else {
260 result.push_back({fz_var_to_index[var], 0});
261 }
262 }
263 }
264 return result;
265}
266
267ConstraintProto* CpModelProtoWithMapping::AddEnforcedConstraint(int literal) {
268 ConstraintProto* result = proto.add_constraints();
269 if (literal != kNoVar) {
270 result->add_enforcement_literal(literal);
271 }
272 return result;
273}
274
275int CpModelProtoWithMapping::GetOrCreateLiteralForVarEqValue(int var,
276 int64_t value) {
277 const std::pair<int, int64_t> key = {var, value};
278 const auto it = var_eq_value_to_literal.find(key);
279 if (it != var_eq_value_to_literal.end()) return it->second;
280 const int bool_var = proto.variables_size();
281 IntegerVariableProto* var_proto = proto.add_variables();
282 var_proto->add_domain(0);
283 var_proto->add_domain(1);
284
285 ConstraintProto* is_eq = AddEnforcedConstraint(TrueLiteral(bool_var));
286 is_eq->mutable_linear()->add_vars(var);
287 is_eq->mutable_linear()->add_coeffs(1);
288 is_eq->mutable_linear()->add_domain(value);
289 is_eq->mutable_linear()->add_domain(value);
290
291 ConstraintProto* is_not_eq = AddEnforcedConstraint(FalseLiteral(bool_var));
292 is_not_eq->mutable_linear()->add_vars(var);
293 is_not_eq->mutable_linear()->add_coeffs(1);
294 is_not_eq->mutable_linear()->add_domain(std::numeric_limits<int64_t>::min());
295 is_not_eq->mutable_linear()->add_domain(value - 1);
296 is_not_eq->mutable_linear()->add_domain(value + 1);
297 is_not_eq->mutable_linear()->add_domain(std::numeric_limits<int64_t>::max());
298
299 var_eq_value_to_literal[key] = bool_var;
300 return bool_var;
301}
302
303int CpModelProtoWithMapping::GetOrCreateLiteralForVarEqVar(int var1, int var2) {
304 CHECK_NE(var1, kNoVar);
305 CHECK_NE(var2, kNoVar);
306 if (var1 > var2) std::swap(var1, var2);
307 if (var1 == var2) return LookupConstant(1);
308
309 const std::pair<int, int> key = {var1, var2};
310 const auto it = var_eq_var_to_literal.find(key);
311 if (it != var_eq_var_to_literal.end()) return it->second;
312
313 const int bool_var = proto.variables_size();
314 IntegerVariableProto* var_proto = proto.add_variables();
315 var_proto->add_domain(0);
316 var_proto->add_domain(1);
317
318 ConstraintProto* is_eq = AddEnforcedConstraint(TrueLiteral(bool_var));
319 is_eq->mutable_linear()->add_vars(var1);
320 is_eq->mutable_linear()->add_coeffs(1);
321 is_eq->mutable_linear()->add_vars(var2);
322 is_eq->mutable_linear()->add_coeffs(-1);
323 is_eq->mutable_linear()->add_domain(0);
324 is_eq->mutable_linear()->add_domain(0);
325
326 ConstraintProto* is_not_eq = AddEnforcedConstraint(FalseLiteral(bool_var));
327 is_not_eq->mutable_linear()->add_vars(var1);
328 is_not_eq->mutable_linear()->add_coeffs(1);
329 is_not_eq->mutable_linear()->add_vars(var2);
330 is_not_eq->mutable_linear()->add_coeffs(-1);
331 is_not_eq->mutable_linear()->add_domain(std::numeric_limits<int64_t>::min());
332 is_not_eq->mutable_linear()->add_domain(-1);
333 is_not_eq->mutable_linear()->add_domain(1);
334 is_not_eq->mutable_linear()->add_domain(std::numeric_limits<int64_t>::max());
335
336 var_eq_var_to_literal[key] = bool_var;
337 return bool_var;
338}
339
340int CpModelProtoWithMapping::GetOrCreateOptionalInterval(VarOrValue start,
341 VarOrValue size,
342 int opt_var) {
343 const int interval_index = proto.constraints_size();
344 const std::tuple<int, int64_t, int, int64_t, int> key =
345 std::make_tuple(start.var, start.value, size.var, size.value, opt_var);
346 const auto [it, inserted] =
347 interval_key_to_index.insert({key, interval_index});
348 if (!inserted) {
349 return it->second;
350 }
351
352 if (size.var == kNoVar || start.var == kNoVar) { // Size or start fixed.
353 auto* interval = AddEnforcedConstraint(opt_var)->mutable_interval();
354 if (start.var != kNoVar) {
355 interval->mutable_start()->add_vars(start.var);
356 interval->mutable_start()->add_coeffs(1);
357 interval->mutable_end()->add_vars(start.var);
358 interval->mutable_end()->add_coeffs(1);
359 } else {
360 interval->mutable_start()->set_offset(start.value);
361 interval->mutable_end()->set_offset(start.value);
362 }
363
364 if (size.var != kNoVar) {
365 interval->mutable_size()->add_vars(size.var);
366 interval->mutable_size()->add_coeffs(1);
367 interval->mutable_end()->add_vars(size.var);
368 interval->mutable_end()->add_coeffs(1);
369 } else {
370 interval->mutable_size()->set_offset(size.value);
371 interval->mutable_end()->set_offset(size.value +
372 interval->end().offset());
373 }
374 return interval_index;
375 } else { // start and size are variable.
376 const int end_var = proto.variables_size();
378 ReadDomainFromProto(proto.variables(start.var))
379 .AdditionWith(ReadDomainFromProto(proto.variables(size.var))),
380 proto.add_variables());
381
382 // Create the interval.
383 auto* interval = AddEnforcedConstraint(opt_var)->mutable_interval();
384 interval->mutable_start()->add_vars(start.var);
385 interval->mutable_start()->add_coeffs(1);
386 interval->mutable_size()->add_vars(size.var);
387 interval->mutable_size()->add_coeffs(1);
388 interval->mutable_end()->add_vars(end_var);
389 interval->mutable_end()->add_coeffs(1);
390
391 // Add the linear constraint (after the interval constraint as we have
392 // stored its index).
393 auto* lin = AddEnforcedConstraint(opt_var)->mutable_linear();
394 lin->add_vars(start.var);
395 lin->add_coeffs(1);
396 lin->add_vars(size.var);
397 lin->add_coeffs(1);
398 lin->add_vars(end_var);
399 lin->add_coeffs(-1);
400 lin->add_domain(0);
401 lin->add_domain(0);
402
403 return interval_index;
404 }
405}
406
407std::vector<int> CpModelProtoWithMapping::CreateIntervals(
408 absl::Span<const VarOrValue> starts, absl::Span<const VarOrValue> sizes) {
409 std::vector<int> intervals;
410 for (int i = 0; i < starts.size(); ++i) {
411 intervals.push_back(
412 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
413 }
414 return intervals;
415}
416
417std::vector<int> CpModelProtoWithMapping::CreateNonZeroOrOptionalIntervals(
418 absl::Span<const VarOrValue> starts, absl::Span<const VarOrValue> sizes) {
419 std::vector<int> intervals;
420 for (int i = 0; i < starts.size(); ++i) {
421 const int opt_var = NonZeroLiteralFrom(sizes[i]);
422 intervals.push_back(
423 GetOrCreateOptionalInterval(starts[i], sizes[i], opt_var));
424 }
425 return intervals;
426}
427
428int CpModelProtoWithMapping::NonZeroLiteralFrom(VarOrValue size) {
429 if (size.var == kNoVar) {
430 return LookupConstant(size.value > 0);
431 }
432 const auto it = var_to_lit_implies_greater_than_zero.find(size.var);
433 if (it != var_to_lit_implies_greater_than_zero.end()) {
434 return it->second;
435 }
436
437 const IntegerVariableProto& var_proto = proto.variables(size.var);
438 const Domain domain = ReadDomainFromProto(var_proto);
439 DCHECK_GE(domain.Min(), 0);
440 if (domain.Min() > 0) return LookupConstant(1);
441 if (domain.Max() == 0) {
442 return LookupConstant(0);
443 }
444
445 const int var_greater_than_zero_lit = proto.variables_size();
446 IntegerVariableProto* lit_proto = proto.add_variables();
447 lit_proto->add_domain(0);
448 lit_proto->add_domain(1);
449
450 ConstraintProto* is_greater =
451 AddEnforcedConstraint(TrueLiteral(var_greater_than_zero_lit));
452 is_greater->mutable_linear()->add_vars(size.var);
453 is_greater->mutable_linear()->add_coeffs(1);
454 const Domain positive = domain.IntersectionWith({1, domain.Max()});
455 FillDomainInProto(positive, is_greater->mutable_linear());
456
457 ConstraintProto* is_null =
458 AddEnforcedConstraint(FalseLiteral(var_greater_than_zero_lit));
459 is_null->mutable_linear()->add_vars(size.var);
460 is_null->mutable_linear()->add_coeffs(1);
461 is_null->mutable_linear()->add_domain(0);
462 is_null->mutable_linear()->add_domain(0);
463
464 var_to_lit_implies_greater_than_zero[size.var] = var_greater_than_zero_lit;
465 return var_greater_than_zero_lit;
466}
467
468void CpModelProtoWithMapping::FillAMinusBInDomain(
469 const std::vector<int64_t>& domain, const fz::Constraint& fz_ct,
470 ConstraintProto* ct) {
471 auto* arg = ct->mutable_linear();
472 if (fz_ct.arguments[1].type == fz::Argument::INT_VALUE) {
473 const int64_t value = fz_ct.arguments[1].Value();
474 const int var_a = LookupVar(fz_ct.arguments[0]);
475 for (const int64_t domain_bound : domain) {
476 if (domain_bound == std::numeric_limits<int64_t>::min() ||
477 domain_bound == std::numeric_limits<int64_t>::max()) {
478 arg->add_domain(domain_bound);
479 } else {
480 arg->add_domain(domain_bound + value);
481 }
482 }
483 arg->add_vars(var_a);
484 arg->add_coeffs(1);
485 } else if (fz_ct.arguments[0].type == fz::Argument::INT_VALUE) {
486 const int64_t value = fz_ct.arguments[0].Value();
487 const int var_b = LookupVar(fz_ct.arguments[1]);
488 for (int64_t domain_bound : gtl::reversed_view(domain)) {
489 if (domain_bound == std::numeric_limits<int64_t>::min()) {
490 arg->add_domain(std::numeric_limits<int64_t>::max());
491 } else if (domain_bound == std::numeric_limits<int64_t>::max()) {
492 arg->add_domain(std::numeric_limits<int64_t>::min());
493 } else {
494 arg->add_domain(value - domain_bound);
495 }
496 }
497 arg->add_vars(var_b);
498 arg->add_coeffs(1);
499 } else {
500 for (const int64_t domain_bound : domain) arg->add_domain(domain_bound);
501 arg->add_vars(LookupVar(fz_ct.arguments[0]));
502 arg->add_coeffs(1);
503 arg->add_vars(LookupVar(fz_ct.arguments[1]));
504 arg->add_coeffs(-1);
505 }
506}
507
508void CpModelProtoWithMapping::FillLinearConstraintWithGivenDomain(
509 absl::Span<const int64_t> domain, const fz::Constraint& fz_ct,
510 ConstraintProto* ct) {
511 auto* arg = ct->mutable_linear();
512 for (const int64_t domain_bound : domain) arg->add_domain(domain_bound);
513 std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
514 for (int i = 0; i < vars.size(); ++i) {
515 arg->add_vars(vars[i]);
516 arg->add_coeffs(fz_ct.arguments[0].values[i]);
517 }
518}
519
520void CpModelProtoWithMapping::BuildTableFromDomainIntLinEq(
521 const fz::Constraint& fz_ct, ConstraintProto* ct) {
522 const std::vector<int64_t>& coeffs = fz_ct.arguments[0].values;
523 const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
524 const int rhs = fz_ct.arguments[2].Value();
525 CHECK_EQ(coeffs.back(), -1);
526 for (const int var : vars) {
527 LinearExpressionProto* expr = ct->mutable_table()->add_exprs();
528 expr->add_vars(var);
529 expr->add_coeffs(1);
530 }
531
532 switch (vars.size()) {
533 case 3: {
534 const Domain domain0 = ReadDomainFromProto(proto.variables(vars[0]));
535 const Domain domain1 = ReadDomainFromProto(proto.variables(vars[1]));
536 for (const int64_t v0 : domain0.Values()) {
537 for (const int64_t v1 : domain1.Values()) {
538 const int64_t v2 = coeffs[0] * v0 + coeffs[1] * v1 - rhs;
539 ct->mutable_table()->add_values(v0);
540 ct->mutable_table()->add_values(v1);
541 ct->mutable_table()->add_values(v2);
542 }
543 }
544 break;
545 }
546 case 4: {
547 const Domain domain0 = ReadDomainFromProto(proto.variables(vars[0]));
548 const Domain domain1 = ReadDomainFromProto(proto.variables(vars[1]));
549 const Domain domain2 = ReadDomainFromProto(proto.variables(vars[2]));
550 for (const int64_t v0 : domain0.Values()) {
551 for (const int64_t v1 : domain1.Values()) {
552 for (const int64_t v2 : domain2.Values()) {
553 const int64_t v3 =
554 coeffs[0] * v0 + coeffs[1] * v1 + coeffs[2] * v2 - rhs;
555 ct->mutable_table()->add_values(v0);
556 ct->mutable_table()->add_values(v1);
557 ct->mutable_table()->add_values(v2);
558 ct->mutable_table()->add_values(v3);
559 }
560 }
561 }
562 break;
563 }
564 default:
565 LOG(FATAL) << "Unsupported size";
566 }
567}
568
569void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
570 ConstraintProto* ct) {
571 if (fz_ct.type == "false_constraint") {
572 // An empty clause is always false.
573 ct->mutable_bool_or();
574 } else if (fz_ct.type == "bool_clause") {
575 auto* arg = ct->mutable_bool_or();
576 for (const int var : LookupVars(fz_ct.arguments[0])) {
577 arg->add_literals(TrueLiteral(var));
578 }
579 for (const int var : LookupVars(fz_ct.arguments[1])) {
580 arg->add_literals(FalseLiteral(var));
581 }
582 } else if (fz_ct.type == "bool_xor") {
583 // This is not the same semantics as the array_bool_xor as this constraint
584 // is actually a fully reified xor(a, b) <==> x.
585 const int a = LookupVar(fz_ct.arguments[0]);
586 const int b = LookupVar(fz_ct.arguments[1]);
587 const int x = LookupVar(fz_ct.arguments[2]);
588
589 // not(x) => a == b
590 ct->add_enforcement_literal(NegatedRef(x));
591 auto* const refute = ct->mutable_linear();
592 refute->add_vars(a);
593 refute->add_coeffs(1);
594 refute->add_vars(b);
595 refute->add_coeffs(-1);
596 refute->add_domain(0);
597 refute->add_domain(0);
598
599 // x => a + b == 1
600 auto* enforce = AddEnforcedConstraint(x)->mutable_linear();
601 enforce->add_vars(a);
602 enforce->add_coeffs(1);
603 enforce->add_vars(b);
604 enforce->add_coeffs(1);
605 enforce->add_domain(1);
606 enforce->add_domain(1);
607 } else if (fz_ct.type == "array_bool_or") {
608 auto* arg = ct->mutable_bool_or();
609 for (const int var : LookupVars(fz_ct.arguments[0])) {
610 arg->add_literals(TrueLiteral(var));
611 }
612 } else if (fz_ct.type == "array_bool_or_negated") {
613 auto* arg = ct->mutable_bool_and();
614 for (const int var : LookupVars(fz_ct.arguments[0])) {
615 arg->add_literals(FalseLiteral(var));
616 }
617 } else if (fz_ct.type == "array_bool_and") {
618 auto* arg = ct->mutable_bool_and();
619 for (const int var : LookupVars(fz_ct.arguments[0])) {
620 arg->add_literals(TrueLiteral(var));
621 }
622 } else if (fz_ct.type == "array_bool_and_negated") {
623 auto* arg = ct->mutable_bool_or();
624 for (const int var : LookupVars(fz_ct.arguments[0])) {
625 arg->add_literals(FalseLiteral(var));
626 }
627 } else if (fz_ct.type == "array_bool_xor") {
628 auto* arg = ct->mutable_bool_xor();
629 for (const int var : LookupVars(fz_ct.arguments[0])) {
630 arg->add_literals(TrueLiteral(var));
631 }
632 } else if (fz_ct.type == "bool_le" || fz_ct.type == "int_le") {
633 FillAMinusBInDomain({std::numeric_limits<int64_t>::min(), 0}, fz_ct, ct);
634 } else if (fz_ct.type == "bool_ge" || fz_ct.type == "int_ge") {
635 FillAMinusBInDomain({0, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
636 } else if (fz_ct.type == "bool_lt" || fz_ct.type == "int_lt") {
637 FillAMinusBInDomain({std::numeric_limits<int64_t>::min(), -1}, fz_ct, ct);
638 } else if (fz_ct.type == "bool_gt" || fz_ct.type == "int_gt") {
639 FillAMinusBInDomain({1, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
640 } else if (fz_ct.type == "bool_eq" || fz_ct.type == "int_eq" ||
641 fz_ct.type == "bool2int") {
642 FillAMinusBInDomain({0, 0}, fz_ct, ct);
643 } else if (fz_ct.type == "bool_ne" || fz_ct.type == "bool_not") {
644 auto* arg = ct->mutable_linear();
645 arg->add_vars(LookupVar(fz_ct.arguments[0]));
646 arg->add_coeffs(1);
647 arg->add_vars(LookupVar(fz_ct.arguments[1]));
648 arg->add_coeffs(1);
649 arg->add_domain(1);
650 arg->add_domain(1);
651 } else if (fz_ct.type == "int_ne") {
652 FillAMinusBInDomain({std::numeric_limits<int64_t>::min(), -1, 1,
653 std::numeric_limits<int64_t>::max()},
654 fz_ct, ct);
655 } else if (fz_ct.type == "int_lin_eq") {
656 // Special case for the index of element 2D and element 3D constraints.
657 if (fz_ct.strong_propagation && fz_ct.arguments[0].Size() >= 3 &&
658 fz_ct.arguments[0].Size() <= 4 &&
659 fz_ct.arguments[0].values.back() == -1) {
660 BuildTableFromDomainIntLinEq(fz_ct, ct);
661 } else {
662 const int64_t rhs = fz_ct.arguments[2].values[0];
663 FillLinearConstraintWithGivenDomain({rhs, rhs}, fz_ct, ct);
664 }
665 } else if (fz_ct.type == "bool_lin_eq") {
666 auto* arg = ct->mutable_linear();
667 const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
668 for (int i = 0; i < vars.size(); ++i) {
669 arg->add_vars(vars[i]);
670 arg->add_coeffs(fz_ct.arguments[0].values[i]);
671 }
672 if (fz_ct.arguments[2].IsVariable()) {
673 arg->add_vars(LookupVar(fz_ct.arguments[2]));
674 arg->add_coeffs(-1);
675 arg->add_domain(0);
676 arg->add_domain(0);
677 } else {
678 const int64_t v = fz_ct.arguments[2].Value();
679 arg->add_domain(v);
680 arg->add_domain(v);
681 }
682 } else if (fz_ct.type == "int_lin_le" || fz_ct.type == "bool_lin_le") {
683 const int64_t rhs = fz_ct.arguments[2].values[0];
684 FillLinearConstraintWithGivenDomain(
685 {std::numeric_limits<int64_t>::min(), rhs}, fz_ct, ct);
686 } else if (fz_ct.type == "int_lin_lt") {
687 const int64_t rhs = fz_ct.arguments[2].values[0];
688 FillLinearConstraintWithGivenDomain(
689 {std::numeric_limits<int64_t>::min(), rhs - 1}, fz_ct, ct);
690 } else if (fz_ct.type == "int_lin_ge") {
691 const int64_t rhs = fz_ct.arguments[2].values[0];
692 FillLinearConstraintWithGivenDomain(
693 {rhs, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
694 } else if (fz_ct.type == "int_lin_gt") {
695 const int64_t rhs = fz_ct.arguments[2].values[0];
696 FillLinearConstraintWithGivenDomain(
697 {rhs + 1, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
698 } else if (fz_ct.type == "int_lin_ne") {
699 const int64_t rhs = fz_ct.arguments[2].values[0];
700 FillLinearConstraintWithGivenDomain(
701 {std::numeric_limits<int64_t>::min(), rhs - 1, rhs + 1,
702 std::numeric_limits<int64_t>::max()},
703 fz_ct, ct);
704 } else if (fz_ct.type == "set_in") {
705 auto* arg = ct->mutable_linear();
706 arg->add_vars(LookupVar(fz_ct.arguments[0]));
707 arg->add_coeffs(1);
708 if (fz_ct.arguments[1].type == fz::Argument::INT_LIST) {
709 FillDomainInProto(Domain::FromValues(std::vector<int64_t>{
710 fz_ct.arguments[1].values.begin(),
711 fz_ct.arguments[1].values.end()}),
712 arg);
713 } else if (fz_ct.arguments[1].type == fz::Argument::INT_INTERVAL) {
715 Domain(fz_ct.arguments[1].values[0], fz_ct.arguments[1].values[1]),
716 arg);
717 } else {
718 LOG(FATAL) << "Wrong format";
719 }
720 } else if (fz_ct.type == "set_in_negated") {
721 auto* arg = ct->mutable_linear();
722 arg->add_vars(LookupVar(fz_ct.arguments[0]));
723 arg->add_coeffs(1);
724 if (fz_ct.arguments[1].type == fz::Argument::INT_LIST) {
726 Domain::FromValues(
727 std::vector<int64_t>{fz_ct.arguments[1].values.begin(),
728 fz_ct.arguments[1].values.end()})
729 .Complement(),
730 arg);
731 } else if (fz_ct.arguments[1].type == fz::Argument::INT_INTERVAL) {
733 Domain(fz_ct.arguments[1].values[0], fz_ct.arguments[1].values[1])
734 .Complement(),
735 arg);
736 } else {
737 LOG(FATAL) << "Wrong format";
738 }
739 } else if (fz_ct.type == "int_min") {
740 auto* arg = ct->mutable_lin_max();
741 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0], /*negate=*/true);
742 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1], /*negate=*/true);
743 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2], /*negate=*/true);
744 } else if (fz_ct.type == "array_int_minimum" || fz_ct.type == "minimum_int") {
745 auto* arg = ct->mutable_lin_max();
746 *arg->mutable_target() = LookupExpr(fz_ct.arguments[0], /*negate=*/true);
747 for (int i = 0; i < fz_ct.arguments[1].Size(); ++i) {
748 *arg->add_exprs() = LookupExprAt(fz_ct.arguments[1], i, /*negate=*/true);
749 }
750 } else if (fz_ct.type == "int_max") {
751 auto* arg = ct->mutable_lin_max();
752 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
753 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
754 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
755 } else if (fz_ct.type == "array_int_maximum" || fz_ct.type == "maximum_int") {
756 auto* arg = ct->mutable_lin_max();
757 *arg->mutable_target() = LookupExpr(fz_ct.arguments[0]);
758 for (int i = 0; i < fz_ct.arguments[1].Size(); ++i) {
759 *arg->add_exprs() = LookupExprAt(fz_ct.arguments[1], i);
760 }
761 } else if (fz_ct.type == "int_times") {
762 auto* arg = ct->mutable_int_prod();
763 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
764 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
765 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
766 } else if (fz_ct.type == "int_abs") {
767 auto* arg = ct->mutable_lin_max();
768 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
769 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0], /*negate=*/true);
770 *arg->mutable_target() = LookupExpr(fz_ct.arguments[1]);
771 } else if (fz_ct.type == "int_plus") {
772 auto* arg = ct->mutable_linear();
773 FillDomainInProto(Domain(0, 0), arg);
774 arg->add_vars(LookupVar(fz_ct.arguments[0]));
775 arg->add_coeffs(1);
776 arg->add_vars(LookupVar(fz_ct.arguments[1]));
777 arg->add_coeffs(1);
778 arg->add_vars(LookupVar(fz_ct.arguments[2]));
779 arg->add_coeffs(-1);
780 } else if (fz_ct.type == "int_div") {
781 auto* arg = ct->mutable_int_div();
782 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
783 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
784 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
785 } else if (fz_ct.type == "int_mod") {
786 auto* arg = ct->mutable_int_mod();
787 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
788 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
789 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
790 } else if (fz_ct.type == "array_int_element" ||
791 fz_ct.type == "array_bool_element" ||
792 fz_ct.type == "array_var_int_element" ||
793 fz_ct.type == "array_var_bool_element" ||
794 fz_ct.type == "array_int_element_nonshifted") {
795 auto* arg = ct->mutable_element();
796 *arg->mutable_linear_index() = LookupExpr(fz_ct.arguments[0]);
797 if (!absl::EndsWith(fz_ct.type, "_nonshifted")) {
798 arg->mutable_linear_index()->set_offset(arg->linear_index().offset() - 1);
799 }
800 *arg->mutable_linear_target() = LookupExpr(fz_ct.arguments[2]);
801
802 for (const VarOrValue elem : LookupVarsOrValues(fz_ct.arguments[1])) {
803 auto* elem_proto = ct->mutable_element()->add_exprs();
804 if (elem.var != kNoVar) {
805 elem_proto->add_vars(elem.var);
806 elem_proto->add_coeffs(1);
807 } else {
808 elem_proto->set_offset(elem.value);
809 }
810 }
811 } else if (fz_ct.type == "ortools_array_int_element" ||
812 fz_ct.type == "ortools_array_bool_element" ||
813 fz_ct.type == "ortools_array_var_int_element" ||
814 fz_ct.type == "ortools_array_var_bool_element") {
815 auto* arg = ct->mutable_element();
816
817 // Index.
818 *arg->mutable_linear_index() = LookupExpr(fz_ct.arguments[0]);
819 const int64_t index_min = fz_ct.arguments[1].values[0];
820 arg->mutable_linear_index()->set_offset(arg->linear_index().offset() -
821 index_min);
822
823 // Target.
824 *arg->mutable_linear_target() = LookupExpr(fz_ct.arguments[3]);
825
826 // Expressions.
827 for (const VarOrValue elem : LookupVarsOrValues(fz_ct.arguments[2])) {
828 auto* elem_proto = ct->mutable_element()->add_exprs();
829 if (elem.var != kNoVar) {
830 elem_proto->add_vars(elem.var);
831 elem_proto->add_coeffs(1);
832 } else {
833 elem_proto->set_offset(elem.value);
834 }
835 }
836 } else if (fz_ct.type == "ortools_table_int") {
837 auto* arg = ct->mutable_table();
838 for (const VarOrValue v : LookupVarsOrValues(fz_ct.arguments[0])) {
839 LinearExpressionProto* expr = arg->add_exprs();
840 if (v.var != kNoVar) {
841 expr->add_vars(v.var);
842 expr->add_coeffs(1);
843 } else {
844 expr->set_offset(v.value);
845 }
846 }
847 for (const int64_t value : fz_ct.arguments[1].values)
848 arg->add_values(value);
849 } else if (fz_ct.type == "ortools_regular") {
850 auto* arg = ct->mutable_automaton();
851 for (const VarOrValue v : LookupVarsOrValues(fz_ct.arguments[0])) {
852 LinearExpressionProto* expr = arg->add_exprs();
853 if (v.var != kNoVar) {
854 expr->add_vars(v.var);
855 expr->add_coeffs(1);
856 } else {
857 expr->set_offset(v.value);
858 }
859 }
860
861 int count = 0;
862 const int num_states = fz_ct.arguments[1].Value();
863 const int num_values = fz_ct.arguments[2].Value();
864 for (int i = 1; i <= num_states; ++i) {
865 for (int j = 1; j <= num_values; ++j) {
866 CHECK_LT(count, fz_ct.arguments[3].values.size());
867 const int next = fz_ct.arguments[3].values[count++];
868 if (next == 0) continue; // 0 is a failing state.
869 arg->add_transition_tail(i);
870 arg->add_transition_label(j);
871 arg->add_transition_head(next);
872 }
873 }
874
875 arg->set_starting_state(fz_ct.arguments[4].Value());
876 switch (fz_ct.arguments[5].type) {
877 case fz::Argument::INT_VALUE: {
878 arg->add_final_states(fz_ct.arguments[5].values[0]);
879 break;
880 }
881 case fz::Argument::INT_INTERVAL: {
882 for (int v = fz_ct.arguments[5].values[0];
883 v <= fz_ct.arguments[5].values[1]; ++v) {
884 arg->add_final_states(v);
885 }
886 break;
887 }
888 case fz::Argument::INT_LIST: {
889 for (const int v : fz_ct.arguments[5].values) {
890 arg->add_final_states(v);
891 }
892 break;
893 }
894 default: {
895 LOG(FATAL) << "Wrong constraint " << fz_ct.DebugString();
896 }
897 }
898 } else if (fz_ct.type == "fzn_all_different_int") {
899 auto* arg = ct->mutable_all_diff();
900 for (int i = 0; i < fz_ct.arguments[0].Size(); ++i) {
901 *arg->add_exprs() = LookupExprAt(fz_ct.arguments[0], i);
902 }
903 } else if (fz_ct.type == "ortools_count_eq_cst") {
904 const std::vector<VarOrValue> counts =
905 LookupVarsOrValues(fz_ct.arguments[0]);
906 const int64_t value = fz_ct.arguments[1].Value();
907 const VarOrValue target = LookupVarOrValue(fz_ct.arguments[2]);
908 LinearConstraintProto* arg = ct->mutable_linear();
909 int64_t fixed_contributions = 0;
910 for (const VarOrValue& count : counts) {
911 if (count.var == kNoVar) {
912 fixed_contributions += count.value == value ? 1 : 0;
913 } else {
914 const int boolvar = GetOrCreateLiteralForVarEqValue(count.var, value);
915 CHECK_GE(boolvar, 0);
916 arg->add_vars(boolvar);
917 arg->add_coeffs(1);
918 }
919 }
920 if (target.var == kNoVar) {
921 arg->add_domain(target.value - fixed_contributions);
922 arg->add_domain(target.value - fixed_contributions);
923 } else {
924 arg->add_vars(target.var);
925 arg->add_coeffs(-1);
926 arg->add_domain(-fixed_contributions);
927 arg->add_domain(-fixed_contributions);
928 }
929 } else if (fz_ct.type == "ortools_count_eq") {
930 const std::vector<VarOrValue> counts =
931 LookupVarsOrValues(fz_ct.arguments[0]);
932 const int var = LookupVar(fz_ct.arguments[1]);
933 const VarOrValue target = LookupVarOrValue(fz_ct.arguments[2]);
934 LinearConstraintProto* arg = ct->mutable_linear();
935 for (const VarOrValue& count : counts) {
936 if (count.var == kNoVar) {
937 const int boolvar = GetOrCreateLiteralForVarEqValue(var, count.value);
938 CHECK_GE(boolvar, 0);
939 arg->add_vars(boolvar);
940 arg->add_coeffs(1);
941 } else {
942 const int boolvar = GetOrCreateLiteralForVarEqVar(var, count.var);
943 CHECK_GE(boolvar, 0);
944 arg->add_vars(boolvar);
945 arg->add_coeffs(1);
946 }
947 }
948 if (target.var == kNoVar) {
949 arg->add_domain(target.value);
950 arg->add_domain(target.value);
951 } else {
952 arg->add_vars(target.var);
953 arg->add_coeffs(-1);
954 arg->add_domain(0);
955 arg->add_domain(0);
956 }
957 } else if (fz_ct.type == "ortools_circuit" ||
958 fz_ct.type == "ortools_subcircuit") {
959 const int64_t min_index = fz_ct.arguments[1].Value();
960 const int size = std::max(fz_ct.arguments[0].values.size(),
961 fz_ct.arguments[0].variables.size());
962
963 const int64_t max_index = min_index + size - 1;
964 // The arc-based mutable circuit.
965 auto* circuit_arg = ct->mutable_circuit();
966
967 // We fully encode all variables so we can use the literal based circuit.
968 // TODO(user): avoid fully encoding more than once?
969 int64_t index = min_index;
970 const bool is_circuit = (fz_ct.type == "ortools_circuit");
971 for (const int var : LookupVars(fz_ct.arguments[0])) {
972 Domain domain = ReadDomainFromProto(proto.variables(var));
973
974 // Restrict the domain of var to [min_index, max_index]
975 domain = domain.IntersectionWith(Domain(min_index, max_index));
976 if (is_circuit) {
977 // We simply make sure that the variable cannot take the value index.
978 domain = domain.IntersectionWith(Domain::FromIntervals(
979 {{std::numeric_limits<int64_t>::min(), index - 1},
980 {index + 1, std::numeric_limits<int64_t>::max()}}));
981 }
982 FillDomainInProto(domain, proto.mutable_variables(var));
983
984 for (const ClosedInterval interval : domain) {
985 for (int64_t value = interval.start; value <= interval.end; ++value) {
986 // Create one Boolean variable for this arc.
987 const int literal = proto.variables_size();
988 {
989 auto* new_var = proto.add_variables();
990 new_var->add_domain(0);
991 new_var->add_domain(1);
992 }
993
994 // Add the arc.
995 circuit_arg->add_tails(index);
996 circuit_arg->add_heads(value);
997 circuit_arg->add_literals(literal);
998
999 // literal => var == value.
1000 {
1001 auto* lin = AddEnforcedConstraint(literal)->mutable_linear();
1002 lin->add_coeffs(1);
1003 lin->add_vars(var);
1004 lin->add_domain(value);
1005 lin->add_domain(value);
1006 }
1007
1008 // not(literal) => var != value
1009 {
1010 auto* lin =
1011 AddEnforcedConstraint(NegatedRef(literal))->mutable_linear();
1012 lin->add_coeffs(1);
1013 lin->add_vars(var);
1014 lin->add_domain(std::numeric_limits<int64_t>::min());
1015 lin->add_domain(value - 1);
1016 lin->add_domain(value + 1);
1017 lin->add_domain(std::numeric_limits<int64_t>::max());
1018 }
1019 }
1020 }
1021
1022 ++index;
1023 }
1024 } else if (fz_ct.type == "ortools_inverse") {
1025 auto* arg = ct->mutable_inverse();
1026
1027 const auto direct_variables = LookupVars(fz_ct.arguments[0]);
1028 const auto inverse_variables = LookupVars(fz_ct.arguments[1]);
1029 const int base_direct = fz_ct.arguments[2].Value();
1030 const int base_inverse = fz_ct.arguments[3].Value();
1031
1032 CHECK_EQ(direct_variables.size(), inverse_variables.size());
1033 const int num_variables = direct_variables.size();
1034 const int end_direct = base_direct + num_variables;
1035 const int end_inverse = base_inverse + num_variables;
1036
1037 // Any convention that maps the "fixed values" to the one of the inverse and
1038 // back works. We decided to follow this one:
1039 // There are 3 cases:
1040 // (A) base_direct == base_inverse, we fill the arrays
1041 // direct = [0, .., base_direct - 1] U [direct_vars]
1042 // inverse = [0, .., base_direct - 1] U [inverse_vars]
1043 // (B) base_direct == base_inverse + offset (> 0), we fill the arrays
1044 // direct = [0, .., base_inverse - 1] U
1045 // [end_inverse, .., end_inverse + offset - 1] U
1046 // [direct_vars]
1047 // inverse = [0, .., base_inverse - 1] U
1048 // [inverse_vars] U
1049 // [base_inverse, .., base_base_inverse + offset - 1]
1050 // (C): base_inverse == base_direct + offset (> 0), we fill the arrays
1051 // direct = [0, .., base_direct - 1] U
1052 // [direct_vars] U
1053 // [base_direct, .., base_direct + offset - 1]
1054 // inverse [0, .., base_direct - 1] U
1055 // [end_direct, .., end_direct + offset - 1] U
1056 // [inverse_vars]
1057 const int arity = std::max(base_inverse, base_direct) + num_variables;
1058 for (int i = 0; i < arity; ++i) {
1059 // Fill the direct array.
1060 if (i < base_direct) {
1061 if (i < base_inverse) {
1062 arg->add_f_direct(LookupConstant(i));
1063 } else if (i >= base_inverse) {
1064 arg->add_f_direct(LookupConstant(i + num_variables));
1065 }
1066 } else if (i >= base_direct && i < end_direct) {
1067 arg->add_f_direct(direct_variables[i - base_direct]);
1068 } else {
1069 arg->add_f_direct(LookupConstant(i - num_variables));
1070 }
1071
1072 // Fill the inverse array.
1073 if (i < base_inverse) {
1074 if (i < base_direct) {
1075 arg->add_f_inverse(LookupConstant(i));
1076 } else if (i >= base_direct) {
1077 arg->add_f_inverse(LookupConstant(i + num_variables));
1078 }
1079 } else if (i >= base_inverse && i < end_inverse) {
1080 arg->add_f_inverse(inverse_variables[i - base_inverse]);
1081 } else {
1082 arg->add_f_inverse(LookupConstant(i - num_variables));
1083 }
1084 }
1085 } else if (fz_ct.type == "fzn_disjunctive") {
1086 const std::vector<VarOrValue> starts =
1087 LookupVarsOrValues(fz_ct.arguments[0]);
1088 const std::vector<VarOrValue> sizes =
1089 LookupVarsOrValues(fz_ct.arguments[1]);
1090
1091 auto* arg = ct->mutable_cumulative();
1092 arg->mutable_capacity()->set_offset(1);
1093 for (int i = 0; i < starts.size(); ++i) {
1094 arg->add_intervals(
1095 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
1096 arg->add_demands()->set_offset(1);
1097 }
1098 } else if (fz_ct.type == "fzn_disjunctive_strict") {
1099 const std::vector<VarOrValue> starts =
1100 LookupVarsOrValues(fz_ct.arguments[0]);
1101 const std::vector<VarOrValue> sizes =
1102 LookupVarsOrValues(fz_ct.arguments[1]);
1103
1104 auto* arg = ct->mutable_no_overlap();
1105 for (int i = 0; i < starts.size(); ++i) {
1106 arg->add_intervals(
1107 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
1108 }
1109 } else if (fz_ct.type == "fzn_cumulative") {
1110 const std::vector<VarOrValue> starts =
1111 LookupVarsOrValues(fz_ct.arguments[0]);
1112 const std::vector<VarOrValue> sizes =
1113 LookupVarsOrValues(fz_ct.arguments[1]);
1114 const std::vector<VarOrValue> demands =
1115 LookupVarsOrValues(fz_ct.arguments[2]);
1116
1117 auto* arg = ct->mutable_cumulative();
1118 if (fz_ct.arguments[3].HasOneValue()) {
1119 arg->mutable_capacity()->set_offset(fz_ct.arguments[3].Value());
1120 } else {
1121 arg->mutable_capacity()->add_vars(LookupVar(fz_ct.arguments[3]));
1122 arg->mutable_capacity()->add_coeffs(1);
1123 }
1124 for (int i = 0; i < starts.size(); ++i) {
1125 // Special case for a 0-1 demand, we mark the interval as optional
1126 // instead and fix the demand to 1.
1127 if (demands[i].var != kNoVar &&
1128 proto.variables(demands[i].var).domain().size() == 2 &&
1129 proto.variables(demands[i].var).domain(0) == 0 &&
1130 proto.variables(demands[i].var).domain(1) == 1 &&
1131 fz_ct.arguments[3].HasOneValue() && fz_ct.arguments[3].Value() == 1) {
1132 arg->add_intervals(
1133 GetOrCreateOptionalInterval(starts[i], sizes[i], demands[i].var));
1134 arg->add_demands()->set_offset(1);
1135 } else {
1136 arg->add_intervals(
1137 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
1138 LinearExpressionProto* demand = arg->add_demands();
1139 if (demands[i].var == kNoVar) {
1140 demand->set_offset(demands[i].value);
1141 } else {
1142 demand->add_vars(demands[i].var);
1143 demand->add_coeffs(1);
1144 }
1145 }
1146 }
1147 } else if (fz_ct.type == "ortools_cumulative_opt") {
1148 const std::vector<int> occurs = LookupVars(fz_ct.arguments[0]);
1149 const std::vector<VarOrValue> starts =
1150 LookupVarsOrValues(fz_ct.arguments[1]);
1151 const std::vector<VarOrValue> durations =
1152 LookupVarsOrValues(fz_ct.arguments[2]);
1153 const std::vector<VarOrValue> demands =
1154 LookupVarsOrValues(fz_ct.arguments[3]);
1155
1156 auto* arg = ct->mutable_cumulative();
1157 if (fz_ct.arguments[3].HasOneValue()) {
1158 arg->mutable_capacity()->set_offset(fz_ct.arguments[4].Value());
1159 } else {
1160 arg->mutable_capacity()->add_vars(LookupVar(fz_ct.arguments[4]));
1161 arg->mutable_capacity()->add_coeffs(1);
1162 }
1163 for (int i = 0; i < starts.size(); ++i) {
1164 arg->add_intervals(
1165 GetOrCreateOptionalInterval(starts[i], durations[i], occurs[i]));
1166 LinearExpressionProto* demand = arg->add_demands();
1167 if (demands[i].var == kNoVar) {
1168 demand->set_offset(demands[i].value);
1169 } else {
1170 demand->add_vars(demands[i].var);
1171 demand->add_coeffs(1);
1172 }
1173 }
1174 } else if (fz_ct.type == "ortools_disjunctive_strict_opt") {
1175 const std::vector<int> occurs = LookupVars(fz_ct.arguments[0]);
1176 const std::vector<VarOrValue> starts =
1177 LookupVarsOrValues(fz_ct.arguments[1]);
1178 const std::vector<VarOrValue> durations =
1179 LookupVarsOrValues(fz_ct.arguments[2]);
1180
1181 auto* arg = ct->mutable_no_overlap();
1182 for (int i = 0; i < starts.size(); ++i) {
1183 arg->add_intervals(
1184 GetOrCreateOptionalInterval(starts[i], durations[i], occurs[i]));
1185 }
1186 } else if (fz_ct.type == "fzn_diffn" || fz_ct.type == "fzn_diffn_nonstrict") {
1187 const bool is_strict = fz_ct.type == "fzn_diffn";
1188 const std::vector<VarOrValue> x = LookupVarsOrValues(fz_ct.arguments[0]);
1189 const std::vector<VarOrValue> y = LookupVarsOrValues(fz_ct.arguments[1]);
1190 const std::vector<VarOrValue> dx = LookupVarsOrValues(fz_ct.arguments[2]);
1191 const std::vector<VarOrValue> dy = LookupVarsOrValues(fz_ct.arguments[3]);
1192 const std::vector<int> x_intervals =
1193 is_strict ? CreateIntervals(x, dx)
1194 : CreateNonZeroOrOptionalIntervals(x, dx);
1195 const std::vector<int> y_intervals =
1196 is_strict ? CreateIntervals(y, dy)
1197 : CreateNonZeroOrOptionalIntervals(y, dy);
1198 auto* arg = ct->mutable_no_overlap_2d();
1199 for (int i = 0; i < x.size(); ++i) {
1200 arg->add_x_intervals(x_intervals[i]);
1201 arg->add_y_intervals(y_intervals[i]);
1202 }
1203 } else if (fz_ct.type == "ortools_network_flow" ||
1204 fz_ct.type == "ortools_network_flow_cost") {
1205 // Note that we leave ct empty here (with just the name set).
1206 // We simply do a linear encoding of this constraint.
1207 const bool has_cost = fz_ct.type == "ortools_network_flow_cost";
1208 const std::vector<int> flow = LookupVars(fz_ct.arguments[3]);
1209
1210 // Flow conservation constraints.
1211 const int num_nodes = fz_ct.arguments[1].values.size();
1212 const int base_node = fz_ct.arguments[2].Value();
1213 std::vector<std::vector<int>> flows_per_node(num_nodes);
1214 std::vector<std::vector<int>> coeffs_per_node(num_nodes);
1215
1216 const int num_arcs = fz_ct.arguments[0].values.size() / 2;
1217 for (int arc = 0; arc < num_arcs; arc++) {
1218 const int tail = fz_ct.arguments[0].values[2 * arc] - base_node;
1219 const int head = fz_ct.arguments[0].values[2 * arc + 1] - base_node;
1220 if (tail == head) continue;
1221
1222 flows_per_node[tail].push_back(flow[arc]);
1223 coeffs_per_node[tail].push_back(1);
1224 flows_per_node[head].push_back(flow[arc]);
1225 coeffs_per_node[head].push_back(-1);
1226 }
1227 for (int node = 0; node < num_nodes; node++) {
1228 auto* arg = proto.add_constraints()->mutable_linear();
1229 arg->add_domain(fz_ct.arguments[1].values[node]);
1230 arg->add_domain(fz_ct.arguments[1].values[node]);
1231 for (int i = 0; i < flows_per_node[node].size(); ++i) {
1232 arg->add_vars(flows_per_node[node][i]);
1233 arg->add_coeffs(coeffs_per_node[node][i]);
1234 }
1235 }
1236
1237 if (has_cost) {
1238 auto* arg = proto.add_constraints()->mutable_linear();
1239 arg->add_domain(0);
1240 arg->add_domain(0);
1241 for (int arc = 0; arc < num_arcs; arc++) {
1242 const int64_t weight = fz_ct.arguments[4].values[arc];
1243 if (weight != 0) {
1244 arg->add_vars(flow[arc]);
1245 arg->add_coeffs(weight);
1246 }
1247 }
1248 arg->add_vars(LookupVar(fz_ct.arguments[5]));
1249 arg->add_coeffs(-1);
1250 }
1251 } else {
1252 LOG(FATAL) << " Not supported " << fz_ct.type;
1253 }
1254} // NOLINT(readability/fn_size)
1255
1256void CpModelProtoWithMapping::FillReifOrImpliedConstraint(
1257 const fz::Constraint& fz_ct, ConstraintProto* ct) {
1258 // Start by adding a non-reified version of the same constraint.
1259 std::string simplified_type;
1260 if (absl::EndsWith(fz_ct.type, "_reif")) {
1261 // Remove _reif.
1262 simplified_type = fz_ct.type.substr(0, fz_ct.type.size() - 5);
1263 } else if (absl::EndsWith(fz_ct.type, "_imp")) {
1264 // Remove _imp.
1265 simplified_type = fz_ct.type.substr(0, fz_ct.type.size() - 4);
1266 } else {
1267 // Keep name as it is an implicit reified constraint.
1268 simplified_type = fz_ct.type;
1269 }
1270
1271 // We need a copy to be able to change the type of the constraint.
1272 fz::Constraint copy = fz_ct;
1273 copy.type = simplified_type;
1274
1275 // Create the CP-SAT constraint.
1276 FillConstraint(copy, ct);
1277
1278 // In case of reified constraints, the type of the opposite constraint.
1279 std::string negated_type;
1280
1281 // Fill enforcement_literal and set copy.type to the negated constraint.
1282 if (simplified_type == "array_bool_or") {
1283 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[1])));
1284 negated_type = "array_bool_or_negated";
1285 } else if (simplified_type == "array_bool_and") {
1286 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[1])));
1287 negated_type = "array_bool_and_negated";
1288 } else if (simplified_type == "set_in") {
1289 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1290 negated_type = "set_in_negated";
1291 } else if (simplified_type == "bool_eq" || simplified_type == "int_eq") {
1292 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1293 negated_type = "int_ne";
1294 } else if (simplified_type == "bool_ne" || simplified_type == "int_ne") {
1295 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1296 negated_type = "int_eq";
1297 } else if (simplified_type == "bool_le" || simplified_type == "int_le") {
1298 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1299 negated_type = "int_gt";
1300 } else if (simplified_type == "bool_lt" || simplified_type == "int_lt") {
1301 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1302 negated_type = "int_ge";
1303 } else if (simplified_type == "bool_ge" || simplified_type == "int_ge") {
1304 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1305 negated_type = "int_lt";
1306 } else if (simplified_type == "bool_gt" || simplified_type == "int_gt") {
1307 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1308 negated_type = "int_le";
1309 } else if (simplified_type == "int_lin_eq") {
1310 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1311 negated_type = "int_lin_ne";
1312 } else if (simplified_type == "int_lin_ne") {
1313 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1314 negated_type = "int_lin_eq";
1315 } else if (simplified_type == "int_lin_le") {
1316 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1317 negated_type = "int_lin_gt";
1318 } else if (simplified_type == "int_lin_ge") {
1319 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1320 negated_type = "int_lin_lt";
1321 } else if (simplified_type == "int_lin_lt") {
1322 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1323 negated_type = "int_lin_ge";
1324 } else if (simplified_type == "int_lin_gt") {
1325 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1326 negated_type = "int_lin_le";
1327 } else {
1328 LOG(FATAL) << "Unsupported " << simplified_type;
1329 }
1330
1331 // One way implication. We can stop here.
1332 if (absl::EndsWith(fz_ct.type, "_imp")) return;
1333
1334 // Add the other side of the reification because CpModelProto only support
1335 // half reification.
1336 ConstraintProto* negated_ct = proto.add_constraints();
1337 negated_ct->set_name(fz_ct.type + " (negated)");
1338 negated_ct->add_enforcement_literal(
1339 sat::NegatedRef(ct->enforcement_literal(0)));
1340 copy.type = negated_type;
1341 FillConstraint(copy, negated_ct);
1342}
1343
1344void CpModelProtoWithMapping::TranslateSearchAnnotations(
1345 absl::Span<const fz::Annotation> search_annotations, SolverLogger* logger) {
1346 std::vector<fz::Annotation> flat_annotations;
1347 for (const fz::Annotation& annotation : search_annotations) {
1348 fz::FlattenAnnotations(annotation, &flat_annotations);
1349 }
1350
1351 // CP-SAT rejects models containing variables duplicated in hints.
1352 absl::flat_hash_set<int> hinted_vars;
1353
1354 for (const fz::Annotation& annotation : flat_annotations) {
1355 if (annotation.IsFunctionCallWithIdentifier("warm_start")) {
1356 CHECK_EQ(2, annotation.annotations.size());
1357 const fz::Annotation& vars = annotation.annotations[0];
1358 const fz::Annotation& values = annotation.annotations[1];
1359 if (vars.type != fz::Annotation::VAR_REF_ARRAY ||
1360 values.type != fz::Annotation::INT_LIST) {
1361 continue;
1362 }
1363 for (int i = 0; i < vars.variables.size(); ++i) {
1364 fz::Variable* fz_var = vars.variables[i];
1365 const int var = fz_var_to_index.at(fz_var);
1366 const int64_t value = values.values[i];
1367 if (hinted_vars.insert(var).second) {
1368 proto.mutable_solution_hint()->add_vars(var);
1369 proto.mutable_solution_hint()->add_values(value);
1370 }
1371 }
1372 } else if (annotation.IsFunctionCallWithIdentifier("int_search") ||
1373 annotation.IsFunctionCallWithIdentifier("bool_search")) {
1374 const std::vector<fz::Annotation>& args = annotation.annotations;
1375 std::vector<fz::Variable*> vars;
1376 args[0].AppendAllVariables(&vars);
1377
1378 DecisionStrategyProto* strategy = proto.add_search_strategy();
1379 for (fz::Variable* v : vars) {
1380 strategy->add_variables(fz_var_to_index.at(v));
1381 }
1382
1383 const fz::Annotation& choose = args[1];
1384 if (choose.id == "input_order") {
1385 strategy->set_variable_selection_strategy(
1386 DecisionStrategyProto::CHOOSE_FIRST);
1387 } else if (choose.id == "first_fail") {
1388 strategy->set_variable_selection_strategy(
1389 DecisionStrategyProto::CHOOSE_MIN_DOMAIN_SIZE);
1390 } else if (choose.id == "anti_first_fail") {
1391 strategy->set_variable_selection_strategy(
1392 DecisionStrategyProto::CHOOSE_MAX_DOMAIN_SIZE);
1393 } else if (choose.id == "smallest") {
1394 strategy->set_variable_selection_strategy(
1395 DecisionStrategyProto::CHOOSE_LOWEST_MIN);
1396 } else if (choose.id == "largest") {
1397 strategy->set_variable_selection_strategy(
1398 DecisionStrategyProto::CHOOSE_HIGHEST_MAX);
1399 } else {
1400 SOLVER_LOG(logger, "Unsupported variable selection strategy '",
1401 choose.id, "', falling back to 'smallest'");
1402 strategy->set_variable_selection_strategy(
1403 DecisionStrategyProto::CHOOSE_LOWEST_MIN);
1404 }
1405
1406 const fz::Annotation& select = args[2];
1407 if (select.id == "indomain_min" || select.id == "indomain") {
1408 strategy->set_domain_reduction_strategy(
1409 DecisionStrategyProto::SELECT_MIN_VALUE);
1410 } else if (select.id == "indomain_max") {
1411 strategy->set_domain_reduction_strategy(
1412 DecisionStrategyProto::SELECT_MAX_VALUE);
1413 } else if (select.id == "indomain_split") {
1414 strategy->set_domain_reduction_strategy(
1415 DecisionStrategyProto::SELECT_LOWER_HALF);
1416 } else if (select.id == "indomain_reverse_split") {
1417 strategy->set_domain_reduction_strategy(
1418 DecisionStrategyProto::SELECT_UPPER_HALF);
1419 } else if (select.id == "indomain_median") {
1420 strategy->set_domain_reduction_strategy(
1421 DecisionStrategyProto::SELECT_MEDIAN_VALUE);
1422 } else {
1423 SOLVER_LOG(logger, "Unsupported value selection strategy '", select.id,
1424 "', falling back to 'indomain_min'");
1425 strategy->set_domain_reduction_strategy(
1426 DecisionStrategyProto::SELECT_MIN_VALUE);
1427 }
1428 }
1429 }
1430}
1431
1432// The format is fixed in the flatzinc specification.
1433std::string SolutionString(
1434 const fz::SolutionOutputSpecs& output,
1435 const std::function<int64_t(fz::Variable*)>& value_func,
1436 double objective_value) {
1437 if (output.variable != nullptr && !output.variable->domain.is_float) {
1438 const int64_t value = value_func(output.variable);
1439 if (output.display_as_boolean) {
1440 return absl::StrCat(output.name, " = ", value == 1 ? "true" : "false",
1441 ";");
1442 } else {
1443 return absl::StrCat(output.name, " = ", value, ";");
1444 }
1445 } else if (output.variable != nullptr && output.variable->domain.is_float) {
1446 return absl::StrCat(output.name, " = ", objective_value, ";");
1447 } else {
1448 const int bound_size = output.bounds.size();
1449 std::string result =
1450 absl::StrCat(output.name, " = array", bound_size, "d(");
1451 for (int i = 0; i < bound_size; ++i) {
1452 if (output.bounds[i].max_value >= output.bounds[i].min_value) {
1453 absl::StrAppend(&result, output.bounds[i].min_value, "..",
1454 output.bounds[i].max_value, ", ");
1455 } else {
1456 result.append("{},");
1457 }
1458 }
1459 result.append("[");
1460 for (int i = 0; i < output.flat_variables.size(); ++i) {
1461 const int64_t value = value_func(output.flat_variables[i]);
1462 if (output.display_as_boolean) {
1463 result.append(value ? "true" : "false");
1464 } else {
1465 absl::StrAppend(&result, value);
1466 }
1467 if (i != output.flat_variables.size() - 1) {
1468 result.append(", ");
1469 }
1470 }
1471 result.append("]);");
1472 return result;
1473 }
1474 return "";
1475}
1476
1477std::string SolutionString(
1478 const fz::Model& model,
1479 const std::function<int64_t(fz::Variable*)>& value_func,
1480 double objective_value) {
1481 std::string solution_string;
1482 for (const auto& output_spec : model.output()) {
1483 solution_string.append(
1484 SolutionString(output_spec, value_func, objective_value));
1485 solution_string.append("\n");
1486 }
1487 return solution_string;
1488}
1489
1490void OutputFlatzincStats(const CpSolverResponse& response,
1491 SolverLogger* solution_logger) {
1492 SOLVER_LOG(solution_logger,
1493 "%%%mzn-stat: objective=", response.objective_value());
1494 SOLVER_LOG(solution_logger,
1495 "%%%mzn-stat: objectiveBound=", response.best_objective_bound());
1496 SOLVER_LOG(solution_logger,
1497 "%%%mzn-stat: boolVariables=", response.num_booleans());
1498 SOLVER_LOG(solution_logger,
1499 "%%%mzn-stat: failures=", response.num_conflicts());
1500 SOLVER_LOG(
1501 solution_logger, "%%%mzn-stat: propagations=",
1502 response.num_binary_propagations() + response.num_integer_propagations());
1503 SOLVER_LOG(solution_logger, "%%%mzn-stat: solveTime=", response.wall_time());
1504}
1505
1506} // namespace
1507
1509 // Scan the model, rename int2float to int_eq, change type of the floating
1510 // point variables to integer.
1511 for (fz::Constraint* ct : fz_model->constraints()) {
1512 if (!ct->active) continue;
1513 if (ct->type == "int2float") {
1514 ct->type = "int_eq";
1515 fz::Domain& float_domain = ct->arguments[1].variables[0]->domain;
1516 float_domain.is_float = false;
1517 for (const double float_value : float_domain.float_values) {
1518 float_domain.values.push_back(static_cast<int64_t>(float_value));
1519 }
1520 float_domain.float_values.clear();
1521 }
1522 }
1523
1524 // Scan the model to find the float objective variable and the float objective
1525 // constraint if defined.
1526 fz::Variable* float_objective_var = nullptr;
1527 for (fz::Variable* var : fz_model->variables()) {
1528 if (!var->active) continue;
1529 if (var->domain.is_float) {
1530 CHECK(float_objective_var == nullptr);
1531 float_objective_var = var;
1532 }
1533 }
1534
1535 fz::Constraint* float_objective_ct = nullptr;
1536 if (float_objective_var != nullptr) {
1537 for (fz::Constraint* ct : fz_model->constraints()) {
1538 if (!ct->active) continue;
1539 if (ct->type == "float_lin_eq") {
1540 CHECK(float_objective_ct == nullptr);
1541 float_objective_ct = ct;
1542 break;
1543 }
1544 }
1545 }
1546
1547 if (float_objective_ct != nullptr || float_objective_var != nullptr) {
1548 CHECK(float_objective_ct != nullptr);
1549 CHECK(float_objective_var != nullptr);
1550 const int arity = float_objective_ct->arguments[0].Size();
1551 CHECK_EQ(float_objective_ct->arguments[1].variables[arity - 1],
1552 float_objective_var);
1553 CHECK_EQ(float_objective_ct->arguments[0].floats[arity - 1], -1.0);
1554 for (int i = 0; i + 1 < arity; ++i) {
1556 float_objective_ct->arguments[1].variables[i],
1557 float_objective_ct->arguments[0].floats[i]);
1558 }
1560 -float_objective_ct->arguments[2].floats[0]);
1561 fz_model->ClearObjective();
1562 float_objective_var->active = false;
1563 float_objective_ct->active = false;
1564 }
1565}
1566
1569 const std::string& sat_params,
1570 SolverLogger* logger,
1571 SolverLogger* solution_logger) {
1572 CpModelProtoWithMapping m;
1573 m.proto.set_name(fz_model.name());
1574
1575 // The translation is easy, we create one variable per flatzinc variable,
1576 // plus eventually a bunch of constant variables that will be created
1577 // lazily.
1578 int num_variables = 0;
1579 for (fz::Variable* fz_var : fz_model.variables()) {
1580 if (!fz_var->active) continue;
1581 CHECK(!fz_var->domain.is_float)
1582 << "CP-SAT does not support float variables";
1583
1584 m.fz_var_to_index[fz_var] = num_variables++;
1585 IntegerVariableProto* var = m.proto.add_variables();
1586 var->set_name(fz_var->name);
1587 if (fz_var->domain.is_interval) {
1588 if (fz_var->domain.values.empty()) {
1589 // The CP-SAT solver checks that constraints cannot overflow during
1590 // their propagation. Because of that, we trim undefined variable
1591 // domains (i.e. int in minizinc) to something hopefully large enough.
1592 LOG_FIRST_N(WARNING, 1)
1593 << "Using flag --fz_int_max for unbounded integer variables.";
1594 LOG_FIRST_N(WARNING, 1)
1595 << " actual domain is [" << -absl::GetFlag(FLAGS_fz_int_max)
1596 << ".." << absl::GetFlag(FLAGS_fz_int_max) << "]";
1597 var->add_domain(-absl::GetFlag(FLAGS_fz_int_max));
1598 var->add_domain(absl::GetFlag(FLAGS_fz_int_max));
1599 } else {
1600 var->add_domain(fz_var->domain.values[0]);
1601 var->add_domain(fz_var->domain.values[1]);
1602 }
1603 } else {
1604 FillDomainInProto(Domain::FromValues(fz_var->domain.values), var);
1605 }
1606 }
1607
1608 // Translate the constraints.
1609 for (fz::Constraint* fz_ct : fz_model.constraints()) {
1610 if (fz_ct == nullptr || !fz_ct->active) continue;
1611 ConstraintProto* ct = m.proto.add_constraints();
1612 ct->set_name(fz_ct->type);
1613 if (absl::EndsWith(fz_ct->type, "_reif") ||
1614 absl::EndsWith(fz_ct->type, "_imp") || fz_ct->type == "array_bool_or" ||
1615 fz_ct->type == "array_bool_and") {
1616 m.FillReifOrImpliedConstraint(*fz_ct, ct);
1617 } else {
1618 m.FillConstraint(*fz_ct, ct);
1619 }
1620 }
1621
1622 // Fill the objective.
1623 if (fz_model.objective() != nullptr) {
1624 CpObjectiveProto* objective = m.proto.mutable_objective();
1625 if (fz_model.maximize()) {
1626 objective->set_scaling_factor(-1);
1627 objective->add_coeffs(-1);
1628 objective->add_vars(m.fz_var_to_index[fz_model.objective()]);
1629 } else {
1630 objective->add_coeffs(1);
1631 objective->add_vars(m.fz_var_to_index[fz_model.objective()]);
1632 }
1633 } else if (!fz_model.float_objective_variables().empty()) {
1634 FloatObjectiveProto* objective = m.proto.mutable_floating_point_objective();
1635 for (int i = 0; i < fz_model.float_objective_variables().size(); ++i) {
1636 objective->add_vars(
1637 m.fz_var_to_index[fz_model.float_objective_variables()[i]]);
1638 objective->add_coeffs(fz_model.float_objective_coefficients()[i]);
1639 }
1640 objective->set_offset(fz_model.float_objective_offset());
1641 objective->set_maximize(fz_model.maximize());
1642 }
1643
1644 // Fill the search order.
1645 m.TranslateSearchAnnotations(fz_model.search_annotations(), logger);
1646
1647 if (p.search_all_solutions && !m.proto.has_objective()) {
1648 // Enumerate all sat solutions.
1649 m.parameters.set_enumerate_all_solutions(true);
1650 }
1651
1652 m.parameters.set_log_search_progress(p.log_search_progress);
1653 m.parameters.set_log_to_stdout(!p.ortools_mode);
1654
1655 // Helps with challenge unit tests.
1656 m.parameters.set_max_domain_size_when_encoding_eq_neq_constraints(32);
1657
1658 // Computes the number of workers.
1659 int num_workers = 1;
1660 if (p.search_all_solutions && fz_model.objective() == nullptr) {
1661 if (p.number_of_threads > 1) {
1662 // We don't support enumerating all solution in parallel for a SAT
1663 // problem. But note that we do support it for an optimization problem
1664 // since the meaning of p.all_solutions is not the same in this case.
1665 SOLVER_LOG(logger,
1666 "Search for all solutions of a SAT problem in parallel is not "
1667 "supported. Switching back to sequential search.");
1668 }
1669 } else if (p.number_of_threads <= 0) {
1670 // TODO(user): Supports setting the number of workers to 0, which will
1671 // then query the number of cores available. This is complex now as we
1672 // need to still support the expected behabior (no flags -> 1 thread
1673 // fixed search, -f -> 1 thread free search).
1674 SOLVER_LOG(logger,
1675 "The number of search workers, is not specified. For better "
1676 "performances, please set the number of workers to 8, 16, or "
1677 "more depending on the number of cores of your computer.");
1678 } else {
1679 num_workers = p.number_of_threads;
1680 }
1681
1682 // Specifies single thread specific search modes.
1683 if (num_workers == 1 && !p.use_free_search) { // Fixed search.
1684 m.parameters.set_search_branching(SatParameters::FIXED_SEARCH);
1685 m.parameters.set_keep_all_feasible_solutions_in_presolve(true);
1686 } else if (num_workers == 1 && p.use_free_search) { // Free search.
1687 m.parameters.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
1688 if (!p.search_all_solutions &&
1689 (absl::GetFlag(FLAGS_force_interleave_search) || p.ortools_mode)) {
1690 m.parameters.set_interleave_search(true);
1691 m.parameters.set_use_rins_lns(false);
1692 m.parameters.add_subsolvers("default_lp");
1693 m.parameters.add_subsolvers("max_lp");
1694 m.parameters.add_subsolvers("quick_restart");
1695 m.parameters.add_subsolvers("core_or_no_lp"); // no_lp if no objective.
1696 m.parameters.set_num_violation_ls(1); // Off if no objective.
1697 if (!m.proto.search_strategy().empty()) {
1698 m.parameters.add_subsolvers("fixed");
1699 }
1700 }
1701 } else if (num_workers > 1 && num_workers < 8 && p.ortools_mode) {
1702 SOLVER_LOG(logger, "Bumping number of workers from ", num_workers, " to 8");
1703 num_workers = 8;
1704 }
1705 m.parameters.set_num_workers(num_workers);
1706
1707 // Time limit.
1708 if (p.max_time_in_seconds > 0) {
1709 m.parameters.set_max_time_in_seconds(p.max_time_in_seconds);
1710 }
1711
1712 // The order is important, we want the flag parameters to overwrite anything
1713 // set in m.parameters.
1714 sat::SatParameters flag_parameters;
1715 CHECK(google::protobuf::TextFormat::ParseFromString(sat_params,
1716 &flag_parameters))
1717 << sat_params;
1718 m.parameters.MergeFrom(flag_parameters);
1719
1720 // We only need an observer if 'p.display_all_solutions' or
1721 // 'p.search_all_solutions' are true.
1722 std::function<void(const CpSolverResponse&)> solution_observer = nullptr;
1724 solution_observer = [&fz_model, &m, &p,
1725 solution_logger](const CpSolverResponse& r) {
1726 const std::string solution_string = SolutionString(
1727 fz_model,
1728 [&m, &r](fz::Variable* v) {
1729 return r.solution(m.fz_var_to_index.at(v));
1730 },
1731 r.objective_value());
1732 SOLVER_LOG(solution_logger, solution_string);
1733 if (p.display_statistics) {
1734 OutputFlatzincStats(r, solution_logger);
1735 }
1736 SOLVER_LOG(solution_logger, "----------");
1737 };
1738 }
1739
1740 Model sat_model;
1741
1742 // Setup logging.
1743 // Note that we need to do that before we start calling the sat functions
1744 // below that might create a SolverLogger() themselves.
1745 sat_model.Register<SolverLogger>(logger);
1746
1747 sat_model.Add(NewSatParameters(m.parameters));
1748 if (solution_observer != nullptr) {
1749 sat_model.Add(NewFeasibleSolutionObserver(solution_observer));
1750 }
1751
1752 const CpSolverResponse response = SolveCpModel(m.proto, &sat_model);
1753
1754 // Check the returned solution with the fz model checker.
1755 if (response.status() == CpSolverStatus::FEASIBLE ||
1756 response.status() == CpSolverStatus::OPTIMAL) {
1757 CHECK(CheckSolution(
1758 fz_model,
1759 [&response, &m](fz::Variable* v) {
1760 return response.solution(m.fz_var_to_index.at(v));
1761 },
1762 logger));
1763 }
1764
1765 // Output the solution in the flatzinc official format.
1766 if (p.ortools_mode) {
1767 if (response.status() == CpSolverStatus::FEASIBLE ||
1768 response.status() == CpSolverStatus::OPTIMAL) {
1770 // Already printed otherwise.
1771 const std::string solution_string = SolutionString(
1772 fz_model,
1773 [&response, &m](fz::Variable* v) {
1774 return response.solution(m.fz_var_to_index.at(v));
1775 },
1776 response.objective_value());
1777 SOLVER_LOG(solution_logger, solution_string);
1778 SOLVER_LOG(solution_logger, "----------");
1779 }
1780 if (response.status() == CpSolverStatus::OPTIMAL) {
1781 SOLVER_LOG(solution_logger, "==========");
1782 }
1783 } else if (response.status() == CpSolverStatus::INFEASIBLE) {
1784 SOLVER_LOG(solution_logger, "=====UNSATISFIABLE=====");
1785 } else if (response.status() == CpSolverStatus::MODEL_INVALID) {
1786 const std::string error_message = ValidateCpModel(m.proto);
1787 VLOG(1) << "%% Error message = '" << error_message << "'";
1788 if (absl::StrContains(error_message, "overflow")) {
1789 SOLVER_LOG(solution_logger, "=====OVERFLOW=====");
1790 } else {
1791 SOLVER_LOG(solution_logger, "=====MODEL INVALID=====");
1792 }
1793 } else {
1794 SOLVER_LOG(solution_logger, "%% TIMEOUT");
1795 }
1796 if (p.display_statistics) {
1797 OutputFlatzincStats(response, solution_logger);
1798 }
1799 }
1800}
1801
1802} // namespace sat
1803} // namespace operations_research
static Domain FromValues(std::vector< int64_t > values)
Domain AdditionWith(const Domain &domain) const
const std::vector< double > & float_objective_coefficients() const
Definition model.h:383
void AddFloatingPointObjectiveTerm(Variable *var, double coeff)
Definition model.h:389
const std::vector< Variable * > & float_objective_variables() const
Definition model.h:380
const std::vector< Constraint * > & constraints() const
Definition model.h:373
void SetFloatingPointObjectiveOffset(double offset)
Definition model.h:393
const std::vector< Variable * > & variables() const
--— Accessors and mutators --—
Definition model.h:372
double float_objective_offset() const
Definition model.h:386
const std::string & name() const
Definition model.h:400
const std::vector< Annotation > & search_annotations() const
Definition model.h:374
Variable * objective() const
Definition model.h:379
::operations_research::sat::LinearConstraintProto *PROTOBUF_NONNULL mutable_linear()
void set_name(Arg_ &&arg, Args_... args)
const ::operations_research::sat::IntegerVariableProto & variables(int index) const
int constraints_size() const
repeated .operations_research.sat.ConstraintProto constraints = 3;
::operations_research::sat::IntegerVariableProto *PROTOBUF_NONNULL add_variables()
::operations_research::sat::PartialVariableAssignment *PROTOBUF_NONNULL mutable_solution_hint()
::operations_research::sat::ConstraintProto *PROTOBUF_NONNULL add_constraints()
int variables_size() const
repeated .operations_research.sat.IntegerVariableProto variables = 2;
::operations_research::sat::IntegerVariableProto *PROTOBUF_NONNULL mutable_variables(int index)
::operations_research::sat::DecisionStrategyProto *PROTOBUF_NONNULL add_search_strategy()
::operations_research::sat::CpSolverStatus status() const
void set_name(Arg_ &&arg, Args_... args)
T Add(std::function< T(Model *)> f)
Definition model.h:87
void Register(T *non_owned_class)
Definition model.h:177
static constexpr SearchBranching AUTOMATIC_SEARCH
static constexpr SearchBranching FIXED_SEARCH
ABSL_FLAG(int64_t, fz_int_max, int64_t{1}<< 40, "Default max value for unbounded integer variables.")
ReverseView< Container > reversed_view(const Container &c)
std::string ValidateCpModel(const CpModelProto &model, bool after_presolve)
void SolveFzWithCpModelProto(const fz::Model &fz_model, const fz::FlatzincSatParameters &p, const std::string &sat_params, SolverLogger *logger, SolverLogger *solution_logger)
Solves the given flatzinc model using the CP-SAT solver.
std::function< SatParameters(Model *)> NewSatParameters(absl::string_view params)
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Serializes a Domain into the domain field of a proto.
CpSolverResponse SolveCpModel(const CpModelProto &model_proto, Model *model)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
std::function< void(Model *)> NewFeasibleSolutionObserver(const std::function< void(const CpSolverResponse &response)> &callback)
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
void ProcessFloatingPointOVariablesAndObjective(fz::Model *fz_model)
In SWIG mode, we don't want anything besides these top-level includes.
int64_t Max() const
Returns the max of the domain.
Definition model.cc:346
int64_t Min() const
Returns the min of the domain.
Definition model.cc:340
std::vector< Argument > arguments
Definition model.h:240
std::vector< int64_t > values
These should never be modified from outside the class.
Definition model.h:107
bool is_float
Float domain.
Definition model.h:113
std::vector< double > float_values
Definition model.h:114
#define SOLVER_LOG(logger,...)
Definition logging.h:110