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