OR-Tools  8.2
boolean_problem.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 <algorithm>
17 #include <cstdlib>
18 #include <limits>
19 #include <numeric>
20 #include <utility>
21 
22 #include "absl/container/flat_hash_map.h"
23 #include "absl/status/status.h"
24 #include "absl/strings/str_format.h"
27 #include "ortools/base/logging.h"
28 #if !defined(__PORTABLE_PLATFORM__)
29 #include "ortools/graph/io.h"
30 #endif // __PORTABLE_PLATFORM__
32 #include "ortools/base/hash.h"
33 #include "ortools/base/int_type.h"
34 #include "ortools/base/map_util.h"
36 #include "ortools/graph/util.h"
38 #include "ortools/sat/sat_parameters.pb.h"
39 
40 ABSL_FLAG(std::string, debug_dump_symmetry_graph_to_file, "",
41  "If this flag is non-empty, an undirected graph whose"
42  " automorphism group is in one-to-one correspondence with the"
43  " symmetries of the SAT problem will be dumped to a file every"
44  " time FindLinearBooleanProblemSymmetries() is called.");
45 
46 namespace operations_research {
47 namespace sat {
48 
49 using util::RemapGraph;
50 
51 void ExtractAssignment(const LinearBooleanProblem& problem,
52  const SatSolver& solver, std::vector<bool>* assignment) {
53  assignment->clear();
54  for (int i = 0; i < problem.num_variables(); ++i) {
55  assignment->push_back(
56  solver.Assignment().LiteralIsTrue(Literal(BooleanVariable(i), true)));
57  }
58 }
59 
60 namespace {
61 
62 // Used by BooleanProblemIsValid() to test that there is no duplicate literals,
63 // that they are all within range and that there is no zero coefficient.
64 //
65 // A non-empty string indicates an error.
66 template <typename LinearTerms>
67 std::string ValidateLinearTerms(const LinearTerms& terms,
68  std::vector<bool>* variable_seen) {
69  // variable_seen already has all items false and is reset before return.
70  std::string err_str;
71  int num_errs = 0;
72  const int max_num_errs = 100;
73  for (int i = 0; i < terms.literals_size(); ++i) {
74  if (terms.literals(i) == 0) {
75  if (++num_errs <= max_num_errs) {
76  err_str += absl::StrFormat("Zero literal at position %d\n", i);
77  }
78  }
79  if (terms.coefficients(i) == 0) {
80  if (++num_errs <= max_num_errs) {
81  err_str += absl::StrFormat("Literal %d has a zero coefficient\n",
82  terms.literals(i));
83  }
84  }
85  const int var = Literal(terms.literals(i)).Variable().value();
86  if (var >= variable_seen->size()) {
87  if (++num_errs <= max_num_errs) {
88  err_str += absl::StrFormat("Out of bound variable %d\n", var);
89  }
90  }
91  if ((*variable_seen)[var]) {
92  if (++num_errs <= max_num_errs) {
93  err_str += absl::StrFormat("Duplicated variable %d\n", var);
94  }
95  }
96  (*variable_seen)[var] = true;
97  }
98 
99  for (int i = 0; i < terms.literals_size(); ++i) {
100  const int var = Literal(terms.literals(i)).Variable().value();
101  (*variable_seen)[var] = false;
102  }
103  if (num_errs) {
104  if (num_errs <= max_num_errs) {
105  err_str = absl::StrFormat("%d validation errors:\n", num_errs) + err_str;
106  } else {
107  err_str =
108  absl::StrFormat("%d validation errors; here are the first %d:\n",
109  num_errs, max_num_errs) +
110  err_str;
111  }
112  }
113  return err_str;
114 }
115 
116 // Converts a linear expression from the protocol buffer format to a vector
117 // of LiteralWithCoeff.
118 template <typename ProtoFormat>
119 std::vector<LiteralWithCoeff> ConvertLinearExpression(
120  const ProtoFormat& input) {
121  std::vector<LiteralWithCoeff> cst;
122  cst.reserve(input.literals_size());
123  for (int i = 0; i < input.literals_size(); ++i) {
124  const Literal literal(input.literals(i));
125  cst.push_back(LiteralWithCoeff(literal, input.coefficients(i)));
126  }
127  return cst;
128 }
129 
130 } // namespace
131 
132 absl::Status ValidateBooleanProblem(const LinearBooleanProblem& problem) {
133  std::vector<bool> variable_seen(problem.num_variables(), false);
134  for (int i = 0; i < problem.constraints_size(); ++i) {
135  const LinearBooleanConstraint& constraint = problem.constraints(i);
136  const std::string error = ValidateLinearTerms(constraint, &variable_seen);
137  if (!error.empty()) {
138  return absl::Status(
139  absl::StatusCode::kInvalidArgument,
140  absl::StrFormat("Invalid constraint %i: ", i) + error);
141  }
142  }
143  const std::string error =
144  ValidateLinearTerms(problem.objective(), &variable_seen);
145  if (!error.empty()) {
146  return absl::Status(absl::StatusCode::kInvalidArgument,
147  absl::StrFormat("Invalid objective: ") + error);
148  }
149  return ::absl::OkStatus();
150 }
151 
152 CpModelProto BooleanProblemToCpModelproto(const LinearBooleanProblem& problem) {
153  CpModelProto result;
154  for (int i = 0; i < problem.num_variables(); ++i) {
155  IntegerVariableProto* var = result.add_variables();
156  if (problem.var_names_size() > i) {
157  var->set_name(problem.var_names(i));
158  }
159  var->add_domain(0);
160  var->add_domain(1);
161  }
162  for (const LinearBooleanConstraint& constraint : problem.constraints()) {
163  ConstraintProto* ct = result.add_constraints();
164  ct->set_name(constraint.name());
165  LinearConstraintProto* linear = ct->mutable_linear();
166  int64 offset = 0;
167  for (int i = 0; i < constraint.literals_size(); ++i) {
168  // Note that the new format is slightly different.
169  const int lit = constraint.literals(i);
170  const int64 coeff = constraint.coefficients(i);
171  if (lit > 0) {
172  linear->add_vars(lit - 1);
173  linear->add_coeffs(coeff);
174  } else {
175  // The term was coeff * (1 - var).
176  linear->add_vars(-lit - 1);
177  linear->add_coeffs(-coeff);
178  offset -= coeff;
179  }
180  }
181  linear->add_domain(constraint.has_lower_bound()
182  ? constraint.lower_bound() + offset
183  : kint32min + offset);
184  linear->add_domain(constraint.has_upper_bound()
185  ? constraint.upper_bound() + offset
186  : kint32max + offset);
187  }
188  if (problem.has_objective()) {
189  CpObjectiveProto* objective = result.mutable_objective();
190  int64 offset = 0;
191  for (int i = 0; i < problem.objective().literals_size(); ++i) {
192  const int lit = problem.objective().literals(i);
193  const int64 coeff = problem.objective().coefficients(i);
194  if (lit > 0) {
195  objective->add_vars(lit - 1);
196  objective->add_coeffs(coeff);
197  } else {
198  objective->add_vars(-lit - 1);
199  objective->add_coeffs(-coeff);
200  offset -= coeff;
201  }
202  }
203  objective->set_offset(offset + problem.objective().offset());
204  objective->set_scaling_factor(problem.objective().scaling_factor());
205  }
206  return result;
207 }
208 
209 void ChangeOptimizationDirection(LinearBooleanProblem* problem) {
210  LinearObjective* objective = problem->mutable_objective();
211  objective->set_scaling_factor(-objective->scaling_factor());
212  objective->set_offset(-objective->offset());
213  // We need 'auto' here to keep the open-source compilation happy
214  // (it uses the public protobuf release).
215  for (auto& coefficients_ref : *objective->mutable_coefficients()) {
216  coefficients_ref = -coefficients_ref;
217  }
218 }
219 
220 bool LoadBooleanProblem(const LinearBooleanProblem& problem,
221  SatSolver* solver) {
222  // TODO(user): Currently, the sat solver can load without any issue
223  // constraints with duplicate variables, so we just output a warning if the
224  // problem is not "valid". Make this a strong check once we have some
225  // preprocessing step to remove duplicates variable in the constraints.
226  const absl::Status status = ValidateBooleanProblem(problem);
227  if (!status.ok()) {
228  LOG(WARNING) << "The given problem is invalid!";
229  }
230 
231  if (solver->parameters().log_search_progress()) {
232  LOG(INFO) << "Loading problem '" << problem.name() << "', "
233  << problem.num_variables() << " variables, "
234  << problem.constraints_size() << " constraints.";
235  }
236  solver->SetNumVariables(problem.num_variables());
237  std::vector<LiteralWithCoeff> cst;
238  int64 num_terms = 0;
239  int num_constraints = 0;
240  for (const LinearBooleanConstraint& constraint : problem.constraints()) {
241  num_terms += constraint.literals_size();
242  cst = ConvertLinearExpression(constraint);
243  if (!solver->AddLinearConstraint(
244  constraint.has_lower_bound(), Coefficient(constraint.lower_bound()),
245  constraint.has_upper_bound(), Coefficient(constraint.upper_bound()),
246  &cst)) {
247  LOG(INFO) << "Problem detected to be UNSAT when "
248  << "adding the constraint #" << num_constraints
249  << " with name '" << constraint.name() << "'";
250  return false;
251  }
252  ++num_constraints;
253  }
254  if (solver->parameters().log_search_progress()) {
255  LOG(INFO) << "The problem contains " << num_terms << " terms.";
256  }
257  return true;
258 }
259 
260 bool LoadAndConsumeBooleanProblem(LinearBooleanProblem* problem,
261  SatSolver* solver) {
262  const absl::Status status = ValidateBooleanProblem(*problem);
263  if (!status.ok()) {
264  LOG(WARNING) << "The given problem is invalid! " << status.message();
265  }
266  if (solver->parameters().log_search_progress()) {
267 #if !defined(__PORTABLE_PLATFORM__)
268  LOG(INFO) << "LinearBooleanProblem memory: " << problem->SpaceUsedLong();
269 #endif
270  LOG(INFO) << "Loading problem '" << problem->name() << "', "
271  << problem->num_variables() << " variables, "
272  << problem->constraints_size() << " constraints.";
273  }
274  solver->SetNumVariables(problem->num_variables());
275  std::vector<LiteralWithCoeff> cst;
276  int64 num_terms = 0;
277  int num_constraints = 0;
278 
279  // We will process the constraints backward so we can free the memory used by
280  // each constraint just after processing it. Because of that, we initially
281  // reverse all the constraints to add them in the same order.
282  std::reverse(problem->mutable_constraints()->begin(),
283  problem->mutable_constraints()->end());
284  for (int i = problem->constraints_size() - 1; i >= 0; --i) {
285  const LinearBooleanConstraint& constraint = problem->constraints(i);
286  num_terms += constraint.literals_size();
287  cst = ConvertLinearExpression(constraint);
288  if (!solver->AddLinearConstraint(
289  constraint.has_lower_bound(), Coefficient(constraint.lower_bound()),
290  constraint.has_upper_bound(), Coefficient(constraint.upper_bound()),
291  &cst)) {
292  LOG(INFO) << "Problem detected to be UNSAT when "
293  << "adding the constraint #" << num_constraints
294  << " with name '" << constraint.name() << "'";
295  return false;
296  }
297  delete problem->mutable_constraints()->ReleaseLast();
298  ++num_constraints;
299  }
300  LinearBooleanProblem empty_problem;
301  problem->mutable_constraints()->Swap(empty_problem.mutable_constraints());
302  if (solver->parameters().log_search_progress()) {
303  LOG(INFO) << "The problem contains " << num_terms << " terms.";
304  }
305  return true;
306 }
307 
308 void UseObjectiveForSatAssignmentPreference(const LinearBooleanProblem& problem,
309  SatSolver* solver) {
310  const LinearObjective& objective = problem.objective();
311  CHECK_EQ(objective.literals_size(), objective.coefficients_size());
312  int64 max_abs_weight = 0;
313  for (const int64 coefficient : objective.coefficients()) {
314  max_abs_weight = std::max(max_abs_weight, std::abs(coefficient));
315  }
316  const double max_abs_weight_double = max_abs_weight;
317  for (int i = 0; i < objective.literals_size(); ++i) {
318  const Literal literal(objective.literals(i));
319  const int64 coefficient = objective.coefficients(i);
320  const double abs_weight = std::abs(coefficient) / max_abs_weight_double;
321  // Because this is a minimization problem, we prefer to assign a Boolean
322  // variable to its "low" objective value. So if a literal has a positive
323  // weight when true, we want to set it to false.
324  solver->SetAssignmentPreference(
325  coefficient > 0 ? literal.Negated() : literal, abs_weight);
326  }
327 }
328 
329 bool AddObjectiveUpperBound(const LinearBooleanProblem& problem,
330  Coefficient upper_bound, SatSolver* solver) {
331  std::vector<LiteralWithCoeff> cst =
332  ConvertLinearExpression(problem.objective());
333  return solver->AddLinearConstraint(false, Coefficient(0), true, upper_bound,
334  &cst);
335 }
336 
337 bool AddObjectiveConstraint(const LinearBooleanProblem& problem,
338  bool use_lower_bound, Coefficient lower_bound,
339  bool use_upper_bound, Coefficient upper_bound,
340  SatSolver* solver) {
341  std::vector<LiteralWithCoeff> cst =
342  ConvertLinearExpression(problem.objective());
343  return solver->AddLinearConstraint(use_lower_bound, lower_bound,
344  use_upper_bound, upper_bound, &cst);
345 }
346 
347 Coefficient ComputeObjectiveValue(const LinearBooleanProblem& problem,
348  const std::vector<bool>& assignment) {
349  CHECK_EQ(assignment.size(), problem.num_variables());
350  Coefficient sum(0);
351  const LinearObjective& objective = problem.objective();
352  for (int i = 0; i < objective.literals_size(); ++i) {
353  const Literal literal(objective.literals(i));
354  if (assignment[literal.Variable().value()] == literal.IsPositive()) {
355  sum += objective.coefficients(i);
356  }
357  }
358  return sum;
359 }
360 
361 bool IsAssignmentValid(const LinearBooleanProblem& problem,
362  const std::vector<bool>& assignment) {
363  CHECK_EQ(assignment.size(), problem.num_variables());
364 
365  // Check that all constraints are satisfied.
366  for (const LinearBooleanConstraint& constraint : problem.constraints()) {
367  Coefficient sum(0);
368  for (int i = 0; i < constraint.literals_size(); ++i) {
369  const Literal literal(constraint.literals(i));
370  if (assignment[literal.Variable().value()] == literal.IsPositive()) {
371  sum += constraint.coefficients(i);
372  }
373  }
374  if (constraint.has_lower_bound() && sum < constraint.lower_bound()) {
375  LOG(WARNING) << "Unsatisfied constraint! sum: " << sum << "\n"
376  << ProtobufDebugString(constraint);
377  return false;
378  }
379  if (constraint.has_upper_bound() && sum > constraint.upper_bound()) {
380  LOG(WARNING) << "Unsatisfied constraint! sum: " << sum << "\n"
381  << ProtobufDebugString(constraint);
382  return false;
383  }
384  }
385  return true;
386 }
387 
388 // Note(user): This function makes a few assumptions about the format of the
389 // given LinearBooleanProblem. All constraint coefficients must be 1 (and of the
390 // form >= 1) and all objective weights must be strictly positive.
392  const LinearBooleanProblem& problem) {
393  std::string output;
394  const bool is_wcnf = (problem.objective().coefficients_size() > 0);
395  const LinearObjective& objective = problem.objective();
396 
397  // Hack: We know that all the variables with index greater than this have been
398  // created "artificially" in order to encode a max-sat problem into our
399  // format. Each extra variable appear only once, and was used as a slack to
400  // reify a soft clause.
401  const int first_slack_variable = problem.original_num_variables();
402 
403  // This will contains the objective.
404  absl::flat_hash_map<int, int64> literal_to_weight;
405  std::vector<std::pair<int, int64>> non_slack_objective;
406 
407  // This will be the weight of the "hard" clauses in the wcnf format. It must
408  // be greater than the sum of the weight of all the soft clauses, so we will
409  // just set it to this sum + 1.
410  int64 hard_weight = 1;
411  if (is_wcnf) {
412  int i = 0;
413  for (int64 weight : objective.coefficients()) {
414  CHECK_NE(weight, 0);
415  int signed_literal = objective.literals(i);
416 
417  // There is no direct support for an objective offset in the wcnf format.
418  // So this is not a perfect translation of the objective. It is however
419  // possible to achieve the same effect by adding a new variable x, and two
420  // soft clauses: x with weight offset, and -x with weight offset.
421  //
422  // TODO(user): implement this trick.
423  if (weight < 0) {
424  signed_literal = -signed_literal;
425  weight = -weight;
426  }
427  literal_to_weight[objective.literals(i)] = weight;
428  if (Literal(signed_literal).Variable() < first_slack_variable) {
429  non_slack_objective.push_back(std::make_pair(signed_literal, weight));
430  }
431  hard_weight += weight;
432  ++i;
433  }
434  output += absl::StrFormat("p wcnf %d %d %d\n", first_slack_variable,
435  static_cast<int>(problem.constraints_size() +
436  non_slack_objective.size()),
437  hard_weight);
438  } else {
439  output += absl::StrFormat("p cnf %d %d\n", problem.num_variables(),
440  problem.constraints_size());
441  }
442 
443  std::string constraint_output;
444  for (const LinearBooleanConstraint& constraint : problem.constraints()) {
445  if (constraint.literals_size() == 0) return ""; // Assumption.
446  constraint_output.clear();
447  int64 weight = hard_weight;
448  for (int i = 0; i < constraint.literals_size(); ++i) {
449  if (constraint.coefficients(i) != 1) return ""; // Assumption.
450  if (is_wcnf && abs(constraint.literals(i)) - 1 >= first_slack_variable) {
451  weight = literal_to_weight[constraint.literals(i)];
452  } else {
453  if (i > 0) constraint_output += " ";
454  constraint_output += Literal(constraint.literals(i)).DebugString();
455  }
456  }
457  if (is_wcnf) {
458  output += absl::StrFormat("%d ", weight);
459  }
460  output += constraint_output + " 0\n";
461  }
462 
463  // Output the rest of the objective as singleton constraints.
464  if (is_wcnf) {
465  for (std::pair<int, int64> p : non_slack_objective) {
466  // Since it is falsifying this clause that cost "weigtht", we need to take
467  // its negation.
468  const Literal literal(-p.first);
469  output += absl::StrFormat("%d %s 0\n", p.second, literal.DebugString());
470  }
471  }
472 
473  return output;
474 }
475 
476 void StoreAssignment(const VariablesAssignment& assignment,
477  BooleanAssignment* output) {
478  output->clear_literals();
479  for (BooleanVariable var(0); var < assignment.NumberOfVariables(); ++var) {
480  if (assignment.VariableIsAssigned(var)) {
481  output->add_literals(
483  }
484  }
485 }
486 
487 void ExtractSubproblem(const LinearBooleanProblem& problem,
488  const std::vector<int>& constraint_indices,
489  LinearBooleanProblem* subproblem) {
490  *subproblem = problem;
491  subproblem->set_name("Subproblem of " + problem.name());
492  subproblem->clear_constraints();
493  for (int index : constraint_indices) {
494  CHECK_LT(index, problem.constraints_size());
495  subproblem->add_constraints()->MergeFrom(problem.constraints(index));
496  }
497 }
498 
499 namespace {
500 // A simple class to generate equivalence class number for
501 // GenerateGraphForSymmetryDetection().
502 class IdGenerator {
503  public:
504  IdGenerator() {}
505 
506  // If the pair (type, coefficient) was never seen before, then generate
507  // a new id, otherwise return the previously generated id.
508  int GetId(int type, Coefficient coefficient) {
509  const std::pair<int, int64> key(type, coefficient.value());
510  return gtl::LookupOrInsert(&id_map_, key, id_map_.size());
511  }
512 
513  private:
514  absl::flat_hash_map<std::pair<int, int64>, int> id_map_;
515 };
516 } // namespace.
517 
518 // Returns a graph whose automorphisms can be mapped back to the symmetries of
519 // the given LinearBooleanProblem.
520 //
521 // Any permutation of the graph that respects the initial_equivalence_classes
522 // output can be mapped to a symmetry of the given problem simply by taking its
523 // restriction on the first 2 * num_variables nodes and interpreting its index
524 // as a literal index. In a sense, a node with a low enough index #i is in
525 // one-to-one correspondence with a literals #i (using the index representation
526 // of literal).
527 //
528 // The format of the initial_equivalence_classes is the same as the one
529 // described in GraphSymmetryFinder::FindSymmetries(). The classes must be dense
530 // in [0, num_classes) and any symmetry will only map nodes with the same class
531 // between each other.
532 template <typename Graph>
534  const LinearBooleanProblem& problem,
535  std::vector<int>* initial_equivalence_classes) {
536  // First, we convert the problem to its canonical representation.
537  const int num_variables = problem.num_variables();
538  CanonicalBooleanLinearProblem canonical_problem;
539  std::vector<LiteralWithCoeff> cst;
540  for (const LinearBooleanConstraint& constraint : problem.constraints()) {
541  cst = ConvertLinearExpression(constraint);
542  CHECK(canonical_problem.AddLinearConstraint(
543  constraint.has_lower_bound(), Coefficient(constraint.lower_bound()),
544  constraint.has_upper_bound(), Coefficient(constraint.upper_bound()),
545  &cst));
546  }
547 
548  // TODO(user): reserve the memory for the graph? not sure it is worthwhile
549  // since it would require some linear scan of the problem though.
550  Graph* graph = new Graph();
551  initial_equivalence_classes->clear();
552 
553  // We will construct a graph with 3 different types of node that must be
554  // in different equivalent classes.
555  enum NodeType { LITERAL_NODE, CONSTRAINT_NODE, CONSTRAINT_COEFFICIENT_NODE };
556  IdGenerator id_generator;
557 
558  // First, we need one node per literal with an edge between each literal
559  // and its negation.
560  for (int i = 0; i < num_variables; ++i) {
561  // We have two nodes for each variable.
562  // Note that the indices are in [0, 2 * num_variables) and in one to one
563  // correspondence with the index representation of a literal.
564  const Literal literal = Literal(BooleanVariable(i), true);
565  graph->AddArc(literal.Index().value(), literal.NegatedIndex().value());
566  graph->AddArc(literal.NegatedIndex().value(), literal.Index().value());
567  }
568 
569  // We use 0 for their initial equivalence class, but that may be modified
570  // with the objective coefficient (see below).
571  initial_equivalence_classes->assign(
572  2 * num_variables,
573  id_generator.GetId(NodeType::LITERAL_NODE, Coefficient(0)));
574 
575  // Literals with different objective coeffs shouldn't be in the same class.
576  //
577  // We need to canonicalize the objective to regroup literals corresponding
578  // to the same variables. Note that we don't care about the offset or
579  // optimization direction here, we just care about literals with the same
580  // canonical coefficient.
581  Coefficient shift;
582  Coefficient max_value;
583  std::vector<LiteralWithCoeff> expr =
584  ConvertLinearExpression(problem.objective());
585  ComputeBooleanLinearExpressionCanonicalForm(&expr, &shift, &max_value);
586  for (LiteralWithCoeff term : expr) {
587  (*initial_equivalence_classes)[term.literal.Index().value()] =
588  id_generator.GetId(NodeType::LITERAL_NODE, term.coefficient);
589  }
590 
591  // Then, for each constraint, we will have one or more nodes.
592  for (int i = 0; i < canonical_problem.NumConstraints(); ++i) {
593  // First we have a node for the constraint with an equivalence class
594  // depending on the rhs.
595  //
596  // Note: Since we add nodes one by one, initial_equivalence_classes->size()
597  // gives the number of nodes at any point, which we use as next node index.
598  const int constraint_node_index = initial_equivalence_classes->size();
599  initial_equivalence_classes->push_back(id_generator.GetId(
600  NodeType::CONSTRAINT_NODE, canonical_problem.Rhs(i)));
601 
602  // This node will also be connected to all literals of the constraint
603  // with a coefficient of 1. Literals with new coefficients will be grouped
604  // under a new node connected to the constraint_node_index.
605  //
606  // Note that this works because a canonical constraint is sorted by
607  // increasing coefficient value (all positive).
608  int current_node_index = constraint_node_index;
609  Coefficient previous_coefficient(1);
610  for (LiteralWithCoeff term : canonical_problem.Constraint(i)) {
611  if (term.coefficient != previous_coefficient) {
612  current_node_index = initial_equivalence_classes->size();
613  initial_equivalence_classes->push_back(id_generator.GetId(
614  NodeType::CONSTRAINT_COEFFICIENT_NODE, term.coefficient));
615  previous_coefficient = term.coefficient;
616 
617  // Connect this node to the constraint node. Note that we don't
618  // technically need the arcs in both directions, but that may help a bit
619  // the algorithm to find symmetries.
620  graph->AddArc(constraint_node_index, current_node_index);
621  graph->AddArc(current_node_index, constraint_node_index);
622  }
623 
624  // Connect this node to the associated term.literal node. Note that we
625  // don't technically need the arcs in both directions, but that may help a
626  // bit the algorithm to find symmetries.
627  graph->AddArc(current_node_index, term.literal.Index().value());
628  graph->AddArc(term.literal.Index().value(), current_node_index);
629  }
630  }
631  graph->Build();
632  DCHECK_EQ(graph->num_nodes(), initial_equivalence_classes->size());
633  return graph;
634 }
635 
636 void MakeAllLiteralsPositive(LinearBooleanProblem* problem) {
637  // Objective.
638  LinearObjective* mutable_objective = problem->mutable_objective();
639  int64 objective_offset = 0;
640  for (int i = 0; i < mutable_objective->literals_size(); ++i) {
641  const int signed_literal = mutable_objective->literals(i);
642  if (signed_literal < 0) {
643  const int64 coefficient = mutable_objective->coefficients(i);
644  mutable_objective->set_literals(i, -signed_literal);
645  mutable_objective->set_coefficients(i, -coefficient);
646  objective_offset += coefficient;
647  }
648  }
649  mutable_objective->set_offset(mutable_objective->offset() + objective_offset);
650 
651  // Constraints.
652  for (LinearBooleanConstraint& constraint :
653  *(problem->mutable_constraints())) {
654  int64 sum = 0;
655  for (int i = 0; i < constraint.literals_size(); ++i) {
656  if (constraint.literals(i) < 0) {
657  sum += constraint.coefficients(i);
658  constraint.set_literals(i, -constraint.literals(i));
659  constraint.set_coefficients(i, -constraint.coefficients(i));
660  }
661  }
662  if (constraint.has_lower_bound()) {
663  constraint.set_lower_bound(constraint.lower_bound() - sum);
664  }
665  if (constraint.has_upper_bound()) {
666  constraint.set_upper_bound(constraint.upper_bound() - sum);
667  }
668  }
669 }
670 
672  const LinearBooleanProblem& problem,
673  std::vector<std::unique_ptr<SparsePermutation>>* generators) {
675  std::vector<int> equivalence_classes;
676  std::unique_ptr<Graph> graph(
677  GenerateGraphForSymmetryDetection<Graph>(problem, &equivalence_classes));
678  LOG(INFO) << "Graph has " << graph->num_nodes() << " nodes and "
679  << graph->num_arcs() / 2 << " edges.";
680 #if !defined(__PORTABLE_PLATFORM__)
681  if (!absl::GetFlag(FLAGS_debug_dump_symmetry_graph_to_file).empty()) {
682  // Remap the graph nodes to sort them by equivalence classes.
683  std::vector<int> new_node_index(graph->num_nodes(), -1);
684  const int num_classes = 1 + *std::max_element(equivalence_classes.begin(),
685  equivalence_classes.end());
686  std::vector<int> class_size(num_classes, 0);
687  for (const int c : equivalence_classes) ++class_size[c];
688  std::vector<int> next_index_by_class(num_classes, 0);
689  std::partial_sum(class_size.begin(), class_size.end() - 1,
690  next_index_by_class.begin() + 1);
691  for (int node = 0; node < graph->num_nodes(); ++node) {
692  new_node_index[node] = next_index_by_class[equivalence_classes[node]]++;
693  }
694  std::unique_ptr<Graph> remapped_graph = RemapGraph(*graph, new_node_index);
695  const absl::Status status = util::WriteGraphToFile(
696  *remapped_graph, absl::GetFlag(FLAGS_debug_dump_symmetry_graph_to_file),
697  /*directed=*/false, class_size);
698  if (!status.ok()) {
699  LOG(DFATAL) << "Error when writing the symmetry graph to file: "
700  << status;
701  }
702  }
703 #endif // __PORTABLE_PLATFORM__
704  GraphSymmetryFinder symmetry_finder(*graph,
705  /*is_undirected=*/true);
706  std::vector<int> factorized_automorphism_group_size;
707  // TODO(user): inject the appropriate time limit here.
708  CHECK_OK(symmetry_finder.FindSymmetries(&equivalence_classes, generators,
709  &factorized_automorphism_group_size));
710 
711  // Remove from the permutations the part not concerning the literals.
712  // Note that some permutation may becomes empty, which means that we had
713  // duplicates constraints. TODO(user): Remove them beforehand?
714  double average_support_size = 0.0;
715  int num_generators = 0;
716  for (int i = 0; i < generators->size(); ++i) {
717  SparsePermutation* permutation = (*generators)[i].get();
718  std::vector<int> to_delete;
719  for (int j = 0; j < permutation->NumCycles(); ++j) {
720  if (*(permutation->Cycle(j).begin()) >= 2 * problem.num_variables()) {
721  to_delete.push_back(j);
722  if (DEBUG_MODE) {
723  // Verify that the cycle's entire support does not touch any variable.
724  for (const int node : permutation->Cycle(j)) {
725  DCHECK_GE(node, 2 * problem.num_variables());
726  }
727  }
728  }
729  }
730  permutation->RemoveCycles(to_delete);
731  if (!permutation->Support().empty()) {
732  average_support_size += permutation->Support().size();
733  swap((*generators)[num_generators], (*generators)[i]);
734  ++num_generators;
735  }
736  }
737  generators->resize(num_generators);
738  average_support_size /= num_generators;
739  LOG(INFO) << "# of generators: " << num_generators;
740  LOG(INFO) << "Average support size: " << average_support_size;
741 }
742 
745  LinearBooleanProblem* problem) {
746  Coefficient bound_shift;
747  Coefficient max_value;
748  std::vector<LiteralWithCoeff> cst;
749 
750  // First the objective.
751  cst = ConvertLinearExpression(problem->objective());
752  ApplyLiteralMapping(mapping, &cst, &bound_shift, &max_value);
753  LinearObjective* mutable_objective = problem->mutable_objective();
754  mutable_objective->clear_literals();
755  mutable_objective->clear_coefficients();
756  mutable_objective->set_offset(mutable_objective->offset() -
757  bound_shift.value());
758  for (const LiteralWithCoeff& entry : cst) {
759  mutable_objective->add_literals(entry.literal.SignedValue());
760  mutable_objective->add_coefficients(entry.coefficient.value());
761  }
762 
763  // Now the clauses.
764  for (LinearBooleanConstraint& constraint : *problem->mutable_constraints()) {
765  cst = ConvertLinearExpression(constraint);
766  constraint.clear_literals();
767  constraint.clear_coefficients();
768  ApplyLiteralMapping(mapping, &cst, &bound_shift, &max_value);
769 
770  // Add bound_shift to the bounds and remove a bound if it is now trivial.
771  if (constraint.has_upper_bound()) {
772  constraint.set_upper_bound(constraint.upper_bound() +
773  bound_shift.value());
774  if (max_value <= constraint.upper_bound()) {
775  constraint.clear_upper_bound();
776  }
777  }
778  if (constraint.has_lower_bound()) {
779  constraint.set_lower_bound(constraint.lower_bound() +
780  bound_shift.value());
781  // This is because ApplyLiteralMapping make all coefficient positive.
782  if (constraint.lower_bound() <= 0) {
783  constraint.clear_lower_bound();
784  }
785  }
786 
787  // If the constraint is always true, we just leave it empty.
788  if (constraint.has_lower_bound() || constraint.has_upper_bound()) {
789  for (const LiteralWithCoeff& entry : cst) {
790  constraint.add_literals(entry.literal.SignedValue());
791  constraint.add_coefficients(entry.coefficient.value());
792  }
793  }
794  }
795 
796  // Remove empty constraints.
797  int new_index = 0;
798  const int num_constraints = problem->constraints_size();
799  for (int i = 0; i < num_constraints; ++i) {
800  if (!(problem->constraints(i).literals_size() == 0)) {
801  problem->mutable_constraints()->SwapElements(i, new_index);
802  ++new_index;
803  }
804  }
805  problem->mutable_constraints()->DeleteSubrange(new_index,
806  num_constraints - new_index);
807 
808  // Computes the new number of variables and set it.
809  int num_vars = 0;
810  for (LiteralIndex index : mapping) {
811  if (index >= 0) {
812  num_vars = std::max(num_vars, Literal(index).Variable().value() + 1);
813  }
814  }
815  problem->set_num_variables(num_vars);
816 
817  // TODO(user): The names is currently all scrambled. Do something about it
818  // so that non-fixed variables keep their names.
819  problem->mutable_var_names()->DeleteSubrange(
820  num_vars, problem->var_names_size() - num_vars);
821 }
822 
823 // A simple preprocessing step that does basic probing and removes the
824 // equivalent literals.
826  LinearBooleanProblem* problem) {
827  // TODO(user): expose the number of iterations as a parameter.
828  for (int iter = 0; iter < 6; ++iter) {
829  SatSolver solver;
830  if (!LoadBooleanProblem(*problem, &solver)) {
831  LOG(INFO) << "UNSAT when loading the problem.";
832  }
833 
835  ProbeAndFindEquivalentLiteral(&solver, postsolver, /*drat_writer=*/nullptr,
836  &equiv_map);
837 
838  // We can abort if no information is learned.
839  if (equiv_map.empty() && solver.LiteralTrail().Index() == 0) break;
840 
841  if (equiv_map.empty()) {
842  const int num_literals = 2 * solver.NumVariables();
843  for (LiteralIndex index(0); index < num_literals; ++index) {
844  equiv_map.push_back(index);
845  }
846  }
847 
848  // Fix fixed variables in the equivalence map and in the postsolver.
849  solver.Backtrack(0);
850  for (int i = 0; i < solver.LiteralTrail().Index(); ++i) {
851  const Literal l = solver.LiteralTrail()[i];
852  equiv_map[l.Index()] = kTrueLiteralIndex;
853  equiv_map[l.NegatedIndex()] = kFalseLiteralIndex;
854  postsolver->FixVariable(l);
855  }
856 
857  // Remap the variables into a dense set. All the variables for which the
858  // equiv_map is not the identity are no longer needed.
859  BooleanVariable new_var(0);
861  for (BooleanVariable var(0); var < solver.NumVariables(); ++var) {
862  if (equiv_map[Literal(var, true).Index()] == Literal(var, true).Index()) {
863  var_map.push_back(new_var);
864  ++new_var;
865  } else {
866  var_map.push_back(BooleanVariable(-1));
867  }
868  }
869 
870  // Apply the variable mapping.
871  postsolver->ApplyMapping(var_map);
872  for (LiteralIndex index(0); index < equiv_map.size(); ++index) {
873  if (equiv_map[index] >= 0) {
874  const Literal l(equiv_map[index]);
875  const BooleanVariable image = var_map[l.Variable()];
876  CHECK_NE(image, BooleanVariable(-1));
877  equiv_map[index] = Literal(image, l.IsPositive()).Index();
878  }
879  }
880  ApplyLiteralMappingToBooleanProblem(equiv_map, problem);
881  }
882 }
883 
884 } // namespace sat
885 } // namespace operations_research
int64 max
Definition: alldiff_cst.cc:139
#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_OK(x)
Definition: base/logging.h:40
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define LOG(severity)
Definition: base/logging.h:420
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
ABSL_FLAG(std::string, debug_dump_symmetry_graph_to_file, "", "If this flag is non-empty, an undirected graph whose" " automorphism group is in one-to-one correspondence with the" " symmetries of the SAT problem will be dumped to a file every" " time FindLinearBooleanProblemSymmetries() is called.")
size_type size() const
bool empty() const
void push_back(const value_type &x)
absl::Status FindSymmetries(std::vector< int > *node_equivalence_classes_io, std::vector< std::unique_ptr< SparsePermutation > > *generators, std::vector< int > *factorized_automorphism_group_size, TimeLimit *time_limit=nullptr)
void RemoveCycles(const std::vector< int > &cycle_indices)
const std::vector< int > & Support() const
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
const std::vector< LiteralWithCoeff > & Constraint(int i) const
LiteralIndex NegatedIndex() const
Definition: sat_base.h:85
LiteralIndex Index() const
Definition: sat_base.h:84
BooleanVariable Variable() const
Definition: sat_base.h:80
std::string DebugString() const
Definition: sat_base.h:93
void ApplyMapping(const absl::StrongVector< BooleanVariable, BooleanVariable > &mapping)
const Trail & LiteralTrail() const
Definition: sat_solver.h:361
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
Definition: sat_solver.cc:299
void SetNumVariables(int num_variables)
Definition: sat_solver.cc:64
const SatParameters & parameters() const
Definition: sat_solver.cc:110
void SetAssignmentPreference(Literal literal, double weight)
Definition: sat_solver.h:150
const VariablesAssignment & Assignment() const
Definition: sat_solver.h:362
void Backtrack(int target_level)
Definition: sat_solver.cc:888
bool VariableIsAssigned(BooleanVariable var) const
Definition: sat_base.h:158
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
Literal GetTrueLiteralForAssignedVariable(BooleanVariable var) const
Definition: sat_base.h:165
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
int64_t int64
static const int32 kint32max
static const int32 kint32min
const int WARNING
Definition: log_severity.h:31
const int INFO
Definition: log_severity.h:31
const bool DEBUG_MODE
Definition: macros.h:24
Collection::value_type::second_type & LookupOrInsert(Collection *const collection, const typename Collection::value_type::first_type &key, const typename Collection::value_type::second_type &value)
Definition: map_util.h:207
bool AddObjectiveConstraint(const LinearBooleanProblem &problem, bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, SatSolver *solver)
void StoreAssignment(const VariablesAssignment &assignment, BooleanAssignment *output)
Graph * GenerateGraphForSymmetryDetection(const LinearBooleanProblem &problem, std::vector< int > *initial_equivalence_classes)
void UseObjectiveForSatAssignmentPreference(const LinearBooleanProblem &problem, SatSolver *solver)
bool ApplyLiteralMapping(const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping, std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
void ExtractSubproblem(const LinearBooleanProblem &problem, const std::vector< int > &constraint_indices, LinearBooleanProblem *subproblem)
absl::Status ValidateBooleanProblem(const LinearBooleanProblem &problem)
bool AddObjectiveUpperBound(const LinearBooleanProblem &problem, Coefficient upper_bound, SatSolver *solver)
void FindLinearBooleanProblemSymmetries(const LinearBooleanProblem &problem, std::vector< std::unique_ptr< SparsePermutation >> *generators)
const LiteralIndex kTrueLiteralIndex(-2)
bool ComputeBooleanLinearExpressionCanonicalForm(std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
const LiteralIndex kFalseLiteralIndex(-3)
bool LoadAndConsumeBooleanProblem(LinearBooleanProblem *problem, SatSolver *solver)
void ApplyLiteralMappingToBooleanProblem(const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping, LinearBooleanProblem *problem)
bool IsAssignmentValid(const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
void ChangeOptimizationDirection(LinearBooleanProblem *problem)
void ProbeAndSimplifyProblem(SatPostsolver *postsolver, LinearBooleanProblem *problem)
Coefficient ComputeObjectiveValue(const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
void ProbeAndFindEquivalentLiteral(SatSolver *solver, SatPostsolver *postsolver, DratProofHandler *drat_proof_handler, absl::StrongVector< LiteralIndex, LiteralIndex > *mapping)
CpModelProto BooleanProblemToCpModelproto(const LinearBooleanProblem &problem)
void MakeAllLiteralsPositive(LinearBooleanProblem *problem)
bool LoadBooleanProblem(const LinearBooleanProblem &problem, SatSolver *solver)
std::string LinearBooleanProblemToCnfString(const LinearBooleanProblem &problem)
void ExtractAssignment(const LinearBooleanProblem &problem, const SatSolver &solver, std::vector< bool > *assignment)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::string ProtobufDebugString(const P &message)
ListGraph Graph
Definition: graph.h:2360
absl::Status WriteGraphToFile(const Graph &graph, const std::string &filename, bool directed, const std::vector< int > &num_nodes_with_color)
Definition: io.h:225
std::unique_ptr< Graph > RemapGraph(const Graph &graph, const std::vector< int > &new_node_index)
Definition: graph/util.h:275
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
int64 weight
Definition: pack.cc:509
static int input(yyscan_t yyscanner)
int64 coefficient
std::vector< int >::const_iterator begin() const