Skip to content

Commit

Permalink
[CP-SAT] fix presolve bug; fix callback bug
Browse files Browse the repository at this point in the history
  • Loading branch information
@lperron
lperron committed Sep 23, 2024
1 parent f3f8830 commit f053be9
Show file tree
Hide file tree
Showing 10 changed files with 385 additions and 91 deletions.
1 change: 1 addition & 0 deletions ortools/sat/BUILD.bazel
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3004,6 +3004,7 @@ cc_library(
":cp_model_utils",
":model",
":sat_parameters_cc_proto",
":util",
"//ortools/util:logging",
"//ortools/util:sorted_interval_list",
"//ortools/util:time_limit",
Expand Down
7 changes: 7 additions & 0 deletions ortools/sat/cp_model_mapping.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -172,6 +172,13 @@ class CpModelMapping {
return reverse_integer_map_[var];
}

// This one should only be used when we have a mapping.
int GetProtoLiteralFromLiteral(sat::Literal lit) const {
const int proto_var = GetProtoVariableFromBooleanVariable(lit.Variable());
DCHECK_NE(proto_var, -1);
return lit.IsPositive() ? proto_var : NegatedRef(proto_var);
}

const std::vector<IntegerVariable>& GetVariableMapping() const {
return integers_;
}
Expand Down
168 changes: 113 additions & 55 deletions ortools/sat/cp_model_presolve.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2508,7 +2508,7 @@ bool CpModelPresolver::PresolveLinearOfSizeOne(ConstraintProto* ct) {
context_->UpdateRuleStats("linear1: infeasible");
return MarkConstraintAsFalse(ct);
}
if (rhs == context_->DomainOf(var)) {
if (rhs == var_domain) {
context_->UpdateRuleStats("linear1: always true");
return RemoveConstraint(ct);
}
Expand Down Expand Up @@ -2544,16 +2544,28 @@ bool CpModelPresolver::PresolveLinearOfSizeOne(ConstraintProto* ct) {
}

// Detect encoding.
bool changed = false;
if (ct->enforcement_literal().size() == 1) {
// If we already have an encoding literal, this constraint is really
// an implication.
const int lit = ct->enforcement_literal(0);
int lit = ct->enforcement_literal(0);

// For correctness below, it is important lit is the canonical literal,
// otherwise we might remove the constraint even though it is the one
// defining an encoding literal.
const int representative = context_->GetLiteralRepresentative(lit);
if (lit != representative) {
lit = representative;
ct->set_enforcement_literal(0, lit);
context_->UpdateRuleStats("linear1: remapped enforcement literal");
changed = true;
}

if (rhs.IsFixed()) {
const int64_t value = rhs.FixedValue();
int encoding_lit;
if (context_->HasVarValueEncoding(var, value, &encoding_lit)) {
if (lit == encoding_lit) return false;
if (lit == encoding_lit) return changed;
context_->AddImplication(lit, encoding_lit);
context_->UpdateNewConstraintsVariableUsage();
ct->Clear();
Expand All @@ -2567,15 +2579,15 @@ bool CpModelPresolver::PresolveLinearOfSizeOne(ConstraintProto* ct) {
}
context_->UpdateNewConstraintsVariableUsage();
}
return false;
return changed;
}

const Domain complement = rhs.Complement().IntersectionWith(var_domain);
if (complement.IsFixed()) {
const int64_t value = complement.FixedValue();
int encoding_lit;
if (context_->HasVarValueEncoding(var, value, &encoding_lit)) {
if (NegatedRef(lit) == encoding_lit) return false;
if (NegatedRef(lit) == encoding_lit) return changed;
context_->AddImplication(lit, NegatedRef(encoding_lit));
context_->UpdateNewConstraintsVariableUsage();
ct->Clear();
Expand All @@ -2589,11 +2601,11 @@ bool CpModelPresolver::PresolveLinearOfSizeOne(ConstraintProto* ct) {
}
context_->UpdateNewConstraintsVariableUsage();
}
return false;
return changed;
}
}

return false;
return changed;
}

bool CpModelPresolver::PresolveLinearOfSizeTwo(ConstraintProto* ct) {
Expand Down Expand Up @@ -7110,9 +7122,6 @@ void CpModelPresolver::Probe() {
}
probing_timer->AddCounter("fixed_bools", num_fixed);

DetectDuplicateConstraintsWithDifferentEnforcements(
mapping, implication_graph, model.GetOrCreate<Trail>());

int num_equiv = 0;
int num_changed_bounds = 0;
const int num_variables = context_->working_model->variables().size();
Expand Down Expand Up @@ -7148,6 +7157,12 @@ void CpModelPresolver::Probe() {
probing_timer->AddCounter("new_binary_clauses",
prober->num_new_binary_clauses());

// Note that we prefer to run this after we exported all equivalence to the
// context, so that our enforcement list can be presolved to the best of our
// knowledge.
DetectDuplicateConstraintsWithDifferentEnforcements(
mapping, implication_graph, model.GetOrCreate<Trail>());

// Stop probing timer now and display info.
probing_timer.reset();

Expand Down Expand Up @@ -8888,37 +8903,20 @@ void CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements(
for (const auto& [dup, rep] : duplicates_without_enforcement) {
auto* dup_ct = context_->working_model->mutable_constraints(dup);
auto* rep_ct = context_->working_model->mutable_constraints(rep);
if (rep_ct->constraint_case() == ConstraintProto::CONSTRAINT_NOT_SET) {
continue;

// Make sure our enforcement list are up to date: nothing fixed and that
// its uses the literal representatives.
if (PresolveEnforcementLiteral(dup_ct)) {
context_->UpdateConstraintVariableUsage(dup);
}
if (PresolveEnforcementLiteral(rep_ct)) {
context_->UpdateConstraintVariableUsage(rep);
}

// If we have a trail, we can check if any variable of the enforcement is
// fixed to false. This is useful for what follows since calling
// implication_graph->DirectImplications() is invalid for fixed variables.
if (trail != nullptr) {
bool found_false_enforcement = false;
for (const int c : {dup, rep}) {
for (const int l :
context_->working_model->constraints(c).enforcement_literal()) {
if (trail->Assignment().LiteralIsFalse(mapping->Literal(l))) {
found_false_enforcement = true;
break;
}
}
if (found_false_enforcement) {
context_->UpdateRuleStats("enforcement: false literal");
if (c == rep) {
rep_ct->Swap(dup_ct);
context_->UpdateConstraintVariableUsage(rep);
}
dup_ct->Clear();
context_->UpdateConstraintVariableUsage(dup);
break;
}
}
if (found_false_enforcement) {
continue;
}
// Skip this pair if one of the constraint was simplified
if (rep_ct->constraint_case() == ConstraintProto::CONSTRAINT_NOT_SET ||
dup_ct->constraint_case() == ConstraintProto::CONSTRAINT_NOT_SET) {
continue;
}

// If one of them has no enforcement, then the other can be ignored.
Expand All @@ -8936,10 +8934,7 @@ void CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements(
// Special case. This looks specific but users might reify with a cost
// a duplicate constraint. In this case, no need to have two variables,
// we can make them equal by duality argument.
const int a = rep_ct->enforcement_literal(0);
const int b = dup_ct->enforcement_literal(0);
if (context_->IsFixed(a) || context_->IsFixed(b)) continue;

//
// TODO(user): Deal with more general situation? Note that we already
// do something similar in dual_bound_strengthening.Strengthen() were we
// are more general as we just require an unique blocking constraint rather
Expand All @@ -8949,6 +8944,8 @@ void CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements(
// we can also add the equality. Alternatively, we can just introduce a new
// variable and merge all duplicate constraint into 1 + bunch of boolean
// constraints liking enforcements.
const int a = rep_ct->enforcement_literal(0);
const int b = dup_ct->enforcement_literal(0);
if (context_->VariableWithCostIsUniqueAndRemovable(a) &&
context_->VariableWithCostIsUniqueAndRemovable(b)) {
// Both these case should be presolved before, but it is easy to deal with
Expand Down Expand Up @@ -9007,19 +9004,19 @@ void CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements(
// B, then constraint A is redundant and we can remove it.
const int c_a = i == 0 ? dup : rep;
const int c_b = i == 0 ? rep : dup;
const auto& ct_a = context_->working_model->constraints(c_a);
const auto& ct_b = context_->working_model->constraints(c_b);

enforcement_vars.clear();
implications_used.clear();
for (const int proto_lit :
context_->working_model->constraints(c_b).enforcement_literal()) {
for (const int proto_lit : ct_b.enforcement_literal()) {
const Literal lit = mapping->Literal(proto_lit);
if (trail->Assignment().LiteralIsTrue(lit)) continue;
DCHECK(!trail->Assignment().LiteralIsAssigned(lit));
enforcement_vars.insert(lit);
}
for (const int proto_lit :
context_->working_model->constraints(c_a).enforcement_literal()) {
for (const int proto_lit : ct_a.enforcement_literal()) {
const Literal lit = mapping->Literal(proto_lit);
if (trail->Assignment().LiteralIsTrue(lit)) continue;
DCHECK(!trail->Assignment().LiteralIsAssigned(lit));
for (const Literal implication_lit :
implication_graph->DirectImplications(lit)) {
auto extracted = enforcement_vars.extract(implication_lit);
Expand All @@ -9029,6 +9026,71 @@ void CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements(
}
}
if (enforcement_vars.empty()) {
// Tricky: Because we keep track of literal <=> var == value, we
// cannot easily simplify linear1 here. This is because a scenario
// like this can happen:
//
// We have registered the fact that a <=> X=1 because we saw two
// constraints a => X=1 and not(a) => X!= 1
//
// Now, we are here and we have:
// a => X=1, b => X=1, a => b
// So we rewrite this as
// a => b, b => X=1
//
// But later, the PresolveLinearOfSizeOne() see
// b => X=1 and just rewrite this as b => a since (a <=> X=1).
// This is wrong because the constraint "b => X=1" is needed for the
// equivalence (a <=> X=1), but we lost that fact.
//
// Note(user): In the scenario above we can see that a <=> b, and if
// we know that fact, then the transformation is correctly handled.
// The bug was triggered when the Probing finished early due to time
// limit and we never detected that equivalence.
//
// TODO(user): Try to find a cleaner way to handle this. We could
// query our HasVarValueEncoding() directly here and directly detect a
// <=> b. However we also need to figure the case of
// half-implications.
{
if (ct_a.constraint_case() == ConstraintProto::kLinear &&
ct_a.linear().vars().size() == 1 &&
ct_a.enforcement_literal().size() == 1) {
const int var = ct_a.linear().vars(0);
const Domain var_domain = context_->DomainOf(var);
const Domain rhs =
ReadDomainFromProto(ct_a.linear())
.InverseMultiplicationBy(ct_a.linear().coeffs(0))
.IntersectionWith(var_domain);

// IsFixed() do not work on empty domain.
if (rhs.IsEmpty()) {
context_->UpdateRuleStats("duplicate: linear1 infeasible");
if (!MarkConstraintAsFalse(rep_ct)) return;
if (!MarkConstraintAsFalse(dup_ct)) return;
context_->UpdateConstraintVariableUsage(rep);
context_->UpdateConstraintVariableUsage(dup);
continue;
}
if (rhs == var_domain) {
context_->UpdateRuleStats("duplicate: linear1 always true");
rep_ct->Clear();
dup_ct->Clear();
context_->UpdateConstraintVariableUsage(rep);
context_->UpdateConstraintVariableUsage(dup);
continue;
}

// We skip if it is a var == value or var != value constraint.
if (rhs.IsFixed() ||
rhs.Complement().IntersectionWith(var_domain).IsFixed()) {
context_->UpdateRuleStats(
"TODO duplicate: skipped identical encoding constraints");
continue;
}
}
}

context_->UpdateRuleStats(
"duplicate: identical constraint with implied enforcements");
if (c_a == rep) {
Expand All @@ -9043,12 +9105,8 @@ void CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements(
// graph. This is because in some case the implications are only true
// in the presence of the "duplicated" constraints.
for (const auto& [a, b] : implications_used) {
const int var_a =
mapping->GetProtoVariableFromBooleanVariable(a.Variable());
const int proto_lit_a = a.IsPositive() ? var_a : NegatedRef(var_a);
const int var_b =
mapping->GetProtoVariableFromBooleanVariable(b.Variable());
const int proto_lit_b = b.IsPositive() ? var_b : NegatedRef(var_b);
const int proto_lit_a = mapping->GetProtoLiteralFromLiteral(a);
const int proto_lit_b = mapping->GetProtoLiteralFromLiteral(b);
context_->AddImplication(proto_lit_a, proto_lit_b);
}
context_->UpdateNewConstraintsVariableUsage();
Expand Down
1 change: 1 addition & 0 deletions ortools/sat/feasibility_jump_test.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@

#include "ortools/sat/feasibility_jump.h"

#include <cstdint>
#include <utility>

#include "gtest/gtest.h"
Expand Down
7 changes: 4 additions & 3 deletions ortools/sat/feasibility_pump.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/sat/sat_solver.h"
#include "ortools/sat/synchronization.h"
#include "ortools/sat/util.h"
#include "ortools/util/saturated_arithmetic.h"
#include "ortools/util/sorted_interval_list.h"
#include "ortools/util/strong_integers.h"
Expand Down Expand Up @@ -610,11 +611,11 @@ bool FeasibilityPump::PropagationRounding() {
}

const int64_t rounded_value =
static_cast<int64_t>(std::round(lp_solution_[var_index]));
SafeDoubleToInt64(std::round(lp_solution_[var_index]));
const int64_t floor_value =
static_cast<int64_t>(std::floor(lp_solution_[var_index]));
SafeDoubleToInt64(std::floor(lp_solution_[var_index]));
const int64_t ceil_value =
static_cast<int64_t>(std::ceil(lp_solution_[var_index]));
SafeDoubleToInt64(std::ceil(lp_solution_[var_index]));

const bool floor_is_in_domain =
(domain.Contains(floor_value) && lb.value() <= floor_value);
Expand Down
Loading

1 comment on commit f053be9

@Mizux
Copy link
Collaborator

@Mizux Mizux commented on f053be9 Sep 24, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

should Fix:

Please sign in to comment.