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"
28#if !defined(__PORTABLE_PLATFORM__)
29#include "ortools/graph/io.h"
30#endif // __PORTABLE_PLATFORM__
32#include "ortools/base/hash.h"
36#include "ortools/graph/util.h"
38#include "ortools/sat/sat_parameters.pb.h"
39
40ABSL_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
46namespace operations_research {
47namespace sat {
48
50
51void 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
60namespace {
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.
66template <typename LinearTerms>
67std::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.
118template <typename ProtoFormat>
119std::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
132absl::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
152CpModelProto 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
209void 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
220bool 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
260bool 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
308void 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.
325 coefficient > 0 ? literal.Negated() : literal, abs_weight);
326 }
327}
328
329bool 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
337bool 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
347Coefficient 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
361bool 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
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
487void 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
499namespace {
500// A simple class to generate equivalence class number for
501// GenerateGraphForSymmetryDetection().
502class 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.
532template <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
636void 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)
const std::vector< int > & Support() const
void RemoveCycles(const std::vector< int > &cycle_indices)
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)
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
const VariablesAssignment & Assignment() const
Definition: sat_solver.h:362
const Trail & LiteralTrail() const
Definition: sat_solver.h:361
void SetAssignmentPreference(Literal literal, double weight)
Definition: sat_solver.h:150
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
const LiteralIndex kFalseLiteralIndex(-3)
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)
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)
Graph * GenerateGraphForSymmetryDetection(const LinearBooleanProblem &problem, std::vector< int > *initial_equivalence_classes)
bool ComputeBooleanLinearExpressionCanonicalForm(std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
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)
void FindLinearBooleanProblemSymmetries(const LinearBooleanProblem &problem, std::vector< std::unique_ptr< SparsePermutation > > *generators)
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)
const LiteralIndex kTrueLiteralIndex(-2)
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