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__)
38#include "ortools/sat/sat_parameters.pb.h"
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.");
52 const SatSolver& solver, std::vector<bool>* assignment) {
54 for (
int i = 0; i < problem.num_variables(); ++i) {
55 assignment->push_back(
66template <
typename LinearTerms>
67std::string ValidateLinearTerms(
const LinearTerms& terms,
68 std::vector<bool>* variable_seen) {
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);
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",
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);
91 if ((*variable_seen)[
var]) {
92 if (++num_errs <= max_num_errs) {
93 err_str += absl::StrFormat(
"Duplicated variable %d\n",
var);
96 (*variable_seen)[
var] =
true;
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;
104 if (num_errs <= max_num_errs) {
105 err_str = absl::StrFormat(
"%d validation errors:\n", num_errs) + err_str;
108 absl::StrFormat(
"%d validation errors; here are the first %d:\n",
109 num_errs, max_num_errs) +
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) {
125 cst.push_back(LiteralWithCoeff(
literal,
input.coefficients(i)));
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()) {
139 absl::StatusCode::kInvalidArgument,
140 absl::StrFormat(
"Invalid constraint %i: ", i) + error);
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);
149 return ::absl::OkStatus();
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));
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();
167 for (
int i = 0; i < constraint.literals_size(); ++i) {
169 const int lit = constraint.literals(i);
170 const int64 coeff = constraint.coefficients(i);
172 linear->add_vars(lit - 1);
173 linear->add_coeffs(coeff);
176 linear->add_vars(-lit - 1);
177 linear->add_coeffs(-coeff);
181 linear->add_domain(constraint.has_lower_bound()
182 ? constraint.lower_bound() + offset
184 linear->add_domain(constraint.has_upper_bound()
185 ? constraint.upper_bound() + offset
188 if (problem.has_objective()) {
189 CpObjectiveProto* objective = result.mutable_objective();
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);
195 objective->add_vars(lit - 1);
196 objective->add_coeffs(coeff);
198 objective->add_vars(-lit - 1);
199 objective->add_coeffs(-coeff);
203 objective->set_offset(offset + problem.objective().offset());
204 objective->set_scaling_factor(problem.objective().scaling_factor());
210 LinearObjective* objective = problem->mutable_objective();
211 objective->set_scaling_factor(-objective->scaling_factor());
212 objective->set_offset(-objective->offset());
215 for (
auto& coefficients_ref : *objective->mutable_coefficients()) {
216 coefficients_ref = -coefficients_ref;
228 LOG(
WARNING) <<
"The given problem is invalid!";
231 if (solver->
parameters().log_search_progress()) {
232 LOG(
INFO) <<
"Loading problem '" << problem.name() <<
"', "
233 << problem.num_variables() <<
" variables, "
234 << problem.constraints_size() <<
" constraints.";
237 std::vector<LiteralWithCoeff> cst;
239 int num_constraints = 0;
240 for (
const LinearBooleanConstraint& constraint : problem.constraints()) {
241 num_terms += constraint.literals_size();
242 cst = ConvertLinearExpression(constraint);
244 constraint.has_lower_bound(), Coefficient(constraint.lower_bound()),
245 constraint.has_upper_bound(), Coefficient(constraint.upper_bound()),
247 LOG(
INFO) <<
"Problem detected to be UNSAT when "
248 <<
"adding the constraint #" << num_constraints
249 <<
" with name '" << constraint.name() <<
"'";
254 if (solver->
parameters().log_search_progress()) {
255 LOG(
INFO) <<
"The problem contains " << num_terms <<
" terms.";
264 LOG(
WARNING) <<
"The given problem is invalid! " << status.message();
266 if (solver->
parameters().log_search_progress()) {
267#if !defined(__PORTABLE_PLATFORM__)
268 LOG(
INFO) <<
"LinearBooleanProblem memory: " << problem->SpaceUsedLong();
270 LOG(
INFO) <<
"Loading problem '" << problem->name() <<
"', "
271 << problem->num_variables() <<
" variables, "
272 << problem->constraints_size() <<
" constraints.";
275 std::vector<LiteralWithCoeff> cst;
277 int num_constraints = 0;
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);
289 constraint.has_lower_bound(), Coefficient(constraint.lower_bound()),
290 constraint.has_upper_bound(), Coefficient(constraint.upper_bound()),
292 LOG(
INFO) <<
"Problem detected to be UNSAT when "
293 <<
"adding the constraint #" << num_constraints
294 <<
" with name '" << constraint.name() <<
"'";
297 delete problem->mutable_constraints()->ReleaseLast();
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.";
310 const LinearObjective& objective = problem.objective();
311 CHECK_EQ(objective.literals_size(), objective.coefficients_size());
312 int64 max_abs_weight = 0;
316 const double max_abs_weight_double = max_abs_weight;
317 for (
int i = 0; i < objective.literals_size(); ++i) {
320 const double abs_weight = std::abs(
coefficient) / max_abs_weight_double;
330 Coefficient upper_bound,
SatSolver* solver) {
331 std::vector<LiteralWithCoeff> cst =
332 ConvertLinearExpression(problem.objective());
338 bool use_lower_bound, Coefficient lower_bound,
339 bool use_upper_bound, Coefficient upper_bound,
341 std::vector<LiteralWithCoeff> cst =
342 ConvertLinearExpression(problem.objective());
344 use_upper_bound, upper_bound, &cst);
348 const std::vector<bool>& assignment) {
349 CHECK_EQ(assignment.size(), problem.num_variables());
351 const LinearObjective& objective = problem.objective();
352 for (
int i = 0; i < objective.literals_size(); ++i) {
355 sum += objective.coefficients(i);
362 const std::vector<bool>& assignment) {
363 CHECK_EQ(assignment.size(), problem.num_variables());
366 for (
const LinearBooleanConstraint& constraint : problem.constraints()) {
368 for (
int i = 0; i < constraint.literals_size(); ++i) {
371 sum += constraint.coefficients(i);
374 if (constraint.has_lower_bound() && sum < constraint.lower_bound()) {
375 LOG(
WARNING) <<
"Unsatisfied constraint! sum: " << sum <<
"\n"
379 if (constraint.has_upper_bound() && sum > constraint.upper_bound()) {
380 LOG(
WARNING) <<
"Unsatisfied constraint! sum: " << sum <<
"\n"
392 const LinearBooleanProblem& problem) {
394 const bool is_wcnf = (problem.objective().coefficients_size() > 0);
395 const LinearObjective& objective = problem.objective();
401 const int first_slack_variable = problem.original_num_variables();
404 absl::flat_hash_map<int, int64> literal_to_weight;
405 std::vector<std::pair<int, int64>> non_slack_objective;
410 int64 hard_weight = 1;
415 int signed_literal = objective.literals(i);
424 signed_literal = -signed_literal;
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));
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()),
439 output += absl::StrFormat(
"p cnf %d %d\n", problem.num_variables(),
440 problem.constraints_size());
443 std::string constraint_output;
444 for (
const LinearBooleanConstraint& constraint : problem.constraints()) {
445 if (constraint.literals_size() == 0)
return "";
446 constraint_output.clear();
448 for (
int i = 0; i < constraint.literals_size(); ++i) {
449 if (constraint.coefficients(i) != 1)
return "";
450 if (is_wcnf && abs(constraint.literals(i)) - 1 >= first_slack_variable) {
451 weight = literal_to_weight[constraint.literals(i)];
453 if (i > 0) constraint_output +=
" ";
458 output += absl::StrFormat(
"%d ",
weight);
460 output += constraint_output +
" 0\n";
465 for (std::pair<int, int64> p : non_slack_objective) {
477 BooleanAssignment* output) {
478 output->clear_literals();
481 output->add_literals(
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) {
495 subproblem->add_constraints()->MergeFrom(problem.constraints(
index));
509 const std::pair<int, int64> key(type,
coefficient.value());
514 absl::flat_hash_map<std::pair<int, int64>,
int> id_map_;
532template <
typename Graph>
534 const LinearBooleanProblem& problem,
535 std::vector<int>* initial_equivalence_classes) {
537 const int num_variables = problem.num_variables();
539 std::vector<LiteralWithCoeff> cst;
540 for (
const LinearBooleanConstraint& constraint : problem.constraints()) {
541 cst = ConvertLinearExpression(constraint);
543 constraint.has_lower_bound(), Coefficient(constraint.lower_bound()),
544 constraint.has_upper_bound(), Coefficient(constraint.upper_bound()),
551 initial_equivalence_classes->clear();
555 enum NodeType { LITERAL_NODE, CONSTRAINT_NODE, CONSTRAINT_COEFFICIENT_NODE };
556 IdGenerator id_generator;
560 for (
int i = 0; i < num_variables; ++i) {
571 initial_equivalence_classes->assign(
573 id_generator.GetId(NodeType::LITERAL_NODE, Coefficient(0)));
582 Coefficient max_value;
583 std::vector<LiteralWithCoeff> expr =
584 ConvertLinearExpression(problem.objective());
587 (*initial_equivalence_classes)[term.literal.Index().value()] =
588 id_generator.GetId(NodeType::LITERAL_NODE, term.coefficient);
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)));
608 int current_node_index = constraint_node_index;
609 Coefficient previous_coefficient(1);
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;
620 graph->AddArc(constraint_node_index, current_node_index);
621 graph->AddArc(current_node_index, constraint_node_index);
627 graph->AddArc(current_node_index, term.literal.Index().value());
628 graph->AddArc(term.literal.Index().value(), current_node_index);
632 DCHECK_EQ(graph->num_nodes(), initial_equivalence_classes->size());
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) {
644 mutable_objective->set_literals(i, -signed_literal);
645 mutable_objective->set_coefficients(i, -
coefficient);
649 mutable_objective->set_offset(mutable_objective->offset() + objective_offset);
652 for (LinearBooleanConstraint& constraint :
653 *(problem->mutable_constraints())) {
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));
662 if (constraint.has_lower_bound()) {
663 constraint.set_lower_bound(constraint.lower_bound() - sum);
665 if (constraint.has_upper_bound()) {
666 constraint.set_upper_bound(constraint.upper_bound() - sum);
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()) {
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]]++;
694 std::unique_ptr<Graph> remapped_graph =
RemapGraph(*graph, new_node_index);
696 *remapped_graph, absl::GetFlag(FLAGS_debug_dump_symmetry_graph_to_file),
699 LOG(DFATAL) <<
"Error when writing the symmetry graph to file: "
706 std::vector<int> factorized_automorphism_group_size;
709 &factorized_automorphism_group_size));
714 double average_support_size = 0.0;
715 int num_generators = 0;
716 for (
int i = 0; i < generators->size(); ++i) {
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);
724 for (
const int node : permutation->
Cycle(j)) {
725 DCHECK_GE(node, 2 * problem.num_variables());
731 if (!permutation->
Support().empty()) {
732 average_support_size += permutation->
Support().size();
733 swap((*generators)[num_generators], (*generators)[i]);
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;
745 LinearBooleanProblem* problem) {
746 Coefficient bound_shift;
747 Coefficient max_value;
748 std::vector<LiteralWithCoeff> cst;
751 cst = ConvertLinearExpression(problem->objective());
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());
759 mutable_objective->add_literals(entry.literal.SignedValue());
760 mutable_objective->add_coefficients(entry.coefficient.value());
764 for (LinearBooleanConstraint& constraint : *problem->mutable_constraints()) {
765 cst = ConvertLinearExpression(constraint);
766 constraint.clear_literals();
767 constraint.clear_coefficients();
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();
778 if (constraint.has_lower_bound()) {
779 constraint.set_lower_bound(constraint.lower_bound() +
780 bound_shift.value());
782 if (constraint.lower_bound() <= 0) {
783 constraint.clear_lower_bound();
788 if (constraint.has_lower_bound() || constraint.has_upper_bound()) {
790 constraint.add_literals(entry.literal.SignedValue());
791 constraint.add_coefficients(entry.coefficient.value());
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);
805 problem->mutable_constraints()->DeleteSubrange(new_index,
806 num_constraints - new_index);
810 for (LiteralIndex
index : mapping) {
815 problem->set_num_variables(num_vars);
819 problem->mutable_var_names()->DeleteSubrange(
820 num_vars, problem->var_names_size() - num_vars);
826 LinearBooleanProblem* problem) {
828 for (
int iter = 0; iter < 6; ++iter) {
831 LOG(
INFO) <<
"UNSAT when loading the problem.";
841 if (equiv_map.
empty()) {
859 BooleanVariable new_var(0);
873 if (equiv_map[
index] >= 0) {
875 const BooleanVariable image = var_map[l.
Variable()];
876 CHECK_NE(image, BooleanVariable(-1));
#define CHECK_LT(val1, val2)
#define CHECK_EQ(val1, val2)
#define DCHECK_GE(val1, val2)
#define CHECK_NE(val1, val2)
#define DCHECK_EQ(val1, val2)
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.")
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)
Iterator Cycle(int i) const
int NumConstraints() const
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
const std::vector< LiteralWithCoeff > & Constraint(int i) const
const Coefficient Rhs(int i) const
LiteralIndex NegatedIndex() const
LiteralIndex Index() const
BooleanVariable Variable() const
std::string DebugString() const
void FixVariable(Literal x)
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)
void SetNumVariables(int num_variables)
const SatParameters & parameters() const
const VariablesAssignment & Assignment() const
const Trail & LiteralTrail() const
void SetAssignmentPreference(Literal literal, double weight)
void Backtrack(int target_level)
bool VariableIsAssigned(BooleanVariable var) const
bool LiteralIsTrue(Literal literal) const
Literal GetTrueLiteralForAssignedVariable(BooleanVariable var) const
int NumberOfVariables() const
static const int32 kint32max
static const int32 kint32min
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)
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)
absl::Status WriteGraphToFile(const Graph &graph, const std::string &filename, bool directed, const std::vector< int > &num_nodes_with_color)
std::unique_ptr< Graph > RemapGraph(const Graph &graph, const std::vector< int > &new_node_index)
static int input(yyscan_t yyscanner)
std::vector< int >::const_iterator begin() const