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