25#include "absl/container/flat_hash_map.h"
26#include "absl/container/flat_hash_set.h"
27#include "absl/flags/flag.h"
28#include "absl/log/check.h"
29#include "absl/strings/match.h"
30#include "absl/strings/str_cat.h"
31#include "absl/types/span.h"
32#include "google/protobuf/text_format.h"
37#include "ortools/sat/cp_model.pb.h"
42#include "ortools/sat/sat_parameters.pb.h"
47 "Default max value for unbounded integer variables.");
54static const int kNoVar = std::numeric_limits<int>::min();
62int TrueLiteral(
int var) {
return var; }
63int FalseLiteral(
int var) {
return -var - 1; }
66struct CpModelProtoWithMapping {
68 int LookupConstant(int64_t value);
72 int LookupVar(
const fz::Argument& argument);
73 LinearExpressionProto LookupExpr(
const fz::Argument& argument,
75 LinearExpressionProto LookupExprAt(
const fz::Argument& argument,
int pos,
77 std::vector<int> LookupVars(
const fz::Argument& argument);
78 std::vector<VarOrValue> LookupVarsOrValues(
const fz::Argument& argument);
83 std::vector<int> CreateIntervals(absl::Span<const VarOrValue> starts,
84 absl::Span<const VarOrValue> sizes);
93 std::vector<int> CreateNonZeroOrOptionalIntervals(
94 absl::Span<const VarOrValue> starts, absl::Span<const VarOrValue> sizes);
101 int GetOrCreateOptionalInterval(VarOrValue start_var, VarOrValue size,
106 int NonZeroLiteralFrom(VarOrValue size);
110 ConstraintProto* AddEnforcedConstraint(
int literal);
113 void FillAMinusBInDomain(
const std::vector<int64_t>& domain,
114 const fz::Constraint& fz_ct, ConstraintProto* ct);
115 void FillLinearConstraintWithGivenDomain(absl::Span<const int64_t> domain,
116 const fz::Constraint& fz_ct,
117 ConstraintProto* ct);
118 void FillConstraint(
const fz::Constraint& fz_ct, ConstraintProto* ct);
119 void FillReifOrImpliedConstraint(
const fz::Constraint& fz_ct,
120 ConstraintProto* ct);
121 void BuildTableFromDomainIntLinEq(
const fz::Constraint& fz_ct,
122 ConstraintProto* ct);
126 void TranslateSearchAnnotations(
127 absl::Span<const fz::Annotation> search_annotations,
128 SolverLogger* logger);
132 SatParameters parameters;
135 absl::flat_hash_map<fz::Variable*, int> fz_var_to_index;
136 absl::flat_hash_map<int64_t, int> constant_value_to_index;
137 absl::flat_hash_map<std::tuple<int, int64_t, int, int64_t, int>,
int>
138 interval_key_to_index;
139 absl::flat_hash_map<int, int> var_to_lit_implies_greater_than_zero;
142int CpModelProtoWithMapping::LookupConstant(int64_t value) {
143 if (constant_value_to_index.contains(value)) {
144 return constant_value_to_index[value];
148 const int index = proto.variables_size();
149 IntegerVariableProto* var_proto = proto.add_variables();
150 var_proto->add_domain(value);
151 var_proto->add_domain(value);
152 constant_value_to_index[value] = index;
156int CpModelProtoWithMapping::LookupVar(
const fz::Argument& argument) {
157 if (argument.HasOneValue())
return LookupConstant(argument.Value());
158 CHECK_EQ(argument.type, fz::Argument::VAR_REF);
159 return fz_var_to_index[argument.Var()];
162LinearExpressionProto CpModelProtoWithMapping::LookupExpr(
163 const fz::Argument& argument,
bool negate) {
164 LinearExpressionProto expr;
165 if (argument.HasOneValue()) {
166 const int64_t value = argument.Value();
167 expr.set_offset(negate ? -value : value);
169 expr.add_vars(LookupVar(argument));
170 expr.add_coeffs(negate ? -1 : 1);
175LinearExpressionProto CpModelProtoWithMapping::LookupExprAt(
176 const fz::Argument& argument,
int pos,
bool negate) {
177 LinearExpressionProto expr;
178 if (argument.HasOneValueAt(pos)) {
179 const int64_t value = argument.ValueAt(pos);
180 expr.set_offset(negate ? -value : value);
182 expr.add_vars(fz_var_to_index[argument.VarAt(pos)]);
183 expr.add_coeffs(negate ? -1 : 1);
188std::vector<int> CpModelProtoWithMapping::LookupVars(
189 const fz::Argument& argument) {
190 std::vector<int> result;
191 if (argument.type == fz::Argument::VOID_ARGUMENT)
return result;
192 if (argument.type == fz::Argument::INT_LIST) {
193 for (int64_t value : argument.values) {
194 result.push_back(LookupConstant(value));
196 }
else if (argument.type == fz::Argument::INT_VALUE) {
197 result.push_back(LookupConstant(argument.Value()));
199 CHECK_EQ(argument.type, fz::Argument::VAR_REF_ARRAY);
200 for (fz::Variable* var : argument.variables) {
201 CHECK(var !=
nullptr);
202 result.push_back(fz_var_to_index[var]);
208std::vector<VarOrValue> CpModelProtoWithMapping::LookupVarsOrValues(
209 const fz::Argument& argument) {
210 std::vector<VarOrValue> result;
211 const int no_var = kNoVar;
212 if (argument.type == fz::Argument::VOID_ARGUMENT)
return result;
213 if (argument.type == fz::Argument::INT_LIST) {
214 for (int64_t value : argument.values) {
215 result.push_back({no_var, value});
217 }
else if (argument.type == fz::Argument::INT_VALUE) {
218 result.push_back({no_var, argument.Value()});
220 CHECK_EQ(argument.type, fz::Argument::VAR_REF_ARRAY);
221 for (fz::Variable* var : argument.variables) {
222 CHECK(var !=
nullptr);
223 if (var->domain.HasOneValue()) {
224 result.push_back({no_var, var->domain.Value()});
226 result.push_back({fz_var_to_index[var], 0});
233ConstraintProto* CpModelProtoWithMapping::AddEnforcedConstraint(
int literal) {
234 ConstraintProto* result = proto.add_constraints();
235 if (literal != kNoVar) {
236 result->add_enforcement_literal(literal);
241int CpModelProtoWithMapping::GetOrCreateOptionalInterval(VarOrValue start,
244 const int interval_index = proto.constraints_size();
245 const std::tuple<int, int64_t, int, int64_t, int> key =
246 std::make_tuple(start.var, start.value, size.var, size.value, opt_var);
247 const auto [it, inserted] =
248 interval_key_to_index.insert({key, interval_index});
253 if (size.var == kNoVar || start.var == kNoVar) {
254 auto* interval = AddEnforcedConstraint(opt_var)->mutable_interval();
255 if (start.var != kNoVar) {
256 interval->mutable_start()->add_vars(start.var);
257 interval->mutable_start()->add_coeffs(1);
258 interval->mutable_end()->add_vars(start.var);
259 interval->mutable_end()->add_coeffs(1);
261 interval->mutable_start()->set_offset(start.value);
262 interval->mutable_end()->set_offset(start.value);
265 if (size.var != kNoVar) {
266 interval->mutable_size()->add_vars(size.var);
267 interval->mutable_size()->add_coeffs(1);
268 interval->mutable_end()->add_vars(size.var);
269 interval->mutable_end()->add_coeffs(1);
271 interval->mutable_size()->set_offset(size.value);
272 interval->mutable_end()->set_offset(size.value +
273 interval->end().offset());
275 return interval_index;
277 const int end_var = proto.variables_size();
281 proto.add_variables());
284 auto* interval = AddEnforcedConstraint(opt_var)->mutable_interval();
285 interval->mutable_start()->add_vars(start.var);
286 interval->mutable_start()->add_coeffs(1);
287 interval->mutable_size()->add_vars(size.var);
288 interval->mutable_size()->add_coeffs(1);
289 interval->mutable_end()->add_vars(end_var);
290 interval->mutable_end()->add_coeffs(1);
294 auto* lin = AddEnforcedConstraint(opt_var)->mutable_linear();
295 lin->add_vars(start.var);
297 lin->add_vars(size.var);
299 lin->add_vars(end_var);
304 return interval_index;
308std::vector<int> CpModelProtoWithMapping::CreateIntervals(
309 absl::Span<const VarOrValue> starts, absl::Span<const VarOrValue> sizes) {
310 std::vector<int> intervals;
311 for (
int i = 0;
i < starts.size(); ++
i) {
313 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
318std::vector<int> CpModelProtoWithMapping::CreateNonZeroOrOptionalIntervals(
319 absl::Span<const VarOrValue> starts, absl::Span<const VarOrValue> sizes) {
320 std::vector<int> intervals;
321 for (
int i = 0;
i < starts.size(); ++
i) {
322 const int opt_var = NonZeroLiteralFrom(sizes[i]);
324 GetOrCreateOptionalInterval(starts[i], sizes[i], opt_var));
329int CpModelProtoWithMapping::NonZeroLiteralFrom(VarOrValue size) {
330 if (size.var == kNoVar) {
331 return LookupConstant(size.value > 0);
333 const auto it = var_to_lit_implies_greater_than_zero.find(size.var);
334 if (it != var_to_lit_implies_greater_than_zero.end()) {
338 const IntegerVariableProto& var_proto = proto.variables(size.var);
340 DCHECK_GE(domain.
Min(), 0);
341 if (domain.
Min() > 0)
return LookupConstant(1);
342 if (domain.
Max() == 0) {
343 return LookupConstant(0);
346 const int var_greater_than_zero_lit = proto.variables_size();
347 IntegerVariableProto* lit_proto = proto.add_variables();
348 lit_proto->add_domain(0);
349 lit_proto->add_domain(1);
351 ConstraintProto* is_greater =
352 AddEnforcedConstraint(TrueLiteral(var_greater_than_zero_lit));
353 is_greater->mutable_linear()->add_vars(size.var);
354 is_greater->mutable_linear()->add_coeffs(1);
355 const Domain positive = domain.IntersectionWith({1, domain.
Max()});
358 ConstraintProto* is_null =
359 AddEnforcedConstraint(FalseLiteral(var_greater_than_zero_lit));
360 is_null->mutable_linear()->add_vars(size.var);
361 is_null->mutable_linear()->add_coeffs(1);
362 is_null->mutable_linear()->add_domain(0);
363 is_null->mutable_linear()->add_domain(0);
365 var_to_lit_implies_greater_than_zero[size.var] = var_greater_than_zero_lit;
366 return var_greater_than_zero_lit;
369void CpModelProtoWithMapping::FillAMinusBInDomain(
370 const std::vector<int64_t>& domain,
const fz::Constraint& fz_ct,
371 ConstraintProto* ct) {
372 auto* arg = ct->mutable_linear();
373 if (fz_ct.arguments[1].type == fz::Argument::INT_VALUE) {
374 const int64_t value = fz_ct.arguments[1].Value();
375 const int var_a = LookupVar(fz_ct.arguments[0]);
376 for (
const int64_t domain_bound : domain) {
377 if (domain_bound == std::numeric_limits<int64_t>::min() ||
378 domain_bound == std::numeric_limits<int64_t>::max()) {
379 arg->add_domain(domain_bound);
381 arg->add_domain(domain_bound + value);
384 arg->add_vars(var_a);
386 }
else if (fz_ct.arguments[0].type == fz::Argument::INT_VALUE) {
387 const int64_t value = fz_ct.arguments[0].Value();
388 const int var_b = LookupVar(fz_ct.arguments[1]);
390 if (domain_bound == std::numeric_limits<int64_t>::min()) {
391 arg->add_domain(std::numeric_limits<int64_t>::max());
392 }
else if (domain_bound == std::numeric_limits<int64_t>::max()) {
393 arg->add_domain(std::numeric_limits<int64_t>::min());
395 arg->add_domain(value - domain_bound);
398 arg->add_vars(var_b);
401 for (
const int64_t domain_bound : domain) arg->add_domain(domain_bound);
402 arg->add_vars(LookupVar(fz_ct.arguments[0]));
404 arg->add_vars(LookupVar(fz_ct.arguments[1]));
409void CpModelProtoWithMapping::FillLinearConstraintWithGivenDomain(
410 absl::Span<const int64_t> domain,
const fz::Constraint& fz_ct,
411 ConstraintProto* ct) {
412 auto* arg = ct->mutable_linear();
413 for (
const int64_t domain_bound : domain) arg->add_domain(domain_bound);
414 std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
415 for (
int i = 0;
i < vars.size(); ++
i) {
416 arg->add_vars(vars[i]);
417 arg->add_coeffs(fz_ct.arguments[0].values[i]);
421void CpModelProtoWithMapping::BuildTableFromDomainIntLinEq(
422 const fz::Constraint& fz_ct, ConstraintProto* ct) {
423 const std::vector<int64_t>& coeffs = fz_ct.arguments[0].values;
424 const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
425 const int rhs = fz_ct.arguments[2].Value();
426 CHECK_EQ(coeffs.back(), -1);
427 for (
const int var : vars) {
428 LinearExpressionProto* expr = ct->mutable_table()->add_exprs();
433 switch (vars.size()) {
437 for (
const int64_t v0 : domain0.Values()) {
438 for (
const int64_t v1 : domain1.Values()) {
439 const int64_t v2 = coeffs[0] * v0 + coeffs[1] * v1 - rhs;
440 ct->mutable_table()->add_values(v0);
441 ct->mutable_table()->add_values(v1);
442 ct->mutable_table()->add_values(v2);
451 for (
const int64_t v0 : domain0.Values()) {
452 for (
const int64_t v1 : domain1.Values()) {
453 for (
const int64_t v2 : domain2.Values()) {
455 coeffs[0] * v0 + coeffs[1] * v1 + coeffs[2] * v2 - rhs;
456 ct->mutable_table()->add_values(v0);
457 ct->mutable_table()->add_values(v1);
458 ct->mutable_table()->add_values(v2);
459 ct->mutable_table()->add_values(v3);
466 LOG(FATAL) <<
"Unsupported size";
470void CpModelProtoWithMapping::FillConstraint(
const fz::Constraint& fz_ct,
471 ConstraintProto* ct) {
472 if (fz_ct.type ==
"false_constraint") {
474 ct->mutable_bool_or();
475 }
else if (fz_ct.type ==
"bool_clause") {
476 auto* arg = ct->mutable_bool_or();
477 for (
const int var : LookupVars(fz_ct.arguments[0])) {
478 arg->add_literals(TrueLiteral(var));
480 for (
const int var : LookupVars(fz_ct.arguments[1])) {
481 arg->add_literals(FalseLiteral(var));
483 }
else if (fz_ct.type ==
"bool_xor") {
486 const int a = LookupVar(fz_ct.arguments[0]);
487 const int b = LookupVar(fz_ct.arguments[1]);
488 const int x = LookupVar(fz_ct.arguments[2]);
492 auto*
const refute = ct->mutable_linear();
494 refute->add_coeffs(1);
496 refute->add_coeffs(-1);
497 refute->add_domain(0);
498 refute->add_domain(0);
501 auto* enforce = AddEnforcedConstraint(x)->mutable_linear();
502 enforce->add_vars(a);
503 enforce->add_coeffs(1);
504 enforce->add_vars(b);
505 enforce->add_coeffs(1);
506 enforce->add_domain(1);
507 enforce->add_domain(1);
508 }
else if (fz_ct.type ==
"array_bool_or") {
509 auto* arg = ct->mutable_bool_or();
510 for (
const int var : LookupVars(fz_ct.arguments[0])) {
511 arg->add_literals(TrueLiteral(var));
513 }
else if (fz_ct.type ==
"array_bool_or_negated") {
514 auto* arg = ct->mutable_bool_and();
515 for (
const int var : LookupVars(fz_ct.arguments[0])) {
516 arg->add_literals(FalseLiteral(var));
518 }
else if (fz_ct.type ==
"array_bool_and") {
519 auto* arg = ct->mutable_bool_and();
520 for (
const int var : LookupVars(fz_ct.arguments[0])) {
521 arg->add_literals(TrueLiteral(var));
523 }
else if (fz_ct.type ==
"array_bool_and_negated") {
524 auto* arg = ct->mutable_bool_or();
525 for (
const int var : LookupVars(fz_ct.arguments[0])) {
526 arg->add_literals(FalseLiteral(var));
528 }
else if (fz_ct.type ==
"array_bool_xor") {
529 auto* arg = ct->mutable_bool_xor();
530 for (
const int var : LookupVars(fz_ct.arguments[0])) {
531 arg->add_literals(TrueLiteral(var));
533 }
else if (fz_ct.type ==
"bool_le" || fz_ct.type ==
"int_le") {
534 FillAMinusBInDomain({std::numeric_limits<int64_t>::min(), 0}, fz_ct, ct);
535 }
else if (fz_ct.type ==
"bool_ge" || fz_ct.type ==
"int_ge") {
536 FillAMinusBInDomain({0, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
537 }
else if (fz_ct.type ==
"bool_lt" || fz_ct.type ==
"int_lt") {
538 FillAMinusBInDomain({std::numeric_limits<int64_t>::min(), -1}, fz_ct, ct);
539 }
else if (fz_ct.type ==
"bool_gt" || fz_ct.type ==
"int_gt") {
540 FillAMinusBInDomain({1, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
541 }
else if (fz_ct.type ==
"bool_eq" || fz_ct.type ==
"int_eq" ||
542 fz_ct.type ==
"bool2int") {
543 FillAMinusBInDomain({0, 0}, fz_ct, ct);
544 }
else if (fz_ct.type ==
"bool_ne" || fz_ct.type ==
"bool_not") {
545 auto* arg = ct->mutable_linear();
546 arg->add_vars(LookupVar(fz_ct.arguments[0]));
548 arg->add_vars(LookupVar(fz_ct.arguments[1]));
552 }
else if (fz_ct.type ==
"int_ne") {
553 FillAMinusBInDomain({std::numeric_limits<int64_t>::min(), -1, 1,
554 std::numeric_limits<int64_t>::max()},
556 }
else if (fz_ct.type ==
"int_lin_eq") {
558 if (fz_ct.strong_propagation && fz_ct.arguments[0].Size() >= 3 &&
559 fz_ct.arguments[0].Size() <= 4 &&
560 fz_ct.arguments[0].values.back() == -1) {
561 BuildTableFromDomainIntLinEq(fz_ct, ct);
563 const int64_t rhs = fz_ct.arguments[2].values[0];
564 FillLinearConstraintWithGivenDomain({rhs, rhs}, fz_ct, ct);
566 }
else if (fz_ct.type ==
"bool_lin_eq") {
567 auto* arg = ct->mutable_linear();
568 const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
569 for (
int i = 0;
i < vars.size(); ++
i) {
570 arg->add_vars(vars[i]);
571 arg->add_coeffs(fz_ct.arguments[0].values[i]);
573 if (fz_ct.arguments[2].IsVariable()) {
574 arg->add_vars(LookupVar(fz_ct.arguments[2]));
579 const int64_t v = fz_ct.arguments[2].Value();
583 }
else if (fz_ct.type ==
"int_lin_le" || fz_ct.type ==
"bool_lin_le") {
584 const int64_t rhs = fz_ct.arguments[2].values[0];
585 FillLinearConstraintWithGivenDomain(
586 {std::numeric_limits<int64_t>::min(), rhs}, fz_ct, ct);
587 }
else if (fz_ct.type ==
"int_lin_lt") {
588 const int64_t rhs = fz_ct.arguments[2].values[0];
589 FillLinearConstraintWithGivenDomain(
590 {std::numeric_limits<int64_t>::min(), rhs - 1}, fz_ct, ct);
591 }
else if (fz_ct.type ==
"int_lin_ge") {
592 const int64_t rhs = fz_ct.arguments[2].values[0];
593 FillLinearConstraintWithGivenDomain(
594 {rhs, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
595 }
else if (fz_ct.type ==
"int_lin_gt") {
596 const int64_t rhs = fz_ct.arguments[2].values[0];
597 FillLinearConstraintWithGivenDomain(
598 {rhs + 1, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
599 }
else if (fz_ct.type ==
"int_lin_ne") {
600 const int64_t rhs = fz_ct.arguments[2].values[0];
601 FillLinearConstraintWithGivenDomain(
602 {std::numeric_limits<int64_t>::min(), rhs - 1, rhs + 1,
603 std::numeric_limits<int64_t>::max()},
605 }
else if (fz_ct.type ==
"set_in") {
606 auto* arg = ct->mutable_linear();
607 arg->add_vars(LookupVar(fz_ct.arguments[0]));
609 if (fz_ct.arguments[1].type == fz::Argument::INT_LIST) {
611 fz_ct.arguments[1].values.begin(),
612 fz_ct.arguments[1].values.end()}),
614 }
else if (fz_ct.arguments[1].type == fz::Argument::INT_INTERVAL) {
616 Domain(fz_ct.arguments[1].values[0], fz_ct.arguments[1].values[1]),
619 LOG(FATAL) <<
"Wrong format";
621 }
else if (fz_ct.type ==
"set_in_negated") {
622 auto* arg = ct->mutable_linear();
623 arg->add_vars(LookupVar(fz_ct.arguments[0]));
625 if (fz_ct.arguments[1].type == fz::Argument::INT_LIST) {
628 std::vector<int64_t>{fz_ct.arguments[1].values.begin(),
629 fz_ct.arguments[1].values.end()})
632 }
else if (fz_ct.arguments[1].type == fz::Argument::INT_INTERVAL) {
634 Domain(fz_ct.arguments[1].values[0], fz_ct.arguments[1].values[1])
638 LOG(FATAL) <<
"Wrong format";
640 }
else if (fz_ct.type ==
"int_min") {
641 auto* arg = ct->mutable_lin_max();
642 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0],
true);
643 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1],
true);
644 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2],
true);
645 }
else if (fz_ct.type ==
"array_int_minimum" || fz_ct.type ==
"minimum_int") {
646 auto* arg = ct->mutable_lin_max();
647 *arg->mutable_target() = LookupExpr(fz_ct.arguments[0],
true);
648 for (
int i = 0;
i < fz_ct.arguments[1].Size(); ++
i) {
649 *arg->add_exprs() = LookupExprAt(fz_ct.arguments[1], i,
true);
651 }
else if (fz_ct.type ==
"int_max") {
652 auto* arg = ct->mutable_lin_max();
653 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
654 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
655 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
656 }
else if (fz_ct.type ==
"array_int_maximum" || fz_ct.type ==
"maximum_int") {
657 auto* arg = ct->mutable_lin_max();
658 *arg->mutable_target() = LookupExpr(fz_ct.arguments[0]);
659 for (
int i = 0;
i < fz_ct.arguments[1].Size(); ++
i) {
660 *arg->add_exprs() = LookupExprAt(fz_ct.arguments[1], i);
662 }
else if (fz_ct.type ==
"int_times") {
663 auto* arg = ct->mutable_int_prod();
664 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
665 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
666 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
667 }
else if (fz_ct.type ==
"int_abs") {
668 auto* arg = ct->mutable_lin_max();
669 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
670 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0],
true);
671 *arg->mutable_target() = LookupExpr(fz_ct.arguments[1]);
672 }
else if (fz_ct.type ==
"int_plus") {
673 auto* arg = ct->mutable_linear();
675 arg->add_vars(LookupVar(fz_ct.arguments[0]));
677 arg->add_vars(LookupVar(fz_ct.arguments[1]));
679 arg->add_vars(LookupVar(fz_ct.arguments[2]));
681 }
else if (fz_ct.type ==
"int_div") {
682 auto* arg = ct->mutable_int_div();
683 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
684 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
685 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
686 }
else if (fz_ct.type ==
"int_mod") {
687 auto* arg = ct->mutable_int_mod();
688 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
689 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
690 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
691 }
else if (fz_ct.type ==
"array_int_element" ||
692 fz_ct.type ==
"array_bool_element" ||
693 fz_ct.type ==
"array_var_int_element" ||
694 fz_ct.type ==
"array_var_bool_element" ||
695 fz_ct.type ==
"array_int_element_nonshifted") {
696 auto* arg = ct->mutable_element();
697 *arg->mutable_linear_index() = LookupExpr(fz_ct.arguments[0]);
698 if (!absl::EndsWith(fz_ct.type,
"_nonshifted")) {
699 arg->mutable_linear_index()->set_offset(arg->linear_index().offset() - 1);
701 *arg->mutable_linear_target() = LookupExpr(fz_ct.arguments[2]);
703 for (
const VarOrValue elem : LookupVarsOrValues(fz_ct.arguments[1])) {
704 auto* elem_proto = ct->mutable_element()->add_exprs();
705 if (elem.var != kNoVar) {
706 elem_proto->add_vars(elem.var);
707 elem_proto->add_coeffs(1);
709 elem_proto->set_offset(elem.value);
712 }
else if (fz_ct.type ==
"ortools_array_int_element" ||
713 fz_ct.type ==
"ortools_array_bool_element" ||
714 fz_ct.type ==
"ortools_array_var_int_element" ||
715 fz_ct.type ==
"ortools_array_var_bool_element") {
716 auto* arg = ct->mutable_element();
719 *arg->mutable_linear_index() = LookupExpr(fz_ct.arguments[0]);
720 const int64_t index_min = fz_ct.arguments[1].values[0];
721 arg->mutable_linear_index()->set_offset(arg->linear_index().offset() -
725 *arg->mutable_linear_target() = LookupExpr(fz_ct.arguments[3]);
728 for (
const VarOrValue elem : LookupVarsOrValues(fz_ct.arguments[2])) {
729 auto* elem_proto = ct->mutable_element()->add_exprs();
730 if (elem.var != kNoVar) {
731 elem_proto->add_vars(elem.var);
732 elem_proto->add_coeffs(1);
734 elem_proto->set_offset(elem.value);
737 }
else if (fz_ct.type ==
"ortools_table_int") {
738 auto* arg = ct->mutable_table();
739 for (
const VarOrValue v : LookupVarsOrValues(fz_ct.arguments[0])) {
740 LinearExpressionProto* expr = arg->add_exprs();
741 if (v.var != kNoVar) {
742 expr->add_vars(v.var);
745 expr->set_offset(v.value);
748 for (
const int64_t value : fz_ct.arguments[1].values)
749 arg->add_values(value);
750 }
else if (fz_ct.type ==
"ortools_regular") {
751 auto* arg = ct->mutable_automaton();
752 for (
const VarOrValue v : LookupVarsOrValues(fz_ct.arguments[0])) {
753 LinearExpressionProto* expr = arg->add_exprs();
754 if (v.var != kNoVar) {
755 expr->add_vars(v.var);
758 expr->set_offset(v.value);
763 const int num_states = fz_ct.arguments[1].Value();
764 const int num_values = fz_ct.arguments[2].Value();
765 for (
int i = 1;
i <= num_states; ++
i) {
766 for (
int j = 1; j <= num_values; ++j) {
767 CHECK_LT(count, fz_ct.arguments[3].values.size());
768 const int next = fz_ct.arguments[3].values[count++];
769 if (next == 0)
continue;
770 arg->add_transition_tail(i);
771 arg->add_transition_label(j);
772 arg->add_transition_head(next);
776 arg->set_starting_state(fz_ct.arguments[4].Value());
777 switch (fz_ct.arguments[5].type) {
778 case fz::Argument::INT_VALUE: {
779 arg->add_final_states(fz_ct.arguments[5].values[0]);
782 case fz::Argument::INT_INTERVAL: {
783 for (
int v = fz_ct.arguments[5].values[0];
784 v <= fz_ct.arguments[5].values[1]; ++v) {
785 arg->add_final_states(v);
789 case fz::Argument::INT_LIST: {
790 for (
const int v : fz_ct.arguments[5].values) {
791 arg->add_final_states(v);
796 LOG(FATAL) <<
"Wrong constraint " << fz_ct.DebugString();
799 }
else if (fz_ct.type ==
"fzn_all_different_int") {
800 auto* arg = ct->mutable_all_diff();
801 for (
int i = 0;
i < fz_ct.arguments[0].Size(); ++
i) {
802 *arg->add_exprs() = LookupExprAt(fz_ct.arguments[0], i);
804 }
else if (fz_ct.type ==
"ortools_circuit" ||
805 fz_ct.type ==
"ortools_subcircuit") {
806 const int64_t min_index = fz_ct.arguments[1].Value();
807 const int size = std::max(fz_ct.arguments[0].values.size(),
808 fz_ct.arguments[0].variables.size());
810 const int64_t max_index = min_index + size - 1;
812 auto* circuit_arg = ct->mutable_circuit();
816 int64_t index = min_index;
817 const bool is_circuit = (fz_ct.type ==
"ortools_circuit");
818 for (
const int var : LookupVars(fz_ct.arguments[0])) {
822 domain = domain.IntersectionWith(Domain(min_index, max_index));
825 domain = domain.IntersectionWith(Domain::FromIntervals(
826 {{std::numeric_limits<int64_t>::min(), index - 1},
827 {index + 1, std::numeric_limits<int64_t>::max()}}));
831 for (
const ClosedInterval interval : domain) {
832 for (int64_t value = interval.start; value <= interval.end; ++value) {
834 const int literal = proto.variables_size();
836 auto* new_var = proto.add_variables();
837 new_var->add_domain(0);
838 new_var->add_domain(1);
842 circuit_arg->add_tails(index);
843 circuit_arg->add_heads(value);
844 circuit_arg->add_literals(literal);
848 auto* lin = AddEnforcedConstraint(literal)->mutable_linear();
851 lin->add_domain(value);
852 lin->add_domain(value);
858 AddEnforcedConstraint(
NegatedRef(literal))->mutable_linear();
861 lin->add_domain(std::numeric_limits<int64_t>::min());
862 lin->add_domain(value - 1);
863 lin->add_domain(value + 1);
864 lin->add_domain(std::numeric_limits<int64_t>::max());
871 }
else if (fz_ct.type ==
"ortools_inverse") {
872 auto* arg = ct->mutable_inverse();
874 const auto direct_variables = LookupVars(fz_ct.arguments[0]);
875 const auto inverse_variables = LookupVars(fz_ct.arguments[1]);
876 const int base_direct = fz_ct.arguments[2].Value();
877 const int base_inverse = fz_ct.arguments[3].Value();
879 CHECK_EQ(direct_variables.size(), inverse_variables.size());
880 const int num_variables = direct_variables.size();
881 const int end_direct = base_direct + num_variables;
882 const int end_inverse = base_inverse + num_variables;
904 const int arity = std::max(base_inverse, base_direct) + num_variables;
905 for (
int i = 0;
i < arity; ++
i) {
907 if (i < base_direct) {
908 if (i < base_inverse) {
909 arg->add_f_direct(LookupConstant(i));
910 }
else if (i >= base_inverse) {
911 arg->add_f_direct(LookupConstant(i + num_variables));
913 }
else if (i >= base_direct && i < end_direct) {
914 arg->add_f_direct(direct_variables[i - base_direct]);
916 arg->add_f_direct(LookupConstant(i - num_variables));
920 if (i < base_inverse) {
921 if (i < base_direct) {
922 arg->add_f_inverse(LookupConstant(i));
923 }
else if (i >= base_direct) {
924 arg->add_f_inverse(LookupConstant(i + num_variables));
926 }
else if (i >= base_inverse && i < end_inverse) {
927 arg->add_f_inverse(inverse_variables[i - base_inverse]);
929 arg->add_f_inverse(LookupConstant(i - num_variables));
932 }
else if (fz_ct.type ==
"fzn_disjunctive") {
933 const std::vector<VarOrValue> starts =
934 LookupVarsOrValues(fz_ct.arguments[0]);
935 const std::vector<VarOrValue> sizes =
936 LookupVarsOrValues(fz_ct.arguments[1]);
938 auto* arg = ct->mutable_cumulative();
939 arg->mutable_capacity()->set_offset(1);
940 for (
int i = 0;
i < starts.size(); ++
i) {
942 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
943 arg->add_demands()->set_offset(1);
945 }
else if (fz_ct.type ==
"fzn_disjunctive_strict") {
946 const std::vector<VarOrValue> starts =
947 LookupVarsOrValues(fz_ct.arguments[0]);
948 const std::vector<VarOrValue> sizes =
949 LookupVarsOrValues(fz_ct.arguments[1]);
951 auto* arg = ct->mutable_no_overlap();
952 for (
int i = 0;
i < starts.size(); ++
i) {
954 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
956 }
else if (fz_ct.type ==
"fzn_cumulative") {
957 const std::vector<VarOrValue> starts =
958 LookupVarsOrValues(fz_ct.arguments[0]);
959 const std::vector<VarOrValue> sizes =
960 LookupVarsOrValues(fz_ct.arguments[1]);
961 const std::vector<VarOrValue> demands =
962 LookupVarsOrValues(fz_ct.arguments[2]);
964 auto* arg = ct->mutable_cumulative();
965 if (fz_ct.arguments[3].HasOneValue()) {
966 arg->mutable_capacity()->set_offset(fz_ct.arguments[3].Value());
968 arg->mutable_capacity()->add_vars(LookupVar(fz_ct.arguments[3]));
969 arg->mutable_capacity()->add_coeffs(1);
971 for (
int i = 0;
i < starts.size(); ++
i) {
974 if (demands[i].var != kNoVar &&
975 proto.variables(demands[i].var).domain().size() == 2 &&
976 proto.variables(demands[i].var).domain(0) == 0 &&
977 proto.variables(demands[i].var).domain(1) == 1 &&
978 fz_ct.arguments[3].HasOneValue() && fz_ct.arguments[3].Value() == 1) {
980 GetOrCreateOptionalInterval(starts[i], sizes[i], demands[i].var));
981 arg->add_demands()->set_offset(1);
984 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
985 LinearExpressionProto* demand = arg->add_demands();
986 if (demands[i].var == kNoVar) {
987 demand->set_offset(demands[i].value);
989 demand->add_vars(demands[i].var);
990 demand->add_coeffs(1);
994 }
else if (fz_ct.type ==
"ortools_cumulative_opt") {
995 const std::vector<int> occurs = LookupVars(fz_ct.arguments[0]);
996 const std::vector<VarOrValue> starts =
997 LookupVarsOrValues(fz_ct.arguments[1]);
998 const std::vector<VarOrValue> durations =
999 LookupVarsOrValues(fz_ct.arguments[2]);
1000 const std::vector<VarOrValue> demands =
1001 LookupVarsOrValues(fz_ct.arguments[3]);
1003 auto* arg = ct->mutable_cumulative();
1004 if (fz_ct.arguments[3].HasOneValue()) {
1005 arg->mutable_capacity()->set_offset(fz_ct.arguments[4].Value());
1007 arg->mutable_capacity()->add_vars(LookupVar(fz_ct.arguments[4]));
1008 arg->mutable_capacity()->add_coeffs(1);
1010 for (
int i = 0;
i < starts.size(); ++
i) {
1012 GetOrCreateOptionalInterval(starts[i], durations[i], occurs[i]));
1013 LinearExpressionProto* demand = arg->add_demands();
1014 if (demands[i].var == kNoVar) {
1015 demand->set_offset(demands[i].value);
1017 demand->add_vars(demands[i].var);
1018 demand->add_coeffs(1);
1021 }
else if (fz_ct.type ==
"ortools_disjunctive_strict_opt") {
1022 const std::vector<int> occurs = LookupVars(fz_ct.arguments[0]);
1023 const std::vector<VarOrValue> starts =
1024 LookupVarsOrValues(fz_ct.arguments[1]);
1025 const std::vector<VarOrValue> durations =
1026 LookupVarsOrValues(fz_ct.arguments[2]);
1028 auto* arg = ct->mutable_no_overlap();
1029 for (
int i = 0;
i < starts.size(); ++
i) {
1031 GetOrCreateOptionalInterval(starts[i], durations[i], occurs[i]));
1033 }
else if (fz_ct.type ==
"fzn_diffn" || fz_ct.type ==
"fzn_diffn_nonstrict") {
1034 const bool is_strict = fz_ct.type ==
"fzn_diffn";
1035 const std::vector<VarOrValue>
x = LookupVarsOrValues(fz_ct.arguments[0]);
1036 const std::vector<VarOrValue> y = LookupVarsOrValues(fz_ct.arguments[1]);
1037 const std::vector<VarOrValue> dx = LookupVarsOrValues(fz_ct.arguments[2]);
1038 const std::vector<VarOrValue> dy = LookupVarsOrValues(fz_ct.arguments[3]);
1039 const std::vector<int> x_intervals =
1040 is_strict ? CreateIntervals(x, dx)
1041 : CreateNonZeroOrOptionalIntervals(
x, dx);
1042 const std::vector<int> y_intervals =
1043 is_strict ? CreateIntervals(y, dy)
1044 : CreateNonZeroOrOptionalIntervals(y, dy);
1045 auto* arg = ct->mutable_no_overlap_2d();
1046 for (
int i = 0;
i <
x.size(); ++
i) {
1047 arg->add_x_intervals(x_intervals[i]);
1048 arg->add_y_intervals(y_intervals[i]);
1050 }
else if (fz_ct.type ==
"ortools_network_flow" ||
1051 fz_ct.type ==
"ortools_network_flow_cost") {
1054 const bool has_cost = fz_ct.type ==
"ortools_network_flow_cost";
1055 const std::vector<int> flow = LookupVars(fz_ct.arguments[3]);
1058 const int num_nodes = fz_ct.arguments[1].values.size();
1059 const int base_node = fz_ct.arguments[2].Value();
1060 std::vector<std::vector<int>> flows_per_node(num_nodes);
1061 std::vector<std::vector<int>> coeffs_per_node(num_nodes);
1063 const int num_arcs = fz_ct.arguments[0].values.size() / 2;
1064 for (
int arc = 0; arc < num_arcs; arc++) {
1065 const int tail = fz_ct.arguments[0].values[2 * arc] - base_node;
1066 const int head = fz_ct.arguments[0].values[2 * arc + 1] - base_node;
1067 if (tail == head)
continue;
1069 flows_per_node[tail].push_back(flow[arc]);
1070 coeffs_per_node[tail].push_back(1);
1071 flows_per_node[head].push_back(flow[arc]);
1072 coeffs_per_node[head].push_back(-1);
1074 for (
int node = 0; node < num_nodes; node++) {
1075 auto* arg = proto.add_constraints()->mutable_linear();
1076 arg->add_domain(fz_ct.arguments[1].values[node]);
1077 arg->add_domain(fz_ct.arguments[1].values[node]);
1078 for (
int i = 0;
i < flows_per_node[node].size(); ++
i) {
1079 arg->add_vars(flows_per_node[node][i]);
1080 arg->add_coeffs(coeffs_per_node[node][i]);
1085 auto* arg = proto.add_constraints()->mutable_linear();
1088 for (
int arc = 0; arc < num_arcs; arc++) {
1089 const int64_t weight = fz_ct.arguments[4].values[arc];
1091 arg->add_vars(flow[arc]);
1092 arg->add_coeffs(weight);
1095 arg->add_vars(LookupVar(fz_ct.arguments[5]));
1096 arg->add_coeffs(-1);
1099 LOG(FATAL) <<
" Not supported " << fz_ct.type;
1103void CpModelProtoWithMapping::FillReifOrImpliedConstraint(
1104 const fz::Constraint& fz_ct, ConstraintProto* ct) {
1106 std::string simplified_type;
1107 if (absl::EndsWith(fz_ct.type,
"_reif")) {
1109 simplified_type = fz_ct.type.substr(0, fz_ct.type.size() - 5);
1110 }
else if (absl::EndsWith(fz_ct.type,
"_imp")) {
1112 simplified_type = fz_ct.type.substr(0, fz_ct.type.size() - 4);
1115 simplified_type = fz_ct.type;
1119 fz::Constraint copy = fz_ct;
1120 copy.type = simplified_type;
1123 FillConstraint(copy, ct);
1126 std::string negated_type;
1129 if (simplified_type ==
"array_bool_or") {
1130 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[1])));
1131 negated_type =
"array_bool_or_negated";
1132 }
else if (simplified_type ==
"array_bool_and") {
1133 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[1])));
1134 negated_type =
"array_bool_and_negated";
1135 }
else if (simplified_type ==
"set_in") {
1136 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1137 negated_type =
"set_in_negated";
1138 }
else if (simplified_type ==
"bool_eq" || simplified_type ==
"int_eq") {
1139 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1140 negated_type =
"int_ne";
1141 }
else if (simplified_type ==
"bool_ne" || simplified_type ==
"int_ne") {
1142 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1143 negated_type =
"int_eq";
1144 }
else if (simplified_type ==
"bool_le" || simplified_type ==
"int_le") {
1145 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1146 negated_type =
"int_gt";
1147 }
else if (simplified_type ==
"bool_lt" || simplified_type ==
"int_lt") {
1148 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1149 negated_type =
"int_ge";
1150 }
else if (simplified_type ==
"bool_ge" || simplified_type ==
"int_ge") {
1151 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1152 negated_type =
"int_lt";
1153 }
else if (simplified_type ==
"bool_gt" || simplified_type ==
"int_gt") {
1154 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1155 negated_type =
"int_le";
1156 }
else if (simplified_type ==
"int_lin_eq") {
1157 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1158 negated_type =
"int_lin_ne";
1159 }
else if (simplified_type ==
"int_lin_ne") {
1160 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1161 negated_type =
"int_lin_eq";
1162 }
else if (simplified_type ==
"int_lin_le") {
1163 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1164 negated_type =
"int_lin_gt";
1165 }
else if (simplified_type ==
"int_lin_ge") {
1166 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1167 negated_type =
"int_lin_lt";
1168 }
else if (simplified_type ==
"int_lin_lt") {
1169 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1170 negated_type =
"int_lin_ge";
1171 }
else if (simplified_type ==
"int_lin_gt") {
1172 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1173 negated_type =
"int_lin_le";
1175 LOG(FATAL) <<
"Unsupported " << simplified_type;
1179 if (absl::EndsWith(fz_ct.type,
"_imp"))
return;
1183 ConstraintProto* negated_ct = proto.add_constraints();
1184 negated_ct->set_name(fz_ct.type +
" (negated)");
1185 negated_ct->add_enforcement_literal(
1186 sat::NegatedRef(ct->enforcement_literal(0)));
1187 copy.type = negated_type;
1188 FillConstraint(copy, negated_ct);
1191void CpModelProtoWithMapping::TranslateSearchAnnotations(
1192 absl::Span<const fz::Annotation> search_annotations, SolverLogger* logger) {
1193 std::vector<fz::Annotation> flat_annotations;
1194 for (
const fz::Annotation& annotation : search_annotations) {
1195 fz::FlattenAnnotations(annotation, &flat_annotations);
1199 absl::flat_hash_set<int> hinted_vars;
1201 for (
const fz::Annotation& annotation : flat_annotations) {
1202 if (annotation.IsFunctionCallWithIdentifier(
"warm_start")) {
1203 CHECK_EQ(2, annotation.annotations.size());
1204 const fz::Annotation& vars = annotation.annotations[0];
1205 const fz::Annotation& values = annotation.annotations[1];
1206 if (vars.type != fz::Annotation::VAR_REF_ARRAY ||
1207 values.type != fz::Annotation::INT_LIST) {
1210 for (
int i = 0;
i < vars.variables.size(); ++
i) {
1211 fz::Variable* fz_var = vars.variables[
i];
1212 const int var = fz_var_to_index.at(fz_var);
1213 const int64_t value = values.values[
i];
1214 if (hinted_vars.insert(var).second) {
1215 proto.mutable_solution_hint()->add_vars(var);
1216 proto.mutable_solution_hint()->add_values(value);
1219 }
else if (annotation.IsFunctionCallWithIdentifier(
"int_search") ||
1220 annotation.IsFunctionCallWithIdentifier(
"bool_search")) {
1221 const std::vector<fz::Annotation>& args = annotation.annotations;
1222 std::vector<fz::Variable*> vars;
1223 args[0].AppendAllVariables(&vars);
1225 DecisionStrategyProto* strategy = proto.add_search_strategy();
1226 for (fz::Variable* v : vars) {
1227 strategy->add_variables(fz_var_to_index.at(v));
1230 const fz::Annotation& choose = args[1];
1231 if (choose.id ==
"input_order") {
1232 strategy->set_variable_selection_strategy(
1233 DecisionStrategyProto::CHOOSE_FIRST);
1234 }
else if (choose.id ==
"first_fail") {
1235 strategy->set_variable_selection_strategy(
1236 DecisionStrategyProto::CHOOSE_MIN_DOMAIN_SIZE);
1237 }
else if (choose.id ==
"anti_first_fail") {
1238 strategy->set_variable_selection_strategy(
1239 DecisionStrategyProto::CHOOSE_MAX_DOMAIN_SIZE);
1240 }
else if (choose.id ==
"smallest") {
1241 strategy->set_variable_selection_strategy(
1242 DecisionStrategyProto::CHOOSE_LOWEST_MIN);
1243 }
else if (choose.id ==
"largest") {
1244 strategy->set_variable_selection_strategy(
1245 DecisionStrategyProto::CHOOSE_HIGHEST_MAX);
1247 SOLVER_LOG(logger,
"Unsupported variable selection strategy '",
1248 choose.id,
"', falling back to 'smallest'");
1249 strategy->set_variable_selection_strategy(
1250 DecisionStrategyProto::CHOOSE_LOWEST_MIN);
1253 const fz::Annotation& select = args[2];
1254 if (select.id ==
"indomain_min" || select.id ==
"indomain") {
1255 strategy->set_domain_reduction_strategy(
1256 DecisionStrategyProto::SELECT_MIN_VALUE);
1257 }
else if (select.id ==
"indomain_max") {
1258 strategy->set_domain_reduction_strategy(
1259 DecisionStrategyProto::SELECT_MAX_VALUE);
1260 }
else if (select.id ==
"indomain_split") {
1261 strategy->set_domain_reduction_strategy(
1262 DecisionStrategyProto::SELECT_LOWER_HALF);
1263 }
else if (select.id ==
"indomain_reverse_split") {
1264 strategy->set_domain_reduction_strategy(
1265 DecisionStrategyProto::SELECT_UPPER_HALF);
1266 }
else if (select.id ==
"indomain_median") {
1267 strategy->set_domain_reduction_strategy(
1268 DecisionStrategyProto::SELECT_MEDIAN_VALUE);
1270 SOLVER_LOG(logger,
"Unsupported value selection strategy '", select.id,
1271 "', falling back to 'indomain_min'");
1272 strategy->set_domain_reduction_strategy(
1273 DecisionStrategyProto::SELECT_MIN_VALUE);
1280std::string SolutionString(
1281 const fz::SolutionOutputSpecs& output,
1282 const std::function<int64_t(fz::Variable*)>& value_func,
1283 double objective_value) {
1284 if (output.variable !=
nullptr && !output.variable->domain.is_float) {
1285 const int64_t value = value_func(output.variable);
1286 if (output.display_as_boolean) {
1287 return absl::StrCat(output.name,
" = ", value == 1 ?
"true" :
"false",
1290 return absl::StrCat(output.name,
" = ", value,
";");
1292 }
else if (output.variable !=
nullptr && output.variable->domain.is_float) {
1293 return absl::StrCat(output.name,
" = ", objective_value,
";");
1295 const int bound_size = output.bounds.size();
1296 std::string result =
1297 absl::StrCat(output.name,
" = array", bound_size,
"d(");
1298 for (
int i = 0;
i < bound_size; ++
i) {
1299 if (output.bounds[
i].max_value >= output.bounds[
i].min_value) {
1300 absl::StrAppend(&result, output.bounds[
i].min_value,
"..",
1301 output.bounds[
i].max_value,
", ");
1303 result.append(
"{},");
1307 for (
int i = 0;
i < output.flat_variables.size(); ++
i) {
1308 const int64_t value = value_func(output.flat_variables[
i]);
1309 if (output.display_as_boolean) {
1310 result.append(value ?
"true" :
"false");
1312 absl::StrAppend(&result, value);
1314 if (
i != output.flat_variables.size() - 1) {
1315 result.append(
", ");
1318 result.append(
"]);");
1324std::string SolutionString(
1325 const fz::Model& model,
1326 const std::function<int64_t(fz::Variable*)>& value_func,
1327 double objective_value) {
1328 std::string solution_string;
1329 for (
const auto& output_spec : model.output()) {
1330 solution_string.append(
1331 SolutionString(output_spec, value_func, objective_value));
1332 solution_string.append(
"\n");
1334 return solution_string;
1337void OutputFlatzincStats(
const CpSolverResponse& response,
1338 SolverLogger* solution_logger) {
1340 "%%%mzn-stat: objective=", response.objective_value());
1342 "%%%mzn-stat: objectiveBound=", response.best_objective_bound());
1344 "%%%mzn-stat: boolVariables=", response.num_booleans());
1346 "%%%mzn-stat: failures=", response.num_conflicts());
1348 solution_logger,
"%%%mzn-stat: propagations=",
1349 response.num_binary_propagations() + response.num_integer_propagations());
1350 SOLVER_LOG(solution_logger,
"%%%mzn-stat: solveTime=", response.wall_time());
1359 if (!ct->active)
continue;
1360 if (ct->type ==
"int2float") {
1361 ct->type =
"int_eq";
1362 fz::Domain& float_domain = ct->arguments[1].variables[0]->domain;
1364 for (
const double float_value : float_domain.
float_values) {
1365 float_domain.
values.push_back(
static_cast<int64_t
>(float_value));
1375 if (!var->active)
continue;
1376 if (var->domain.is_float) {
1377 CHECK(float_objective_var ==
nullptr);
1378 float_objective_var = var;
1383 if (float_objective_var !=
nullptr) {
1385 if (!ct->active)
continue;
1386 if (ct->type ==
"float_lin_eq") {
1387 CHECK(float_objective_ct ==
nullptr);
1388 float_objective_ct = ct;
1394 if (float_objective_ct !=
nullptr || float_objective_var !=
nullptr) {
1395 CHECK(float_objective_ct !=
nullptr);
1396 CHECK(float_objective_var !=
nullptr);
1397 const int arity = float_objective_ct->
arguments[0].Size();
1398 CHECK_EQ(float_objective_ct->
arguments[1].variables[arity - 1],
1399 float_objective_var);
1400 CHECK_EQ(float_objective_ct->
arguments[0].floats[arity - 1], -1.0);
1401 for (
int i = 0;
i + 1 < arity; ++
i) {
1403 float_objective_ct->
arguments[1].variables[
i],
1407 -float_objective_ct->
arguments[2].floats[0]);
1409 float_objective_var->
active =
false;
1410 float_objective_ct->
active =
false;
1416 const std::string& sat_params,
1419 CpModelProtoWithMapping m;
1420 m.proto.set_name(fz_model.
name());
1425 int num_variables = 0;
1427 if (!fz_var->active)
continue;
1428 CHECK(!fz_var->domain.is_float)
1429 <<
"CP-SAT does not support float variables";
1431 m.fz_var_to_index[fz_var] = num_variables++;
1432 IntegerVariableProto* var = m.proto.add_variables();
1433 var->set_name(fz_var->name);
1434 if (fz_var->domain.is_interval) {
1435 if (fz_var->domain.values.empty()) {
1439 LOG_FIRST_N(WARNING, 1)
1440 <<
"Using flag --fz_int_max for unbounded integer variables.";
1441 LOG_FIRST_N(WARNING, 1)
1442 <<
" actual domain is [" << -absl::GetFlag(FLAGS_fz_int_max)
1443 <<
".." << absl::GetFlag(FLAGS_fz_int_max) <<
"]";
1444 var->add_domain(-absl::GetFlag(FLAGS_fz_int_max));
1445 var->add_domain(absl::GetFlag(FLAGS_fz_int_max));
1447 var->add_domain(fz_var->domain.values[0]);
1448 var->add_domain(fz_var->domain.values[1]);
1457 if (fz_ct ==
nullptr || !fz_ct->active)
continue;
1458 ConstraintProto* ct = m.proto.add_constraints();
1459 ct->set_name(fz_ct->type);
1460 if (absl::EndsWith(fz_ct->type,
"_reif") ||
1461 absl::EndsWith(fz_ct->type,
"_imp") || fz_ct->type ==
"array_bool_or" ||
1462 fz_ct->type ==
"array_bool_and") {
1463 m.FillReifOrImpliedConstraint(*fz_ct, ct);
1465 m.FillConstraint(*fz_ct, ct);
1471 CpObjectiveProto* objective = m.proto.mutable_objective();
1473 objective->set_scaling_factor(-1);
1474 objective->add_coeffs(-1);
1475 objective->add_vars(m.fz_var_to_index[fz_model.
objective()]);
1477 objective->add_coeffs(1);
1478 objective->add_vars(m.fz_var_to_index[fz_model.
objective()]);
1481 FloatObjectiveProto* objective = m.proto.mutable_floating_point_objective();
1483 objective->add_vars(
1488 objective->set_maximize(fz_model.
maximize());
1496 m.parameters.set_enumerate_all_solutions(
true);
1503 m.parameters.set_max_domain_size_when_encoding_eq_neq_constraints(32);
1506 int num_workers = 1;
1513 "Search for all solutions of a SAT problem in parallel is not "
1514 "supported. Switching back to sequential search.");
1522 "The number of search workers, is not specified. For better "
1523 "performances, please set the number of workers to 8, 16, or "
1524 "more depending on the number of cores of your computer.");
1531 m.parameters.set_search_branching(SatParameters::FIXED_SEARCH);
1532 m.parameters.set_keep_all_feasible_solutions_in_presolve(
true);
1534 m.parameters.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
1536 m.parameters.set_interleave_search(
true);
1538 m.parameters.add_subsolvers(
"default_lp");
1539 m.parameters.add_subsolvers(
1540 m.proto.search_strategy().empty() ?
"quick_restart" :
"fixed");
1541 m.parameters.add_subsolvers(
"core_or_no_lp"),
1542 m.parameters.add_subsolvers(
"max_lp");
1545 m.parameters.add_subsolvers(
"default_lp");
1546 m.parameters.add_subsolvers(
1547 m.proto.search_strategy().empty() ?
"probing" :
"fixed");
1548 m.parameters.add_subsolvers(
"no_lp");
1549 m.parameters.add_subsolvers(
"max_lp");
1550 m.parameters.add_subsolvers(
"quick_restart");
1553 }
else if (num_workers > 1 && num_workers < 8 && p.
ortools_mode) {
1554 SOLVER_LOG(logger,
"Bumping number of workers from ", num_workers,
" to 8");
1557 m.parameters.set_num_workers(num_workers);
1566 sat::SatParameters flag_parameters;
1567 CHECK(google::protobuf::TextFormat::ParseFromString(sat_params,
1570 m.parameters.MergeFrom(flag_parameters);
1574 std::function<void(
const CpSolverResponse&)> solution_observer =
nullptr;
1576 solution_observer = [&fz_model, &m, &p,
1577 solution_logger](
const CpSolverResponse& r) {
1578 const std::string solution_string = SolutionString(
1581 return r.solution(m.fz_var_to_index.at(v));
1583 r.objective_value());
1584 SOLVER_LOG(solution_logger, solution_string);
1585 if (p.display_statistics) {
1586 OutputFlatzincStats(r, solution_logger);
1600 if (solution_observer !=
nullptr) {
1604 const CpSolverResponse response =
SolveCpModel(m.proto, &sat_model);
1607 if (response.status() == CpSolverStatus::FEASIBLE ||
1608 response.status() == CpSolverStatus::OPTIMAL) {
1609 CHECK(CheckSolution(
1612 return response.solution(m.fz_var_to_index.at(v));
1619 if (response.status() == CpSolverStatus::FEASIBLE ||
1620 response.status() == CpSolverStatus::OPTIMAL) {
1623 const std::string solution_string = SolutionString(
1626 return response.solution(m.fz_var_to_index.at(v));
1628 response.objective_value());
1629 SOLVER_LOG(solution_logger, solution_string);
1632 if (response.status() == CpSolverStatus::OPTIMAL) {
1635 }
else if (response.status() == CpSolverStatus::INFEASIBLE) {
1636 SOLVER_LOG(solution_logger,
"=====UNSATISFIABLE=====");
1637 }
else if (response.status() == CpSolverStatus::MODEL_INVALID) {
1639 VLOG(1) <<
"%% Error message = '" << error_message <<
"'";
1640 if (absl::StrContains(error_message,
"overflow")) {
1641 SOLVER_LOG(solution_logger,
"=====OVERFLOW=====");
1643 SOLVER_LOG(solution_logger,
"=====MODEL INVALID=====");
1649 OutputFlatzincStats(response, solution_logger);
static Domain FromValues(std::vector< int64_t > values)
Domain AdditionWith(const Domain &domain) const
const std::vector< double > & float_objective_coefficients() const
void AddFloatingPointObjectiveTerm(Variable *var, double coeff)
const std::vector< Variable * > & float_objective_variables() const
const std::vector< Constraint * > & constraints() const
void SetFloatingPointObjectiveOffset(double offset)
const std::vector< Variable * > & variables() const
--— Accessors and mutators --—
double float_objective_offset() const
const std::string & name() const
const std::vector< Annotation > & search_annotations() const
Variable * objective() const
T Add(std::function< T(Model *)> f)
void Register(T *non_owned_class)
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::function< SatParameters(Model *)> NewSatParameters(const std::string ¶ms)
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.
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.
int64_t Min() const
Returns the min of the domain.
std::vector< Argument > arguments
std::vector< int64_t > values
These should never be modified from outside the class.
bool is_float
Float domain.
std::vector< double > float_values
bool search_all_solutions
double max_time_in_seconds
bool display_all_solutions
#define SOLVER_LOG(logger,...)