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