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"
36#if !defined(__PORTABLE_PLATFORM__)
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.");
65 const SatSolver& solver, std::vector<bool>* assignment) {
68 assignment->push_back(
79template <
typename LinearTerms>
80std::string ValidateLinearTerms(
const LinearTerms& terms,
81 std::vector<bool>* variable_seen) {
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);
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",
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);
104 if ((*variable_seen)[var]) {
105 if (++num_errs <= max_num_errs) {
106 err_str += absl::StrFormat(
"Duplicated variable %d\n", var);
109 (*variable_seen)[var] =
true;
112 for (
int i = 0;
i < terms.literals_size(); ++
i) {
114 (*variable_seen)[var] =
false;
117 if (num_errs <= max_num_errs) {
118 err_str = absl::StrFormat(
"%d validation errors:\n", num_errs) + err_str;
121 absl::StrFormat(
"%d validation errors; here are the first %d:\n",
122 num_errs, max_num_errs) +
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) {
146 std::vector<bool> variable_seen(problem.
num_variables(),
false);
149 const std::string error = ValidateLinearTerms(constraint, &variable_seen);
150 if (!error.empty()) {
152 absl::StatusCode::kInvalidArgument,
153 absl::StrFormat(
"Invalid constraint %i: ",
i) + error);
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);
162 return ::absl::OkStatus();
180 for (
int i = 0;
i < constraint.literals_size(); ++
i) {
182 const int lit = constraint.literals(
i);
183 const int64_t coeff = constraint.coefficients(
i);
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);
204 for (
int i = 0;
i < problem.
objective().literals_size(); ++
i) {
229 coefficients_ref = -coefficients_ref;
241 LOG(WARNING) <<
"The given problem is invalid!";
245 LOG(INFO) <<
"Loading problem '" << problem.
name() <<
"', "
250 std::vector<LiteralWithCoeff> cst;
251 int64_t num_terms = 0;
252 int num_constraints = 0;
254 num_terms += constraint.literals_size();
255 cst = ConvertLinearExpression(constraint);
257 constraint.has_lower_bound(), Coefficient(constraint.lower_bound()),
258 constraint.has_upper_bound(), Coefficient(constraint.upper_bound()),
260 LOG(INFO) <<
"Problem detected to be UNSAT when "
261 <<
"adding the constraint #" << num_constraints
262 <<
" with name '" << constraint.name() <<
"'";
268 LOG(INFO) <<
"The problem contains " << num_terms <<
" terms.";
277 LOG(WARNING) <<
"The given problem is invalid! " << status.message();
280#if !defined(__PORTABLE_PLATFORM__)
281 LOG(INFO) <<
"LinearBooleanProblem memory: " << problem->SpaceUsedLong();
283 LOG(INFO) <<
"Loading problem '" << problem->
name() <<
"', "
288 std::vector<LiteralWithCoeff> cst;
289 int64_t num_terms = 0;
290 int num_constraints = 0;
300 cst = ConvertLinearExpression(constraint);
305 LOG(INFO) <<
"Problem detected to be UNSAT when "
306 <<
"adding the constraint #" << num_constraints
307 <<
" with name '" << constraint.
name() <<
"'";
316 LOG(INFO) <<
"The problem contains " << num_terms <<
" terms.";
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));
329 const double max_abs_weight_double = max_abs_weight;
333 const double abs_weight = std::abs(coefficient) / max_abs_weight_double;
338 coefficient > 0 ? literal.
Negated() : literal, abs_weight);
343 Coefficient upper_bound,
SatSolver* solver) {
344 std::vector<LiteralWithCoeff> cst =
345 ConvertLinearExpression(problem.
objective());
351 bool use_lower_bound, Coefficient lower_bound,
352 bool use_upper_bound, Coefficient upper_bound,
354 std::vector<LiteralWithCoeff> cst =
355 ConvertLinearExpression(problem.
objective());
357 use_upper_bound, upper_bound, &cst);
361 const std::vector<bool>& assignment) {
375 const std::vector<bool>& assignment) {
381 for (
int i = 0;
i < constraint.literals_size(); ++
i) {
382 const Literal literal(constraint.literals(
i));
384 sum += constraint.coefficients(
i);
387 if (constraint.has_lower_bound() && sum < constraint.lower_bound()) {
388 LOG(WARNING) <<
"Unsatisfied constraint! sum: " << sum <<
"\n"
392 if (constraint.has_upper_bound() && sum > constraint.upper_bound()) {
393 LOG(WARNING) <<
"Unsatisfied constraint! sum: " << sum <<
"\n"
407 const bool is_wcnf = (problem.
objective().coefficients_size() > 0);
417 absl::flat_hash_map<int, int64_t> literal_to_weight;
418 std::vector<std::pair<int, int64_t>> non_slack_objective;
423 int64_t hard_weight = 1;
428 int signed_literal = objective.
literals(
i);
437 signed_literal = -signed_literal;
440 literal_to_weight[objective.
literals(
i)] = weight;
442 non_slack_objective.push_back(std::make_pair(signed_literal, weight));
444 hard_weight += weight;
447 output += absl::StrFormat(
"p wcnf %d %d %d\n", first_slack_variable,
449 non_slack_objective.size()),
452 output += absl::StrFormat(
"p cnf %d %d\n", problem.
num_variables(),
456 std::string constraint_output;
458 if (constraint.literals_size() == 0)
return "";
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 "";
463 if (is_wcnf && abs(constraint.literals(
i)) - 1 >= first_slack_variable) {
464 weight = literal_to_weight[constraint.literals(
i)];
466 if (
i > 0) constraint_output +=
" ";
471 output += absl::StrFormat(
"%d ", weight);
473 output += constraint_output +
" 0\n";
478 for (std::pair<int, int64_t> p : non_slack_objective) {
481 const Literal literal(-p.first);
482 output += absl::StrFormat(
"%d %s 0\n", p.second, literal.
DebugString());
501 absl::Span<const int> constraint_indices,
503 *subproblem = problem;
504 subproblem->
set_name(
"Subproblem of " + problem.
name());
506 for (
int index : constraint_indices) {
517 IdGenerator() =
default;
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;
527 absl::flat_hash_map<std::pair<int, int64_t>,
int> id_map_;
545template <
typename Graph>
548 std::vector<int>* initial_equivalence_classes) {
552 std::vector<LiteralWithCoeff> cst;
554 cst = ConvertLinearExpression(constraint);
556 constraint.has_lower_bound(), Coefficient(constraint.lower_bound()),
557 constraint.has_upper_bound(), Coefficient(constraint.upper_bound()),
564 initial_equivalence_classes->clear();
568 enum NodeType { LITERAL_NODE, CONSTRAINT_NODE, CONSTRAINT_COEFFICIENT_NODE };
569 IdGenerator id_generator;
573 for (
int i = 0;
i < num_variables; ++
i) {
584 initial_equivalence_classes->assign(
586 id_generator.GetId(NodeType::LITERAL_NODE, Coefficient(0)));
595 Coefficient max_value;
596 std::vector<LiteralWithCoeff> expr =
597 ConvertLinearExpression(problem.
objective());
600 (*initial_equivalence_classes)[term.literal.Index().value()] =
601 id_generator.GetId(NodeType::LITERAL_NODE, term.coefficient);
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)));
621 int current_node_index = constraint_node_index;
622 Coefficient previous_coefficient(1);
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;
633 graph->
AddArc(constraint_node_index, current_node_index);
634 graph->
AddArc(current_node_index, constraint_node_index);
640 graph->
AddArc(current_node_index, term.literal.Index().value());
641 graph->
AddArc(term.literal.Index().value(), current_node_index);
645 DCHECK_EQ(graph->
num_nodes(), initial_equivalence_classes->size());
652 int64_t objective_offset = 0;
654 const int signed_literal = mutable_objective->
literals(
i);
655 if (signed_literal < 0) {
656 const int64_t coefficient = mutable_objective->
coefficients(
i);
659 objective_offset += coefficient;
662 mutable_objective->
set_offset(mutable_objective->
offset() + objective_offset);
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));
675 if (constraint.has_lower_bound()) {
676 constraint.set_lower_bound(constraint.lower_bound() - sum);
678 if (constraint.has_upper_bound()) {
679 constraint.set_upper_bound(constraint.upper_bound() - sum);
686 std::vector<std::unique_ptr<SparsePermutation>>* generators) {
688 std::vector<int> equivalence_classes;
689 std::unique_ptr<Graph> graph(
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()) {
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]]++;
707 std::unique_ptr<Graph> remapped_graph =
RemapGraph(*graph, new_node_index);
709 *remapped_graph, absl::GetFlag(FLAGS_debug_dump_symmetry_graph_to_file),
712 LOG(DFATAL) <<
"Error when writing the symmetry graph to file: "
719 std::vector<int> factorized_automorphism_group_size;
721 CHECK_OK(symmetry_finder.
FindSymmetries(&equivalence_classes, generators,
722 &factorized_automorphism_group_size));
727 double average_support_size = 0.0;
728 int num_generators = 0;
729 for (
int i = 0;
i < generators->size(); ++
i) {
731 std::vector<int> to_delete;
732 for (
int j = 0; j < permutation->
NumCycles(); ++j) {
734 to_delete.push_back(j);
737 for (
const int node : permutation->
Cycle(j)) {
744 if (!permutation->
Support().empty()) {
745 average_support_size += permutation->
Support().size();
746 swap((*generators)[num_generators], (*generators)[
i]);
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;
759 Coefficient bound_shift;
760 Coefficient max_value;
761 std::vector<LiteralWithCoeff> cst;
764 cst = ConvertLinearExpression(problem->
objective());
770 bound_shift.value());
772 mutable_objective->
add_literals(entry.literal.SignedValue());
778 cst = ConvertLinearExpression(constraint);
779 constraint.clear_literals();
780 constraint.clear_coefficients();
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();
791 if (constraint.has_lower_bound()) {
792 constraint.set_lower_bound(constraint.lower_bound() +
793 bound_shift.value());
795 if (constraint.lower_bound() <= 0) {
796 constraint.clear_lower_bound();
801 if (constraint.has_lower_bound() || constraint.has_upper_bound()) {
803 constraint.add_literals(entry.literal.SignedValue());
804 constraint.add_coefficients(entry.coefficient.value());
812 for (
int i = 0;
i < num_constraints; ++
i) {
819 num_constraints - new_index);
823 for (LiteralIndex index : mapping) {
841 for (
int iter = 0; iter < 6; ++iter) {
844 LOG(INFO) <<
"UNSAT when loading the problem.";
854 if (equiv_map.empty()) {
856 for (LiteralIndex index(0); index < num_literals; ++index) {
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()) {
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));
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)
::util::StaticGraph Graph
void RemoveCycles(absl::Span< const int > cycle_indices)
const std::vector< int > & Support() const
Iterator Cycle(int i) const
void add_literals(::int32_t value)
int NumConstraints() const
Getters. All the constraints are guaranteed to be in canonical form.
Coefficient Rhs(int i) const
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_scaling_factor(double value)
void add_coeffs(::int64_t value)
void set_offset(double value)
void add_vars(::int32_t value)
void add_domain(::int64_t value)
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;
const ::std::string & name() const
::int64_t lower_bound() const
bool has_upper_bound() const
optional int64 upper_bound = 4;
::int64_t upper_bound() const
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
void set_num_variables(::int32_t value)
const ::std::string & name() const
::int32_t original_num_variables() 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
::int32_t num_variables() 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)
void add_vars(::int32_t value)
void add_domain(::int64_t value)
void add_coeffs(::int64_t value)
int literals_size() const
repeated int32 literals = 1;
void add_literals(::int32_t value)
void clear_coefficients()
void set_literals(int index, ::int32_t value)
void add_coefficients(::int64_t value)
::int64_t coefficients(int index) const
void set_scaling_factor(double value)
double scaling_factor() const
::int32_t literals(int index) const
::google::protobuf::RepeatedField<::int64_t > *PROTOBUF_NONNULL mutable_coefficients()
void set_coefficients(int index, ::int64_t value)
void set_offset(double value)
int coefficients_size() const
repeated int64 coefficients = 2;
std::string DebugString() const
LiteralIndex NegatedIndex() const
LiteralIndex Index() const
BooleanVariable Variable() const
bool log_search_progress() const
void ApplyMapping(const util_intops::StrongVector< BooleanVariable, BooleanVariable > &mapping)
void FixVariable(Literal x)
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)
void Backtrack(int target_level)
const SatParameters & parameters() const
const VariablesAssignment & Assignment() const
const Trail & LiteralTrail() const
void SetNumVariables(int num_variables)
bool VariableIsAssigned(BooleanVariable var) const
Returns true iff the given variable is assigned.
Literal GetTrueLiteralForAssignedVariable(BooleanVariable var) const
int NumberOfVariables() const
bool LiteralIsTrue(Literal literal) const
NodeIndexType num_nodes() const
ArcIndexType AddArc(NodeIndexType tail, NodeIndexType head)
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)
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.
std::string ProtobufDebugString(const P &message)
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)
std::unique_ptr< Graph > RemapGraph(const Graph &graph, absl::Span< const int > new_node_index)
static int input(yyscan_t yyscanner)
std::vector< int >::const_iterator begin() const
Represents a term in a pseudo-Boolean formula.