always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

more symmetry detection

Browse Source
This commit is contained in:
Laurent Perron
2018-07-13 09:39:03 -07:00
parent 83a2129026
commit 12c83e19cf
1 changed files with 101 additions and 32 deletions
Download Patch File Download Diff File Expand all files Collapse all files

133
ortools/sat/cp_model_symmetries.cc
View File

@@ -54,22 +54,18 @@ class IdGenerator {
};
// Appends values in `repeated_field` to `vector`.
template <typename FieldIntType>
void Append(const google::protobuf::RepeatedField<FieldIntType>& repeated_field,
std::vector<int64>* vector) {
//
// We use a template as proto int64 != C++ int64 in open source.
template <typename FieldInt64Type>
void Append(
const google::protobuf::RepeatedField<FieldInt64Type>& repeated_field,
std::vector<int64>* vector) {
CHECK(vector != nullptr);
for (const FieldIntType value : repeated_field) {
for (const FieldInt64Type value : repeated_field) {
vector->push_back(value);
}
}
template <typename Graph>
void AddEdge(int node_index_1, int node_index_2, Graph* graph) {
CHECK(graph != nullptr);
graph->AddArc(node_index_1, node_index_2);
graph->AddArc(node_index_2, node_index_1);
}
// Returns a graph whose automorphisms can be mapped back to the symmetries of
// the model described in the given CpModelProto.
//
@@ -102,7 +98,12 @@ std::unique_ptr<Graph> GenerateGraphForSymmetryDetection(
const int num_variables = problem.variables_size();
auto graph = absl::make_unique<Graph>();
initial_equivalence_classes->clear();
enum NodeType { VARIABLE_NODE, CONSTRAINT_NODE, CONSTRAINT_COEFFICIENT_NODE };
enum NodeType {
VARIABLE_NODE,
CONSTRAINT_NODE,
CONSTRAINT_COEFFICIENT_NODE,
ENFORCEMENT_LITERAL
};
IdGenerator id_generator;
// For two variables to be in the same equivalence class, they need to have
@@ -113,36 +114,55 @@ std::unique_ptr<Graph> GenerateGraphForSymmetryDetection(
problem.objective().coeffs(i);
}
auto new_node = [&initial_equivalence_classes,
&id_generator](const std::vector<int64>& key) {
// Since we add nodes one by one, initial_equivalence_classes->size() gives
// the number of nodes at any point, which we use as the next node index.
const int node = initial_equivalence_classes->size();
initial_equivalence_classes->push_back(id_generator.GetId(key));
return node;
};
for (int v = 0; v < num_variables; ++v) {
const IntegerVariableProto& variable = problem.variables(v);
std::vector<int64> key = {VARIABLE_NODE, objective_by_var[v]};
Append(variable.domain(), &key);
initial_equivalence_classes->push_back(id_generator.GetId(key));
CHECK_EQ(v, new_node(key));
// Make sure the graph contains all the variable nodes, even if no edges are
// attached to them through constraints.
graph->AddNode(v);
}
auto add_edge = [&graph](int node_1, int node_2) {
graph->AddArc(node_1, node_2);
graph->AddArc(node_2, node_1);
};
auto add_literal_edge = [&add_edge, &new_node](int ref, int constraint_node) {
const int variable_node = PositiveRef(ref);
if (RefIsPositive(ref)) {
add_edge(variable_node, constraint_node);
} else {
const int coefficient_node = new_node({CONSTRAINT_COEFFICIENT_NODE, -1});
add_edge(variable_node, coefficient_node);
add_edge(coefficient_node, constraint_node);
}
};
// Add constraints to the graph.
for (const ConstraintProto& constraint : problem.constraints()) {
// Since we add nodes one by one, initial_equivalence_classes->size() gives
// the number of nodes at any point, which we use as the next node index.
const int constraint_node_index = initial_equivalence_classes->size();
const int constraint_node = initial_equivalence_classes->size();
std::vector<int64> key = {CONSTRAINT_NODE, constraint.constraint_case()};
switch (constraint.constraint_case()) {
case ConstraintProto::kLinear: {
std::vector<int64> key = {CONSTRAINT_NODE, ConstraintProto::kLinear};
Append(constraint.linear().domain(), &key);
initial_equivalence_classes->push_back(id_generator.GetId(key));
CHECK_EQ(constraint_node, new_node(key));
for (int i = 0; i < constraint.linear().vars_size(); ++i) {
if (constraint.enforcement_literal_size() > 0) {
// TODO(user): support enforcement literals on constraints.
LOG(ERROR) << "Unsupported enforcement literal on constraints.";
return nullptr;
}
if (constraint.linear().coeffs(i) == 0) continue;
const int ref = constraint.linear().vars(i);
const int variable_node_index = PositiveRef(ref);
const int variable_node = PositiveRef(ref);
const int64 coeff = RefIsPositive(ref)
? constraint.linear().coeffs(i)
: -constraint.linear().coeffs(i);
@@ -150,19 +170,57 @@ std::unique_ptr<Graph> GenerateGraphForSymmetryDetection(
// For all coefficients equal to one, which are the most common, we
// can optimize the size of the graph by omitting the coefficient
// node altogether.
AddEdge(variable_node_index, constraint_node_index, graph.get());
add_edge(variable_node, constraint_node);
} else {
const int coefficient_node_index =
initial_equivalence_classes->size();
initial_equivalence_classes->push_back(
id_generator.GetId({CONSTRAINT_COEFFICIENT_NODE, coeff}));
const int coefficient_node =
new_node({CONSTRAINT_COEFFICIENT_NODE, coeff});
AddEdge(variable_node_index, coefficient_node_index, graph.get());
AddEdge(coefficient_node_index, constraint_node_index, graph.get());
add_edge(variable_node, coefficient_node);
add_edge(coefficient_node, constraint_node);
}
}
break;
}
case ConstraintProto::kBoolOr: {
CHECK_EQ(constraint_node, new_node(key));
for (const int ref : constraint.bool_or().literals()) {
add_literal_edge(ref, constraint_node);
}
break;
}
case ConstraintProto::kBoolXor: {
CHECK_EQ(constraint_node, new_node(key));
for (const int ref : constraint.bool_xor().literals()) {
add_literal_edge(ref, constraint_node);
}
break;
}
case ConstraintProto::kBoolAnd: {
if (constraint.enforcement_literal_size() == 0) {
// All literals are true in this case.
CHECK_EQ(constraint_node, new_node(key));
for (const int ref : constraint.bool_and().literals()) {
add_literal_edge(ref, constraint_node);
}
break;
}
// To make the BoolAnd constraint more generic in the graph, we expand
// it into a set of BoolOr constraints where
// not(enforcement_literal) OR literal = true
// for all constraint's literals. This is equivalent to
// enforcement_literal => literal
// for all literals.
std::vector<int64> key = {CONSTRAINT_NODE, ConstraintProto::kBoolOr};
const int non_enforcement_literal =
NegatedRef(constraint.enforcement_literal(0));
for (const int literal : constraint.bool_and().literals()) {
const int constraint_node = new_node(key);
add_literal_edge(non_enforcement_literal, constraint_node);
add_literal_edge(literal, constraint_node);
}
break;
}
default: {
// If the model contains any non-supported constraints, return an empty
// graph.
@@ -172,6 +230,17 @@ std::unique_ptr<Graph> GenerateGraphForSymmetryDetection(
return nullptr;
}
}
if (constraint.constraint_case() != ConstraintProto::kBoolAnd &&
constraint.enforcement_literal_size() > 0) {
const int ref = constraint.enforcement_literal(0);
const int enforcement_literal_node = PositiveRef(ref);
const int enforcement_type_node =
new_node({ENFORCEMENT_LITERAL, RefIsPositive(ref)});
add_edge(constraint_node, enforcement_type_node);
add_edge(enforcement_type_node, enforcement_literal_node);
}
}
graph->Build();
@@ -204,7 +273,7 @@ void FindCpModelSymmetries(
&factorized_automorphism_group_size));
// Remove from the permutations the part not concerning the variables.
// Note that some permutation may become empty, which means that we had
// Note that some permutations may become empty, which means that we had
// duplicate constraints.
double average_support_size = 0.0;
int num_generators = 0;