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__)
30 #endif // __PORTABLE_PLATFORM__
39 ABSL_FLAG(std::string, debug_dump_symmetry_graph_to_file,
"",
40 "If this flag is non-empty, an undirected graph whose"
41 " automorphism group is in one-to-one correspondence with the"
42 " symmetries of the SAT problem will be dumped to a file every"
43 " time FindLinearBooleanProblemSymmetries() is called.");
51 const SatSolver& solver, std::vector<bool>* assignment) {
53 for (
int i = 0; i < problem.num_variables(); ++i) {
54 assignment->push_back(
65 template <
typename LinearTerms>
66 std::string ValidateLinearTerms(
const LinearTerms& terms,
67 std::vector<bool>* variable_seen) {
71 const int max_num_errs = 100;
72 for (
int i = 0; i < terms.literals_size(); ++i) {
73 if (terms.literals(i) == 0) {
74 if (++num_errs <= max_num_errs) {
75 err_str += absl::StrFormat(
"Zero literal at position %d\n", i);
78 if (terms.coefficients(i) == 0) {
79 if (++num_errs <= max_num_errs) {
80 err_str += absl::StrFormat(
"Literal %d has a zero coefficient\n",
84 const int var = Literal(terms.literals(i)).Variable().value();
85 if (
var >= variable_seen->size()) {
86 if (++num_errs <= max_num_errs) {
87 err_str += absl::StrFormat(
"Out of bound variable %d\n",
var);
90 if ((*variable_seen)[
var]) {
91 if (++num_errs <= max_num_errs) {
92 err_str += absl::StrFormat(
"Duplicated variable %d\n",
var);
95 (*variable_seen)[
var] =
true;
98 for (
int i = 0; i < terms.literals_size(); ++i) {
99 const int var = Literal(terms.literals(i)).Variable().value();
100 (*variable_seen)[
var] =
false;
103 if (num_errs <= max_num_errs) {
104 err_str = absl::StrFormat(
"%d validation errors:\n", num_errs) + err_str;
107 absl::StrFormat(
"%d validation errors; here are the first %d:\n",
108 num_errs, max_num_errs) +
117 template <
typename ProtoFormat>
118 std::vector<LiteralWithCoeff> ConvertLinearExpression(
119 const ProtoFormat&
input) {
120 std::vector<LiteralWithCoeff> cst;
121 cst.reserve(
input.literals_size());
122 for (
int i = 0; i <
input.literals_size(); ++i) {
124 cst.push_back(LiteralWithCoeff(
literal,
input.coefficients(i)));
132 std::vector<bool> variable_seen(problem.num_variables(),
false);
133 for (
int i = 0; i < problem.constraints_size(); ++i) {
134 const LinearBooleanConstraint& constraint = problem.constraints(i);
135 const std::string error = ValidateLinearTerms(constraint, &variable_seen);
136 if (!error.empty()) {
138 absl::StatusCode::kInvalidArgument,
139 absl::StrFormat(
"Invalid constraint %i: ", i) + error);
142 const std::string error =
143 ValidateLinearTerms(problem.objective(), &variable_seen);
144 if (!error.empty()) {
145 return absl::Status(absl::StatusCode::kInvalidArgument,
146 absl::StrFormat(
"Invalid objective: ") + error);
148 return ::absl::OkStatus();
153 for (
int i = 0; i < problem.num_variables(); ++i) {
154 IntegerVariableProto*
var = result.add_variables();
155 if (problem.var_names_size() > i) {
156 var->set_name(problem.var_names(i));
161 for (
const LinearBooleanConstraint& constraint : problem.constraints()) {
162 ConstraintProto*
ct = result.add_constraints();
163 ct->set_name(constraint.name());
164 LinearConstraintProto* linear =
ct->mutable_linear();
166 for (
int i = 0; i < constraint.literals_size(); ++i) {
168 const int lit = constraint.literals(i);
169 const int64 coeff = constraint.coefficients(i);
171 linear->add_vars(lit - 1);
172 linear->add_coeffs(coeff);
175 linear->add_vars(-lit - 1);
176 linear->add_coeffs(-coeff);
180 linear->add_domain(constraint.has_lower_bound()
181 ? constraint.lower_bound() + offset
183 linear->add_domain(constraint.has_upper_bound()
184 ? constraint.upper_bound() + offset
187 if (problem.has_objective()) {
188 CpObjectiveProto* objective = result.mutable_objective();
190 for (
int i = 0; i < problem.objective().literals_size(); ++i) {
191 const int lit = problem.objective().literals(i);
192 const int64 coeff = problem.objective().coefficients(i);
194 objective->add_vars(lit - 1);
195 objective->add_coeffs(coeff);
197 objective->add_vars(-lit - 1);
198 objective->add_coeffs(-coeff);
202 objective->set_offset(offset + problem.objective().offset());
203 objective->set_scaling_factor(problem.objective().scaling_factor());
209 LinearObjective* objective = problem->mutable_objective();
210 objective->set_scaling_factor(-objective->scaling_factor());
211 objective->set_offset(-objective->offset());
214 for (
auto& coefficients_ref : *objective->mutable_coefficients()) {
215 coefficients_ref = -coefficients_ref;
227 LOG(
WARNING) <<
"The given problem is invalid!";
230 if (solver->
parameters().log_search_progress()) {
231 LOG(
INFO) <<
"Loading problem '" << problem.name() <<
"', "
232 << problem.num_variables() <<
" variables, "
233 << problem.constraints_size() <<
" constraints.";
236 std::vector<LiteralWithCoeff> cst;
238 int num_constraints = 0;
239 for (
const LinearBooleanConstraint& constraint : problem.constraints()) {
240 num_terms += constraint.literals_size();
241 cst = ConvertLinearExpression(constraint);
243 constraint.has_lower_bound(), Coefficient(constraint.lower_bound()),
244 constraint.has_upper_bound(), Coefficient(constraint.upper_bound()),
246 LOG(
INFO) <<
"Problem detected to be UNSAT when "
247 <<
"adding the constraint #" << num_constraints
248 <<
" with name '" << constraint.name() <<
"'";
253 if (solver->
parameters().log_search_progress()) {
254 LOG(
INFO) <<
"The problem contains " << num_terms <<
" terms.";
263 LOG(
WARNING) <<
"The given problem is invalid! " << status.message();
265 if (solver->
parameters().log_search_progress()) {
266 #if !defined(__PORTABLE_PLATFORM__)
267 LOG(
INFO) <<
"LinearBooleanProblem memory: " << problem->SpaceUsedLong();
269 LOG(
INFO) <<
"Loading problem '" << problem->name() <<
"', "
270 << problem->num_variables() <<
" variables, "
271 << problem->constraints_size() <<
" constraints.";
274 std::vector<LiteralWithCoeff> cst;
276 int num_constraints = 0;
281 std::reverse(problem->mutable_constraints()->begin(),
282 problem->mutable_constraints()->end());
283 for (
int i = problem->constraints_size() - 1; i >= 0; --i) {
284 const LinearBooleanConstraint& constraint = problem->constraints(i);
285 num_terms += constraint.literals_size();
286 cst = ConvertLinearExpression(constraint);
288 constraint.has_lower_bound(), Coefficient(constraint.lower_bound()),
289 constraint.has_upper_bound(), Coefficient(constraint.upper_bound()),
291 LOG(
INFO) <<
"Problem detected to be UNSAT when "
292 <<
"adding the constraint #" << num_constraints
293 <<
" with name '" << constraint.name() <<
"'";
296 delete problem->mutable_constraints()->ReleaseLast();
299 LinearBooleanProblem empty_problem;
300 problem->mutable_constraints()->Swap(empty_problem.mutable_constraints());
301 if (solver->
parameters().log_search_progress()) {
302 LOG(
INFO) <<
"The problem contains " << num_terms <<
" terms.";
309 const LinearObjective& objective = problem.objective();
310 CHECK_EQ(objective.literals_size(), objective.coefficients_size());
311 int64 max_abs_weight = 0;
315 const double max_abs_weight_double = max_abs_weight;
316 for (
int i = 0; i < objective.literals_size(); ++i) {
319 const double abs_weight = std::abs(
coefficient) / max_abs_weight_double;
329 Coefficient upper_bound,
SatSolver* solver) {
330 std::vector<LiteralWithCoeff> cst =
331 ConvertLinearExpression(problem.objective());
337 bool use_lower_bound, Coefficient lower_bound,
338 bool use_upper_bound, Coefficient upper_bound,
340 std::vector<LiteralWithCoeff> cst =
341 ConvertLinearExpression(problem.objective());
343 use_upper_bound, upper_bound, &cst);
347 const std::vector<bool>& assignment) {
348 CHECK_EQ(assignment.size(), problem.num_variables());
350 const LinearObjective& objective = problem.objective();
351 for (
int i = 0; i < objective.literals_size(); ++i) {
354 sum += objective.coefficients(i);
361 const std::vector<bool>& assignment) {
362 CHECK_EQ(assignment.size(), problem.num_variables());
365 for (
const LinearBooleanConstraint& constraint : problem.constraints()) {
367 for (
int i = 0; i < constraint.literals_size(); ++i) {
370 sum += constraint.coefficients(i);
373 if (constraint.has_lower_bound() && sum < constraint.lower_bound()) {
374 LOG(
WARNING) <<
"Unsatisfied constraint! sum: " << sum <<
"\n"
378 if (constraint.has_upper_bound() && sum > constraint.upper_bound()) {
379 LOG(
WARNING) <<
"Unsatisfied constraint! sum: " << sum <<
"\n"
391 const LinearBooleanProblem& problem) {
393 const bool is_wcnf = (problem.objective().coefficients_size() > 0);
394 const LinearObjective& objective = problem.objective();
400 const int first_slack_variable = problem.original_num_variables();
403 absl::flat_hash_map<int, int64> literal_to_weight;
404 std::vector<std::pair<int, int64>> non_slack_objective;
409 int64 hard_weight = 1;
414 int signed_literal = objective.literals(i);
423 signed_literal = -signed_literal;
426 literal_to_weight[objective.literals(i)] =
weight;
427 if (
Literal(signed_literal).Variable() < first_slack_variable) {
428 non_slack_objective.push_back(std::make_pair(signed_literal,
weight));
433 output += absl::StrFormat(
"p wcnf %d %d %d\n", first_slack_variable,
434 static_cast<int>(problem.constraints_size() +
435 non_slack_objective.size()),
438 output += absl::StrFormat(
"p cnf %d %d\n", problem.num_variables(),
439 problem.constraints_size());
442 std::string constraint_output;
443 for (
const LinearBooleanConstraint& constraint : problem.constraints()) {
444 if (constraint.literals_size() == 0)
return "";
445 constraint_output.clear();
447 for (
int i = 0; i < constraint.literals_size(); ++i) {
448 if (constraint.coefficients(i) != 1)
return "";
449 if (is_wcnf && abs(constraint.literals(i)) - 1 >= first_slack_variable) {
450 weight = literal_to_weight[constraint.literals(i)];
452 if (i > 0) constraint_output +=
" ";
457 output += absl::StrFormat(
"%d ",
weight);
459 output += constraint_output +
" 0\n";
464 for (std::pair<int, int64> p : non_slack_objective) {
476 BooleanAssignment* output) {
477 output->clear_literals();
480 output->add_literals(
487 const std::vector<int>& constraint_indices,
488 LinearBooleanProblem* subproblem) {
489 *subproblem = problem;
490 subproblem->set_name(
"Subproblem of " + problem.name());
491 subproblem->clear_constraints();
492 for (
int index : constraint_indices) {
494 subproblem->add_constraints()->MergeFrom(problem.constraints(
index));
508 const std::pair<int, int64> key(type,
coefficient.value());
513 absl::flat_hash_map<std::pair<int, int64>,
int> id_map_;
531 template <
typename Graph>
533 const LinearBooleanProblem& problem,
534 std::vector<int>* initial_equivalence_classes) {
536 const int num_variables = problem.num_variables();
538 std::vector<LiteralWithCoeff> cst;
539 for (
const LinearBooleanConstraint& constraint : problem.constraints()) {
540 cst = ConvertLinearExpression(constraint);
542 constraint.has_lower_bound(), Coefficient(constraint.lower_bound()),
543 constraint.has_upper_bound(), Coefficient(constraint.upper_bound()),
550 initial_equivalence_classes->clear();
554 enum NodeType { LITERAL_NODE, CONSTRAINT_NODE, CONSTRAINT_COEFFICIENT_NODE };
555 IdGenerator id_generator;
559 for (
int i = 0; i < num_variables; ++i) {
570 initial_equivalence_classes->assign(
572 id_generator.GetId(NodeType::LITERAL_NODE, Coefficient(0)));
581 Coefficient max_value;
582 std::vector<LiteralWithCoeff> expr =
583 ConvertLinearExpression(problem.objective());
586 (*initial_equivalence_classes)[term.literal.Index().value()] =
587 id_generator.GetId(NodeType::LITERAL_NODE, term.coefficient);
597 const int constraint_node_index = initial_equivalence_classes->size();
598 initial_equivalence_classes->push_back(id_generator.GetId(
599 NodeType::CONSTRAINT_NODE, canonical_problem.
Rhs(i)));
607 int current_node_index = constraint_node_index;
608 Coefficient previous_coefficient(1);
610 if (term.coefficient != previous_coefficient) {
611 current_node_index = initial_equivalence_classes->size();
612 initial_equivalence_classes->push_back(id_generator.GetId(
613 NodeType::CONSTRAINT_COEFFICIENT_NODE, term.coefficient));
614 previous_coefficient = term.coefficient;
619 graph->AddArc(constraint_node_index, current_node_index);
620 graph->AddArc(current_node_index, constraint_node_index);
626 graph->AddArc(current_node_index, term.literal.Index().value());
627 graph->AddArc(term.literal.Index().value(), current_node_index);
631 DCHECK_EQ(graph->num_nodes(), initial_equivalence_classes->size());
637 LinearObjective* mutable_objective = problem->mutable_objective();
638 int64 objective_offset = 0;
639 for (
int i = 0; i < mutable_objective->literals_size(); ++i) {
640 const int signed_literal = mutable_objective->literals(i);
641 if (signed_literal < 0) {
643 mutable_objective->set_literals(i, -signed_literal);
644 mutable_objective->set_coefficients(i, -
coefficient);
648 mutable_objective->set_offset(mutable_objective->offset() + objective_offset);
651 for (LinearBooleanConstraint& constraint :
652 *(problem->mutable_constraints())) {
654 for (
int i = 0; i < constraint.literals_size(); ++i) {
655 if (constraint.literals(i) < 0) {
656 sum += constraint.coefficients(i);
657 constraint.set_literals(i, -constraint.literals(i));
658 constraint.set_coefficients(i, -constraint.coefficients(i));
661 if (constraint.has_lower_bound()) {
662 constraint.set_lower_bound(constraint.lower_bound() - sum);
664 if (constraint.has_upper_bound()) {
665 constraint.set_upper_bound(constraint.upper_bound() - sum);
671 const LinearBooleanProblem& problem,
672 std::vector<std::unique_ptr<SparsePermutation>>* generators) {
674 std::vector<int> equivalence_classes;
675 std::unique_ptr<Graph> graph(
676 GenerateGraphForSymmetryDetection<Graph>(problem, &equivalence_classes));
677 LOG(
INFO) <<
"Graph has " << graph->num_nodes() <<
" nodes and "
678 << graph->num_arcs() / 2 <<
" edges.";
679 #if !defined(__PORTABLE_PLATFORM__)
680 if (!absl::GetFlag(FLAGS_debug_dump_symmetry_graph_to_file).empty()) {
682 std::vector<int> new_node_index(graph->num_nodes(), -1);
683 const int num_classes = 1 + *std::max_element(equivalence_classes.begin(),
684 equivalence_classes.end());
685 std::vector<int> class_size(num_classes, 0);
686 for (
const int c : equivalence_classes) ++class_size[c];
687 std::vector<int> next_index_by_class(num_classes, 0);
688 std::partial_sum(class_size.begin(), class_size.end() - 1,
689 next_index_by_class.begin() + 1);
690 for (
int node = 0; node < graph->num_nodes(); ++node) {
691 new_node_index[node] = next_index_by_class[equivalence_classes[node]]++;
693 std::unique_ptr<Graph> remapped_graph =
RemapGraph(*graph, new_node_index);
695 *remapped_graph, absl::GetFlag(FLAGS_debug_dump_symmetry_graph_to_file),
698 LOG(DFATAL) <<
"Error when writing the symmetry graph to file: "
702 #endif // __PORTABLE_PLATFORM__
705 std::vector<int> factorized_automorphism_group_size;
708 std::numeric_limits<double>::infinity(),
709 &equivalence_classes, generators, &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));