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

[CP-SAT] various fixes for corner cases in presolve, checker; added some presolve for all_diff and bool_xor; internal cleanup

Browse Source
This commit is contained in:
Laurent Perron
2021-09-27 19:40:36 +02:00
parent c754932ce4
commit bc2ab43d03
8 changed files with 148 additions and 46 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
ortools/sat/cp_model_checker.cc
View File

@@ -1445,7 +1445,9 @@ bool SolutionIsFeasible(const CpModelProto& model,
const CpModelProto* mapping_proto,
const std::vector<int>* postsolve_mapping) {
if (variable_values.size() != model.variables_size()) {
VLOG(1) << "Wrong number of variables in the solution vector";
VLOG(1) << "Wrong number of variables (" << variable_values.size()
<< ") in the solution vector. It should be "
<< model.variables_size() << ".";
return false;
}

119
ortools/sat/cp_model_presolve.cc
View File

@@ -170,11 +170,41 @@ bool CpModelPresolver::PresolveBoolXor(ConstraintProto* ct) {
ct->mutable_bool_xor()->set_literals(new_size++, literal);
}
if (new_size == 1) {
context_->UpdateRuleStats("TODO bool_xor: one active literal");
} else if (new_size == 2) {
context_->UpdateRuleStats("TODO bool_xor: two active literals");
if (new_size == 0) {
if (num_true_literals % 2 == 0) {
return context_->NotifyThatModelIsUnsat("bool_xor: always false");
} else {
context_->UpdateRuleStats("bool_xor: always true");
return RemoveConstraint(ct);
}
} else if (new_size == 1) { // We can fix the only active literal.
if (num_true_literals % 2 == 0) {
if (!context_->SetLiteralToTrue(ct->bool_xor().literals(0))) {
return context_->NotifyThatModelIsUnsat(
"bool_xor: cannot fix last literal");
}
} else {
if (!context_->SetLiteralToFalse(ct->bool_xor().literals(0))) {
return context_->NotifyThatModelIsUnsat(
"bool_xor: cannot fix last literal");
}
}
context_->UpdateRuleStats("bool_xor: one active literal");
return RemoveConstraint(ct);
} else if (new_size == 2) { // We can simplify the bool_xor.
const int a = ct->bool_xor().literals(0);
const int b = ct->bool_xor().literals(1);
if (num_true_literals % 2 == 0) { // a == not(b).
context_->StoreBooleanEqualityRelation(a, NegatedRef(b));
} else { // a == b.
context_->StoreBooleanEqualityRelation(a, b);
}
context_->UpdateNewConstraintsVariableUsage();
context_->UpdateRuleStats("bool_xor: two active literals");
return RemoveConstraint(ct);
}
if (num_true_literals % 2 == 1) {
CHECK_NE(true_literal, std::numeric_limits<int32_t>::min());
ct->mutable_bool_xor()->set_literals(new_size++, true_literal);
@@ -1658,8 +1688,12 @@ bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) {
"could be improved.";
continue;
}
if (!context_->SubstituteVariableInObjective(var, coeff, *ct)) {
if (context_->ModelIsUnsat()) return true;
continue;
}
context_->UpdateRuleStats("linear: singleton column define objective.");
context_->SubstituteVariableInObjective(var, coeff, *ct);
context_->MarkVariableAsRemoved(var);
*(context_->mapping_model->add_constraints()) = *ct;
return RemoveConstraint(ct);
@@ -1668,7 +1702,10 @@ bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) {
// Update the objective and remove the variable from its equality
// constraint by expanding its rhs. This might fail if the new linear
// objective expression can lead to overflow.
if (!context_->SubstituteVariableInObjective(var, coeff, *ct)) continue;
if (!context_->SubstituteVariableInObjective(var, coeff, *ct)) {
if (context_->ModelIsUnsat()) return true;
continue;
}
context_->UpdateRuleStats(
"linear: singleton column in equality and in objective.");
@@ -1779,7 +1816,9 @@ bool CpModelPresolver::PresolveSmallLinear(ConstraintProto* ct) {
if (linear.domain_size() == 2 && linear.domain(0) == linear.domain(1)) {
const int64_t value = RefIsPositive(ref) ? linear.domain(0) * coeff
: -linear.domain(0) * coeff;
if (context_->StoreLiteralImpliesVarEqValue(literal, var, value)) {
if (!context_->DomainOf(var).Contains(value)) {
if (!context_->SetLiteralToFalse(literal)) return false;
} else if (context_->StoreLiteralImpliesVarEqValue(literal, var, value)) {
// The domain is not actually modified, but we want to rescan the
// constraints linked to this variable. See TODO below.
context_->modified_domains.Set(var);
@@ -2659,6 +2698,16 @@ void CpModelPresolver::AddLinearConstraintFromInterval(
new_ct->mutable_linear()->add_vars(end);
new_ct->mutable_linear()->add_coeffs(-1);
CanonicalizeLinear(new_ct);
if (context_->MinOf(size) < 0) {
CHECK(!ct.enforcement_literal().empty());
ConstraintProto* positive = context_->working_model->add_constraints();
*(positive->mutable_enforcement_literal()) = ct.enforcement_literal();
positive->mutable_linear()->add_domain(0);
positive->mutable_linear()->add_domain(context_->MaxOf(size));
positive->mutable_linear()->add_vars(size);
positive->mutable_linear()->add_coeffs(1);
}
context_->UpdateNewConstraintsVariableUsage();
}
@@ -3300,12 +3349,29 @@ bool CpModelPresolver::PresolveAllDiff(ConstraintProto* ct) {
}
}
std::sort(new_variables.begin(), new_variables.end());
std::sort(new_variables.begin(), new_variables.end(),
[](int ref_a, int ref_b) {
const int var_a = PositiveRef(ref_a);
const int var_b = PositiveRef(ref_b);
return std::tie(var_a, ref_a) < std::tie(var_b, ref_b);
});
for (int i = 1; i < new_variables.size(); ++i) {
if (new_variables[i] == new_variables[i - 1]) {
return context_->NotifyThatModelIsUnsat(
"Duplicate variable in all_diff");
}
if (new_variables[i] == NegatedRef(new_variables[i - 1])) {
bool domain_modified = false;
if (!context_->IntersectDomainWith(PositiveRef(new_variables[i]),
Domain(0).Complement(),
&domain_modified)) {
return false;
}
if (domain_modified) {
context_->UpdateRuleStats(
"all_diff: remove 0 from variable appearing with its opposite.");
}
}
}
if (new_variables.size() < all_diff.vars_size()) {
@@ -4123,6 +4189,7 @@ bool CpModelPresolver::PresolveRoutes(ConstraintProto* ct) {
if (HasEnforcementLiteral(*ct)) return false;
RoutesConstraintProto& proto = *ct->mutable_routes();
const int old_size = proto.literals_size();
int new_size = 0;
std::vector<bool> has_incoming_or_outgoing_arcs;
const int num_arcs = proto.literals_size();
@@ -4147,6 +4214,15 @@ bool CpModelPresolver::PresolveRoutes(ConstraintProto* ct) {
has_incoming_or_outgoing_arcs[tail] = true;
has_incoming_or_outgoing_arcs[head] = true;
}
if (old_size > 0 && new_size == 0) {
// A routes constraint cannot have a self loop on 0. Therefore, if there
// were arcs, it means it contains non zero nodes. Without arc, the
// constraint is unfeasible.
return context_->NotifyThatModelIsUnsat(
"routes: graph with nodes and no arcs");
}
if (new_size < num_arcs) {
proto.mutable_literals()->Truncate(new_size);
proto.mutable_tails()->Truncate(new_size);
@@ -4690,6 +4766,8 @@ void CpModelPresolver::ExtractBoolAnd() {
}
}
// TODO(user): It might make sense to run this in parallel. The same apply for
// other expansive and self-contains steps like symmetry detection, etc...
void CpModelPresolver::Probe() {
if (context_->ModelIsUnsat()) return;
@@ -4977,7 +5055,7 @@ void CpModelPresolver::PresolvePureSatPart() {
void CpModelPresolver::ExpandObjective() {
if (context_->ModelIsUnsat()) return;
// The objective is already loaded in the constext, but we re-canonicalize
// The objective is already loaded in the context, but we re-canonicalize
// it with the latest information.
if (!context_->CanonicalizeObjective()) {
(void)context_->NotifyThatModelIsUnsat();
@@ -5120,16 +5198,19 @@ void CpModelPresolver::ExpandObjective() {
}
if (expanded_linear_index != -1) {
context_->UpdateRuleStats("objective: expanded objective constraint.");
// Update the objective map. Note that the division is possible because
// currently we only expand with coeff with a magnitude of 1.
CHECK_EQ(std::abs(objective_coeff_in_expanded_constraint), 1);
const ConstraintProto& ct =
context_->working_model->constraints(expanded_linear_index);
context_->SubstituteVariableInObjective(
objective_var, objective_coeff_in_expanded_constraint, ct,
&new_vars_in_objective);
if (!context_->SubstituteVariableInObjective(
objective_var, objective_coeff_in_expanded_constraint, ct,
&new_vars_in_objective)) {
if (context_->ModelIsUnsat()) return;
continue;
}
context_->UpdateRuleStats("objective: expanded objective constraint.");
// Add not yet processed new variables.
for (const int var : new_vars_in_objective) {
@@ -5426,13 +5507,13 @@ bool CpModelPresolver::PresolveOneConstraint(int c) {
// PropagateDomainsInLinear().
//
// TODO(user): The move in only one direction code is redundant with the
// dual bound strengthening code. So maybe we don't need both. Especially
// since the implementation here is a bit hacky.
// dual bound strengthening code. So maybe we don't need both.
for (const int ref : ct->linear().vars()) {
const int var = PositiveRef(ref);
context_->var_to_lb_only_constraints[var].erase(c);
context_->var_to_ub_only_constraints[var].erase(c);
}
if (CanonicalizeLinear(ct)) {
context_->UpdateConstraintVariableUsage(c);
}
@@ -5458,7 +5539,7 @@ bool CpModelPresolver::PresolveOneConstraint(int c) {
if (PresolveLinearOnBooleans(ct)) {
context_->UpdateConstraintVariableUsage(c);
}
if (ct->constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
if (ct->constraint_case() == ConstraintProto::kLinear) {
const int old_num_enforcement_literals = ct->enforcement_literal_size();
ExtractEnforcementLiteralFromLinearConstraint(c, ct);
if (ct->constraint_case() ==
@@ -7202,7 +7283,7 @@ std::vector<std::pair<int, int>> FindDuplicateConstraints(
// We use a map hash: serialized_constraint_proto hash -> constraint index.
ConstraintProto copy;
absl::flat_hash_map<int64_t, int> equiv_constraints;
absl::flat_hash_map<uint64_t, int> equiv_constraints;
std::string s;
const int num_constraints = model_proto.constraints().size();
@@ -7218,7 +7299,7 @@ std::vector<std::pair<int, int>> FindDuplicateConstraints(
copy = CopyConstraintForDuplicateDetection(model_proto.constraints(c));
s = copy.SerializeAsString();
const int64_t hash = absl::Hash<std::string>()(s);
const uint64_t hash = absl::Hash<std::string>()(s);
const auto [it, inserted] = equiv_constraints.insert({hash, c});
if (!inserted) {
// Already present!

18
ortools/sat/cp_model_solver.cc
View File

@@ -103,12 +103,12 @@ ABSL_FLAG(bool, cp_model_dump_models, false,
"DEBUG ONLY. When set to true, SolveCpModel() will dump its model "
"protos (original model, presolved model, mapping model) in text "
"format to 'FLAGS_cp_model_dump_prefix'{model|presolved_model|"
"mapping_model}.pbtxt.");
"mapping_model}.pb.txt.");
ABSL_FLAG(bool, cp_model_dump_lns, false,
"DEBUG ONLY. When set to true, solve will dump all "
"lns models proto in text format to "
"'FLAGS_cp_model_dump_prefix'lns_xxx.pbtxt.");
"'FLAGS_cp_model_dump_prefix'lns_xxx.pb.txt.");
ABSL_FLAG(
bool, cp_model_dump_problematic_lns, false,
@@ -118,7 +118,7 @@ ABSL_FLAG(
ABSL_FLAG(bool, cp_model_dump_response, false,
"DEBUG ONLY. If true, the final response of each solve will be "
"dumped to 'FLAGS_cp_model_dump_prefix'response.pbtxt");
"dumped to 'FLAGS_cp_model_dump_prefix'response.pb.txt");
ABSL_FLAG(std::string, cp_model_params, "",
"This is interpreted as a text SatParameters proto. The "
@@ -2449,7 +2449,7 @@ class LnsSolver : public SubSolver {
// TODO(user): export the delta too if needed.
const std::string lns_name =
absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix),
lns_fragment.name(), ".pbtxt");
lns_fragment.name(), ".pb.txt");
LOG(INFO) << "Dumping LNS model to '" << lns_name << "'.";
CHECK_OK(file::SetTextProto(lns_name, lns_fragment, file::Defaults()));
}
@@ -2551,7 +2551,7 @@ class LnsSolver : public SubSolver {
if (absl::GetFlag(FLAGS_cp_model_dump_problematic_lns)) {
const std::string name =
absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix),
debug_copy.name(), ".pbtxt");
debug_copy.name(), ".pb.txt");
LOG(INFO) << "Dumping problematic LNS model to '" << name << "'.";
CHECK_OK(file::SetTextProto(name, debug_copy, file::Defaults()));
}
@@ -2907,7 +2907,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
// Dump initial model?
if (absl::GetFlag(FLAGS_cp_model_dump_models)) {
const std::string file =
absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix), "model.pbtxt");
absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix), "model.pb.txt");
LOG(INFO) << "Dumping cp model proto to '" << file << "'.";
CHECK_OK(file::SetTextProto(file, model_proto, file::Defaults()));
}
@@ -3143,7 +3143,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
for (int i = 0; i < model_proto.solution_hint().vars_size(); ++i) {
const int ref = model_proto.solution_hint().vars(i);
const int64_t value = model_proto.solution_hint().values(i);
solution[PositiveRef(ref)] = RefIsPositive(ref) ? value : CapOpp(value);
solution[PositiveRef(ref)] = RefIsPositive(ref) ? value : -value;
}
if (SolutionIsFeasible(model_proto, solution)) {
SOLVER_LOG(context->logger(),
@@ -3293,14 +3293,14 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
#if !defined(__PORTABLE_PLATFORM__)
if (absl::GetFlag(FLAGS_cp_model_dump_models)) {
const std::string presolved_file = absl::StrCat(
absl::GetFlag(FLAGS_cp_model_dump_prefix), "presolved_model.pbtxt");
absl::GetFlag(FLAGS_cp_model_dump_prefix), "presolved_model.pb.txt");
LOG(INFO) << "Dumping presolved cp model proto to '" << presolved_file
<< "'.";
CHECK_OK(file::SetTextProto(presolved_file, new_cp_model_proto,
file::Defaults()));
const std::string mapping_file = absl::StrCat(
absl::GetFlag(FLAGS_cp_model_dump_prefix), "mapping_model.pbtxt");
absl::GetFlag(FLAGS_cp_model_dump_prefix), "mapping_model.pb.txt");
LOG(INFO) << "Dumping mapping cp model proto to '" << mapping_file << "'.";
CHECK_OK(file::SetTextProto(mapping_file, mapping_proto, file::Defaults()));
}

15
ortools/sat/presolve_context.cc
View File

@@ -1127,10 +1127,14 @@ void PresolveContext::CanonicalizeDomainOfSizeTwo(int var) {
void PresolveContext::InsertVarValueEncodingInternal(int literal, int var,
int64_t value,
bool add_constraints) {
CHECK(RefIsPositive(var));
CHECK(!VariableWasRemoved(literal));
CHECK(!VariableWasRemoved(var));
absl::flat_hash_map<int64_t, SavedLiteral>& var_map = encoding_[var];
// The code below is not 100% correct if this is not the case.
DCHECK(DomainOf(var).Contains(value));
// Ticky and rare: I have only observed this on the LNS of
// radiation_m18_12_05_sat.fzn. The value was encoded, but maybe we never
// used the involved variables / constraints, so it was removed (with the
@@ -1159,6 +1163,8 @@ void PresolveContext::InsertVarValueEncodingInternal(int literal, int var,
}
if (DomainOf(var).Size() == 2) {
// TODO(user): There is a bug here if the var == value was not in the
// domain, it will just be ignored.
CanonicalizeDomainOfSizeTwo(var);
} else {
VLOG(2) << "Insert lit(" << literal << ") <=> var(" << var
@@ -1213,12 +1219,15 @@ bool PresolveContext::CanonicalizeEncoding(int* ref, int64_t* value) {
return true;
}
void PresolveContext::InsertVarValueEncoding(int literal, int ref,
bool PresolveContext::InsertVarValueEncoding(int literal, int ref,
int64_t value) {
if (!RemapEncodingMaps()) return;
if (!CanonicalizeEncoding(&ref, &value)) return;
if (!RemapEncodingMaps()) return false;
if (!CanonicalizeEncoding(&ref, &value)) {
return SetLiteralToFalse(literal);
}
literal = GetLiteralRepresentative(literal);
InsertVarValueEncodingInternal(literal, ref, value, /*add_constraints=*/true);
return true;
}
bool PresolveContext::StoreLiteralImpliesVarEqValue(int literal, int var,

18
ortools/sat/presolve_context.h
View File

@@ -70,8 +70,7 @@ class SavedVariable {
// in-memory domain of each variables and the constraint variable graph.
class PresolveContext {
public:
explicit PresolveContext(Model* model, CpModelProto* cp_model,
CpModelProto* mapping)
PresolveContext(Model* model, CpModelProto* cp_model, CpModelProto* mapping)
: working_model(cp_model),
mapping_model(mapping),
logger_(model->GetOrCreate<SolverLogger>()),
@@ -80,6 +79,9 @@ class PresolveContext {
random_(model->GetOrCreate<ModelRandomGenerator>()) {}
// Helpers to adds new variables to the presolved model.
//
// TODO(user): We should control more how this is called so we can update
// a solution hint accordingly.
int NewIntVar(const Domain& domain);
int NewBoolVar();
int GetOrCreateConstantVar(int64_t cst);
@@ -269,7 +271,13 @@ class PresolveContext {
// Important: This does not update the constraint<->variable graph, so
// ConstraintVariableGraphIsUpToDate() will be false until
// UpdateNewConstraintsVariableUsage() is called.
void InsertVarValueEncoding(int literal, int ref, int64_t value);
//
// Returns false if the model become UNSAT.
//
// TODO(user): This function is not always correct if
// !context->DomainOf(ref).contains(value), we could make it correct but it
// might be a bit expansive to do so. For now we just have a DCHECK().
bool InsertVarValueEncoding(int literal, int ref, int64_t value);
// Gets the associated literal if it is already created. Otherwise
// create it, add the corresponding constraints and returns it.
@@ -337,7 +345,7 @@ class PresolveContext {
// satisfy our overflow preconditions. Note that this can only happen if the
// substitued variable is not implied free (i.e. if its domain is smaller than
// the implied domain from the equality).
bool SubstituteVariableInObjective(
ABSL_MUST_USE_RESULT bool SubstituteVariableInObjective(
int var_in_equality, int64_t coeff_in_equality,
const ConstraintProto& equality,
std::vector<int>* new_vars_in_objective = nullptr);
@@ -476,7 +484,7 @@ class PresolveContext {
// Makes sure we only insert encoding about the current representative.
//
// Returns false if ref cannot take the given value (it might not have been
// propagated yed).
// propagated yet).
bool CanonicalizeEncoding(int* ref, int64_t* value);
// Inserts an half reified var value encoding (literal => var ==/!= value).

14
ortools/sat/sat_parameters.proto
View File

@@ -842,12 +842,12 @@ message SatParameters {
optional bool optimize_with_max_hs = 85 [default = false];
// Whether we enumerate all solutions of a problem without objective. Note
// that setting this to true automatically disable the presolve. This is
// because the presolve rules only guarantee the existence of one feasible
// solution to the presolved problem.
// that setting this to true automatically disable some presolve reduction
// that can remove feasible solution. That is it has the same effect as
// setting keep_all_feasible_solutions_in_presolve.
//
// TODO(user): Do not disable the presolve and let the user choose what
// behavior is best by setting keep_all_feasible_solutions_in_presolve.
// TODO(user): Do not do that and let the user choose what behavior is best by
// setting keep_all_feasible_solutions_in_presolve ?
optional bool enumerate_all_solutions = 87 [default = false];
// If true, we disable the presolve reductions that remove feasible solutions
@@ -868,7 +868,9 @@ message SatParameters {
optional bool fill_tightened_domains_in_response = 132 [default = false];
// If true, the solver will add a default integer branching strategy to the
// already defined search strategy.
// already defined search strategy. If not, some variable might still not be
// fixed at the end of the search. For now we assume these variable can just
// be set to their lower bound.
optional bool instantiate_all_variables = 106 [default = true];
// If true, then the precedences propagator try to detect for each variable if

2
ortools/sat/synchronization.cc
View File

@@ -534,7 +534,7 @@ void SharedResponseManager::NewSolution(const CpSolverResponse& response,
// another solution manager, and we do not want to dump those.
if (absl::GetFlag(FLAGS_cp_model_dump_solutions)) {
const std::string file =
absl::StrCat(dump_prefix_, "solution_", num_solutions_, ".pbtxt");
absl::StrCat(dump_prefix_, "solution_", num_solutions_, ".pb.txt");
LOG(INFO) << "Dumping solution to '" << file << "'.";
CHECK_OK(file::SetTextProto(file, best_response_, file::Defaults()));
}

4
ortools/sat/synchronization.h
View File

@@ -59,7 +59,7 @@ class SharedSolutionRepository {
// this rank is actually the unscaled internal minimization objective.
// Remove this assumptions by simply recomputing this value since it is not
// too costly to do so.
int64_t rank;
int64_t rank = 0;
std::vector<ValueType> variable_values;
@@ -536,7 +536,7 @@ void SharedSolutionRepository<ValueType>::Synchronize() {
// We use a stable sort to keep the num_selected count for the already
// existing solutions.
//
// TODO(user): Intoduce a notion of orthogonality to diversify the pool?
// TODO(user): Introduce a notion of orthogonality to diversify the pool?
gtl::STLStableSortAndRemoveDuplicates(&solutions_);
if (solutions_.size() > num_solutions_to_keep_) {
solutions_.resize(num_solutions_to_keep_);