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

[CP-SAT] more bug fixes; more moving of hint management to solution_crush

Browse Source
This commit is contained in:
Laurent Perron
2025-01-22 14:36:02 +01:00
parent 52a91707f6
commit eee2f106cd
10 changed files with 399 additions and 401 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
ortools/sat/BUILD.bazel
View File

@@ -835,9 +835,12 @@ cc_library(
":cp_model_cc_proto",
":cp_model_utils",
":sat_parameters_cc_proto",
":symmetry_util",
"//ortools/algorithms:sparse_permutation",
"//ortools/util:sorted_interval_list",
"@com_google_absl//absl/container:flat_hash_map",
"@com_google_absl//absl/container:inlined_vector",
"@com_google_absl//absl/log",
"@com_google_absl//absl/log:check",
"@com_google_absl//absl/types:span",
],

5
ortools/sat/cp_model.proto
View File

@@ -160,8 +160,9 @@ message NoOverlap2DConstraintProto {
// this constraint. Moreover, intervals of size zero are ignored.
//
// All demands must not contain any negative value in their domains. This is
// checked at validation. The capacity can currently contains negative values,
// but it will be propagated to >= 0 right away.
// checked at validation. Even if there are no intervals, this constraint
// implicit enforces capacity >= 0. In other words, a negative capacity is
// considered valid but always infeasible.
message CumulativeConstraintProto {
LinearExpressionProto capacity = 1;
repeated int32 intervals = 2;

33
ortools/sat/cp_model_checker.cc
View File

@@ -423,6 +423,20 @@ std::string ValidateIntDivConstraint(const CpModelProto& model,
return "";
}
void AppendToOverflowValidator(const LinearExpressionProto& input,
LinearExpressionProto* output,
int64_t prod = 1) {
output->mutable_vars()->Add(input.vars().begin(), input.vars().end());
for (const int64_t coeff : input.coeffs()) {
output->add_coeffs(coeff * prod);
}
// We add the absolute value to be sure that future computation will not
// overflow depending on the order they are performed in.
output->set_offset(
CapAdd(std::abs(output->offset()), std::abs(input.offset())));
}
std::string ValidateElementConstraint(const CpModelProto& model,
const ConstraintProto& ct) {
const ElementConstraintProto& element = ct.element();
@@ -484,10 +498,7 @@ std::string ValidateElementConstraint(const CpModelProto& model,
for (const LinearExpressionProto& expr : element.exprs()) {
RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, expr));
LinearExpressionProto overflow_detection = ct.element().linear_target();
for (int i = 0; i < expr.vars_size(); ++i) {
overflow_detection.add_vars(expr.vars(i));
overflow_detection.add_coeffs(-expr.coeffs(i));
}
AppendToOverflowValidator(expr, &overflow_detection, -1);
overflow_detection.set_offset(overflow_detection.offset() -
expr.offset());
if (PossibleIntegerOverflow(model, overflow_detection.vars(),
@@ -647,17 +658,6 @@ std::string ValidateRoutesConstraint(const ConstraintProto& ct) {
return ValidateGraphInput(/*is_route=*/true, ct.routes());
}
void AppendToOverflowValidator(const LinearExpressionProto& input,
LinearExpressionProto* output) {
output->mutable_vars()->Add(input.vars().begin(), input.vars().end());
output->mutable_coeffs()->Add(input.coeffs().begin(), input.coeffs().end());
// We add the absolute value to be sure that future computation will not
// overflow depending on the order they are performed in.
output->set_offset(
CapAdd(std::abs(output->offset()), std::abs(input.offset())));
}
std::string ValidateIntervalConstraint(const CpModelProto& model,
const ConstraintProto& ct) {
if (ct.enforcement_literal().size() > 1) {
@@ -705,7 +705,7 @@ std::string ValidateIntervalConstraint(const CpModelProto& model,
"variable are currently not supported.";
}
RETURN_IF_NOT_EMPTY(ValidateLinearExpression(model, arg.end()));
AppendToOverflowValidator(arg.end(), &for_overflow_validation);
AppendToOverflowValidator(arg.end(), &for_overflow_validation, -1);
if (PossibleIntegerOverflow(model, for_overflow_validation.vars(),
for_overflow_validation.coeffs(),
@@ -1484,6 +1484,7 @@ class ConstraintChecker {
bool CumulativeConstraintIsFeasible(const CpModelProto& model,
const ConstraintProto& ct) {
const int64_t capacity = LinearExpressionValue(ct.cumulative().capacity());
if (capacity < 0) return false;
const int num_intervals = ct.cumulative().intervals_size();
std::vector<std::pair<int64_t, int64_t>> events;
for (int i = 0; i < num_intervals; ++i) {

257
ortools/sat/cp_model_expand.cc
View File

@@ -337,24 +337,14 @@ void ExpandReservoir(ConstraintProto* reservoir_ct, PresolveContext* context) {
lin->add_coeffs(1);
AddLinearExpressionToLinearConstraint(demand, -1, lin);
context->CanonicalizeLinearConstraint(demand_ct);
context->solution_crush().SetVarToLinearExpressionIf(new_var, demand,
active);
}
// not(active) => new_var == 0.
context->AddImplyInDomain(NegatedRef(active), new_var, Domain(0));
SolutionCrush& crush = context->solution_crush();
if (crush.HintIsLoaded() &&
crush.VarHasSolutionHint(PositiveRef(active))) {
if (crush.LiteralSolutionHint(active)) {
const std::optional<int64_t> demand_hint =
crush.GetExpressionSolutionHint(demand);
if (demand_hint.has_value()) {
crush.SetNewVariableHint(new_var, demand_hint.value());
}
} else {
crush.SetNewVariableHint(new_var, 0);
}
}
context->solution_crush().SetVarToValueIf(new_var, 0,
NegatedRef(active));
}
}
sum->add_domain(reservoir.min_level());
@@ -504,8 +494,8 @@ void ExpandIntMod(ConstraintProto* ct, PresolveContext* context) {
context->UpdateRuleStats("int_mod: expanded");
}
void ExpandNonBinaryIntProd(ConstraintProto* ct, PresolveContext* context) {
CHECK_GT(ct->int_prod().exprs_size(), 2);
void ExpandIntProd(ConstraintProto* ct, PresolveContext* context) {
if (ct->int_prod().exprs_size() <= 2) return;
std::deque<LinearExpressionProto> terms(
{ct->int_prod().exprs().begin(), ct->int_prod().exprs().end()});
std::vector<int> new_vars;
@@ -539,54 +529,6 @@ void ExpandNonBinaryIntProd(ConstraintProto* ct, PresolveContext* context) {
ct->Clear();
}
// TODO(user): Move this into the presolve instead?
void ExpandIntProdWithBoolean(int bool_ref,
const LinearExpressionProto& int_expr,
const LinearExpressionProto& product_expr,
PresolveContext* context) {
ConstraintProto* const one = context->working_model->add_constraints();
one->add_enforcement_literal(bool_ref);
one->mutable_linear()->add_domain(0);
one->mutable_linear()->add_domain(0);
AddLinearExpressionToLinearConstraint(int_expr, 1, one->mutable_linear());
AddLinearExpressionToLinearConstraint(product_expr, -1,
one->mutable_linear());
ConstraintProto* const zero = context->working_model->add_constraints();
zero->add_enforcement_literal(NegatedRef(bool_ref));
zero->mutable_linear()->add_domain(0);
zero->mutable_linear()->add_domain(0);
AddLinearExpressionToLinearConstraint(product_expr, 1,
zero->mutable_linear());
}
void ExpandIntProd(ConstraintProto* ct, PresolveContext* context) {
const LinearArgumentProto& int_prod = ct->int_prod();
if (int_prod.exprs_size() > 2) {
ExpandNonBinaryIntProd(ct, context);
return;
}
if (int_prod.exprs_size() != 2) return;
const LinearExpressionProto& a = int_prod.exprs(0);
const LinearExpressionProto& b = int_prod.exprs(1);
const LinearExpressionProto& p = int_prod.target();
int literal;
const bool a_is_literal = context->ExpressionIsALiteral(a, &literal);
const bool b_is_literal = context->ExpressionIsALiteral(b, &literal);
// We expand if exactly one of {a, b} is a literal. If both are literals, it
// will be presolved into a better version.
if (a_is_literal && !b_is_literal) {
ExpandIntProdWithBoolean(literal, b, p, context);
ct->Clear();
context->UpdateRuleStats("int_prod: expanded product with Boolean var");
} else if (b_is_literal) {
ExpandIntProdWithBoolean(literal, a, p, context);
ct->Clear();
context->UpdateRuleStats("int_prod: expanded product with Boolean var");
}
}
void ExpandInverse(ConstraintProto* ct, PresolveContext* context) {
const auto& f_direct = ct->inverse().f_direct();
const auto& f_inverse = ct->inverse().f_inverse();
@@ -719,47 +661,16 @@ void ExpandLinMax(ConstraintProto* ct, PresolveContext* context) {
// Second, for each expr, create a new boolean bi, and add bi => target <= ai
// With exactly_one(bi)
SolutionCrush& crush = context->solution_crush();
std::vector<bool> enforcement_hints;
if (crush.HintIsLoaded()) {
const std::optional<int64_t> target_hint =
crush.GetExpressionSolutionHint(ct->lin_max().target());
if (target_hint.has_value()) {
int enforcement_hint_sum = 0;
enforcement_hints.reserve(num_exprs);
for (const LinearExpressionProto& expr : ct->lin_max().exprs()) {
const std::optional<int64_t> expr_hint =
crush.GetExpressionSolutionHint(expr);
if (!expr_hint.has_value()) {
enforcement_hints.clear();
break;
}
if (enforcement_hint_sum == 0) {
const bool hint = target_hint.value() <= expr_hint.value();
enforcement_hints.push_back(hint);
enforcement_hint_sum += hint;
} else {
enforcement_hints.push_back(false);
}
}
}
}
std::vector<int> enforcement_literals;
enforcement_literals.reserve(num_exprs);
if (num_exprs == 2) {
const int new_bool = context->NewBoolVar("lin max expansion");
if (!enforcement_hints.empty()) {
crush.SetNewVariableHint(new_bool, enforcement_hints[0]);
}
enforcement_literals.push_back(new_bool);
enforcement_literals.push_back(NegatedRef(new_bool));
} else {
ConstraintProto* exactly_one = context->working_model->add_constraints();
for (int i = 0; i < num_exprs; ++i) {
const int new_bool = context->NewBoolVar("lin max expansion");
if (!enforcement_hints.empty()) {
crush.SetNewVariableHint(new_bool, enforcement_hints[i]);
}
exactly_one->mutable_exactly_one()->add_literals(new_bool);
enforcement_literals.push_back(new_bool);
}
@@ -776,6 +687,8 @@ void ExpandLinMax(ConstraintProto* ct, PresolveContext* context) {
context->CanonicalizeLinearConstraint(new_ct);
}
context->solution_crush().SetLinMaxExpandedVars(ct->lin_max(),
enforcement_literals);
context->UpdateRuleStats("lin_max: expanded lin_max");
ct->Clear();
}
@@ -1023,33 +936,6 @@ void AddImplyInReachableValues(int literal,
}
}
std::vector<int64_t> GetAutomatonStateHints(ConstraintProto* ct,
PresolveContext* context) {
SolutionCrush& crush = context->solution_crush();
if (!crush.HintIsLoaded()) return {};
const AutomatonConstraintProto& proto = ct->automaton();
absl::flat_hash_map<std::pair<int64_t, int64_t>, int64_t> transitions;
for (int i = 0; i < proto.transition_tail_size(); ++i) {
transitions[{proto.transition_tail(i), proto.transition_label(i)}] =
proto.transition_head(i);
}
int64_t current_state = proto.starting_state();
std::vector<int64_t> state_hints;
state_hints.push_back(current_state);
for (int i = 0; i < proto.exprs_size(); ++i) {
const std::optional<int64_t> label_hint =
crush.GetExpressionSolutionHint(proto.exprs(i));
if (!label_hint.has_value()) return {};
const auto it = transitions.find({current_state, label_hint.value()});
if (it == transitions.end()) return {};
current_state = it->second;
state_hints.push_back(current_state);
}
return state_hints;
}
void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
AutomatonConstraintProto& proto = *ct->mutable_automaton();
@@ -1082,12 +968,10 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
absl::flat_hash_map<int64_t, int> in_encoding;
absl::flat_hash_map<int64_t, int> out_encoding;
bool removed_values = false;
SolutionCrush& crush = context->solution_crush();
const std::vector<int64_t> state_hints = GetAutomatonStateHints(ct, context);
DCHECK(state_hints.empty() || state_hints.size() == proto.exprs_size() + 1);
const int n = proto.exprs_size();
std::vector<SolutionCrush::StateVar> new_state_vars;
std::vector<SolutionCrush::TransitionVar> new_transition_vars;
for (int time = 0; time < n; ++time) {
// All these vectors have the same size. We will use them to enforce a
// local table constraint representing one step of the automaton at the
@@ -1184,9 +1068,7 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
out_encoding.clear();
if (states.size() == 2) {
const int var = context->NewBoolVar("automaton expansion");
if (!state_hints.empty()) {
crush.SetNewVariableHint(var, state_hints[time + 1] == states[0]);
}
new_state_vars.push_back({var, time + 1, states[0]});
out_encoding[states[0]] = var;
out_encoding[states[1]] = NegatedRef(var);
} else if (states.size() > 2) {
@@ -1236,10 +1118,7 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
}
out_encoding[state] = context->NewBoolVar("automaton expansion");
if (!state_hints.empty()) {
crush.SetNewVariableHint(out_encoding[state],
state_hints[time + 1] == state);
}
new_state_vars.push_back({out_encoding[state], time + 1, state});
}
}
}
@@ -1300,15 +1179,10 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
//
// TODO(user): Call and use the same heuristics as the table constraint to
// expand this small table with 3 columns (i.e. compress, negate, etc...).
const int64_t label_hint =
crush.GetExpressionSolutionHint(proto.exprs(time)).value_or(0);
std::vector<int> tuple_literals;
if (num_tuples == 2) {
const int bool_var = context->NewBoolVar("automaton expansion");
if (!state_hints.empty()) {
crush.SetNewVariableHint(bool_var, state_hints[time] == in_states[0] &&
label_hint == labels[0]);
}
new_transition_vars.push_back({bool_var, time, in_states[0], labels[0]});
tuple_literals.push_back(bool_var);
tuple_literals.push_back(NegatedRef(bool_var));
} else {
@@ -1327,11 +1201,8 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
tuple_literal = out_encoding[out_states[i]];
} else {
tuple_literal = context->NewBoolVar("automaton expansion");
if (!state_hints.empty()) {
crush.SetNewVariableHint(
tuple_literal,
state_hints[time] == in_states[i] && label_hint == labels[i]);
}
new_transition_vars.push_back(
{tuple_literal, time, in_states[i], labels[i]});
}
tuple_literals.push_back(tuple_literal);
@@ -1353,6 +1224,8 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
out_encoding.clear();
}
context->solution_crush().SetAutomatonExpandedVars(proto, new_state_vars,
new_transition_vars);
if (removed_values) {
context->UpdateRuleStats("automaton: reduced variable domains");
}
@@ -1870,8 +1743,6 @@ void CompressAndExpandPositiveTable(ConstraintProto* ct,
// selected or not. Enforce an exactly one between them.
BoolArgumentProto* exactly_one =
context->working_model->add_constraints()->mutable_exactly_one();
int exactly_one_hint_sum = 0;
SolutionCrush& crush = context->solution_crush();
std::optional<int> table_is_active_literal = std::nullopt;
// Process enforcement literals.
@@ -1890,10 +1761,12 @@ void CompressAndExpandPositiveTable(ConstraintProto* ct,
bool_or->add_literals(NegatedRef(lit));
}
}
std::vector<int> existing_row_literals;
std::vector<SolutionCrush::TableRowLiteral> new_row_literals;
if (table_is_active_literal.has_value()) {
const int inactive_lit = NegatedRef(table_is_active_literal.value());
exactly_one->add_literals(inactive_lit);
exactly_one_hint_sum += crush.LiteralSolutionHintIs(inactive_lit, true);
existing_row_literals.push_back(inactive_lit);
}
int num_reused_variables = 0;
@@ -1914,38 +1787,15 @@ void CompressAndExpandPositiveTable(ConstraintProto* ct,
create_new_var = false;
tuple_literals[i] =
context->GetOrCreateVarValueEncoding(vars[var_index], v);
exactly_one_hint_sum += crush.SolutionHint(vars[var_index]) == v;
existing_row_literals.push_back(tuple_literals[i]);
break;
}
if (create_new_var) {
tuple_literals[i] = context->NewBoolVar("table expansion");
tuples_with_new_variable.push_back(i);
new_row_literals.push_back({tuple_literals[i], compressed_table[i]});
}
exactly_one->add_literals(tuple_literals[i]);
}
// Set the hint of the `tuple_literals` for which new variables were created.
// If the existing `tuple_literals` hints do not sum to 1, set the hint of the
// first tuple which can be selected to true, and the others to false. A tuple
// T can be selected if, for each variable v, the hint of v is in the set of
// values T[v] (an empty set means "any value").
for (const int i : tuples_with_new_variable) {
if (exactly_one_hint_sum >= 1) {
crush.SetNewVariableHint(tuple_literals[i], false);
continue;
}
bool tuple_literal_hint = true;
for (int var_index = 0; var_index < num_vars; ++var_index) {
const auto& values = compressed_table[i][var_index];
if (!values.empty() &&
std::find(values.begin(), values.end(),
crush.SolutionHint(vars[var_index])) == values.end()) {
tuple_literal_hint = false;
break;
}
}
crush.SetNewVariableHint(tuple_literals[i], tuple_literal_hint);
exactly_one_hint_sum += tuple_literal_hint;
}
if (num_reused_variables > 0) {
context->UpdateRuleStats("table: reused literals");
}
@@ -1971,6 +1821,8 @@ void CompressAndExpandPositiveTable(ConstraintProto* ct,
table_is_active_literal, context);
}
context->solution_crush().SetTableExpandedVars(vars, existing_row_literals,
new_row_literals);
context->UpdateRuleStats("table: expanded positive constraint");
}
@@ -2237,37 +2089,6 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
if (ct->linear().domain().size() <= 2) return;
if (ct->linear().vars().size() == 1) return;
// If we have a hint for all variables of this linear constraint, finds in
// which bucket it fall.
int64_t expr_hint = 0;
int hint_bucket = -1;
bool has_complete_hint = false;
SolutionCrush& crush = context->solution_crush();
if (crush.HintIsLoaded()) {
has_complete_hint = true;
const int num_terms = ct->linear().vars().size();
const absl::Span<const int64_t> hint = crush.SolutionHint();
for (int i = 0; i < num_terms; ++i) {
const int var = ct->linear().vars(i);
DCHECK_LT(var, hint.size());
if (!crush.VarHasSolutionHint(var)) {
has_complete_hint = false;
break;
}
expr_hint += ct->linear().coeffs(i) * hint[var];
}
if (has_complete_hint) {
for (int i = 0; i < ct->linear().domain_size(); i += 2) {
const int64_t lb = ct->linear().domain(i);
const int64_t ub = ct->linear().domain(i + 1);
if (expr_hint >= lb && expr_hint <= ub) {
hint_bucket = i;
break;
}
}
}
}
const SatParameters& params = context->params();
if (params.encode_complex_linear_constraint_with_integer()) {
// Integer encoding.
@@ -2276,9 +2097,8 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
// expr \in rhs to expr - slack = 0
const Domain rhs = ReadDomainFromProto(ct->linear());
const int slack = context->NewIntVar(rhs);
if (has_complete_hint) {
crush.SetNewVariableHint(slack, expr_hint);
}
context->solution_crush().SetVarToLinearExpression(
slack, ct->linear().vars(), ct->linear().coeffs());
ct->mutable_linear()->add_vars(slack);
ct->mutable_linear()->add_coeffs(-1);
ct->mutable_linear()->clear_domain();
@@ -2292,9 +2112,6 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
// We cover the special case of no enforcement and two choices by creating
// a single Boolean.
single_bool = context->NewBoolVar("complex linear expansion");
if (has_complete_hint) {
crush.SetNewVariableHint(single_bool, hint_bucket == 0);
}
} else {
clause = context->working_model->add_constraints()->mutable_bool_or();
for (const int ref : ct->enforcement_literal()) {
@@ -2314,9 +2131,6 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
int subdomain_literal;
if (clause != nullptr) {
subdomain_literal = context->NewBoolVar("complex linear expansion");
if (has_complete_hint) {
crush.SetNewVariableHint(subdomain_literal, hint_bucket == i);
}
clause->add_literals(subdomain_literal);
domain_literals.push_back(subdomain_literal);
} else {
@@ -2331,6 +2145,8 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
new_ct->add_enforcement_literal(subdomain_literal);
FillDomainInProto(Domain(lb, ub), new_ct->mutable_linear());
}
context->solution_crush().SetLinearWithComplexDomainExpandedVars(
ct->linear(), domain_literals);
// Make sure all booleans are tights when enumerating all solutions.
if (context->params().enumerate_all_solutions() &&
@@ -2348,21 +2164,8 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
maintain_linear_is_enforced->add_literals(NegatedRef(e_lit));
}
maintain_linear_is_enforced->add_literals(linear_is_enforced);
if (crush.HintIsLoaded()) {
bool has_complete_enforced_hint = true;
bool linear_is_enforced_hint = true;
for (const int e_lit : enforcement_literals) {
if (!crush.VarHasSolutionHint(PositiveRef(e_lit))) {
has_complete_enforced_hint = false;
break;
}
linear_is_enforced_hint &= crush.LiteralSolutionHint(e_lit);
}
if (has_complete_enforced_hint) {
crush.SetNewVariableHint(linear_is_enforced,
linear_is_enforced_hint);
}
}
context->solution_crush().SetVarToConjunction(linear_is_enforced,
enforcement_literals);
}
for (const int lit : domain_literals) {

90
ortools/sat/cp_model_presolve.cc
View File

@@ -505,10 +505,7 @@ bool CpModelPresolver::PresolveBoolAnd(ConstraintProto* ct) {
// hint(enforcement) = 0. But in this case the `enforcement` hint can be
// increased to 1 to preserve the hint feasibility.
const int implied_literal = ct->bool_and().literals(0);
SolutionCrush& crush = context_->solution_crush();
if (crush.LiteralSolutionHintIs(implied_literal, true)) {
crush.UpdateLiteralSolutionHint(enforcement, true);
}
solution_crush_.SetLiteralToValueIf(enforcement, true, implied_literal);
context_->StoreBooleanEqualityRelation(enforcement, implied_literal);
}
}
@@ -2332,10 +2329,8 @@ bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) {
}
continue;
}
SolutionCrush& crush = context_->solution_crush();
crush.UpdateVarSolutionHint(
ct->linear().vars(i),
crush.LiteralSolutionHint(indicator) ? other_value : best_value);
solution_crush_.SetVarToConditionalValue(
ct->linear().vars(i), {indicator}, other_value, best_value);
if (RefIsPositive(indicator)) {
if (!context_->StoreAffineRelation(ct->linear().vars(i), indicator,
other_value - best_value,
@@ -2965,34 +2960,6 @@ bool CpModelPresolver::PresolveSmallLinear(ConstraintProto* ct) {
return false;
}
namespace {
// Set the hint in `context` for the variable in `equality` that has no hint, if
// there is exactly one. Otherwise do nothing.
void MaybeComputeMissingHint(SolutionCrush& crush,
const LinearConstraintProto& equality) {
DCHECK(equality.domain_size() == 2 &&
equality.domain(0) == equality.domain(1));
if (!crush.HintIsLoaded()) return;
int term_with_missing_hint = -1;
int64_t missing_term_value = equality.domain(0);
for (int i = 0; i < equality.vars_size(); ++i) {
if (crush.VarHasSolutionHint(equality.vars(i))) {
missing_term_value -=
crush.SolutionHint(equality.vars(i)) * equality.coeffs(i);
} else if (term_with_missing_hint == -1) {
term_with_missing_hint = i;
} else {
// More than one variable has a missing hint.
return;
}
}
if (term_with_missing_hint == -1) return;
crush.SetNewVariableHint(
equality.vars(term_with_missing_hint),
missing_term_value / equality.coeffs(term_with_missing_hint));
}
} // namespace
bool CpModelPresolver::PresolveDiophantine(ConstraintProto* ct) {
if (ct->constraint_case() != ConstraintProto::kLinear) return false;
if (ct->linear().vars().size() <= 1) return false;
@@ -3120,9 +3087,11 @@ bool CpModelPresolver::PresolveDiophantine(ConstraintProto* ct) {
// and from the hints of `new_variables[k']`, with k' > k.
const int num_constraints = context_->working_model->constraints_size();
for (int i = 0; i < num_replaced_variables; ++i) {
MaybeComputeMissingHint(
context_->solution_crush(),
context_->working_model->constraints(num_constraints - 1 - i).linear());
const LinearConstraintProto& linear =
context_->working_model->constraints(num_constraints - 1 - i).linear();
DCHECK(linear.domain_size() == 2 && linear.domain(0) == linear.domain(1));
solution_crush_.SetVarToLinearConstraintSolution(
std::nullopt, linear.vars(), linear.coeffs(), linear.domain(0));
}
if (VLOG_IS_ON(2)) {
@@ -3956,21 +3925,8 @@ bool CpModelPresolver::PropagateDomainsInLinear(int ct_index,
if (fixed) {
context_->UpdateRuleStats("linear: tightened into equality");
// Compute a new `var` hint so that the lhs of `ct` is equal to `rhs`.
SolutionCrush& crush = context_->solution_crush();
int64_t var_hint = rhs.FixedValue();
bool var_hint_is_valid = true;
for (int j = 0; j < num_vars; ++j) {
if (j == i) continue;
const int term_var = ct->linear().vars(j);
if (!crush.VarHasSolutionHint(term_var)) {
var_hint_is_valid = false;
break;
}
var_hint -= crush.SolutionHint(term_var) * ct->linear().coeffs(j);
}
if (var_hint_is_valid) {
crush.UpdateRefSolutionHint(var, var_hint / var_coeff);
}
solution_crush_.SetVarToLinearConstraintSolution(
i, ct->linear().vars(), ct->linear().coeffs(), rhs.FixedValue());
FillDomainInProto(rhs, ct->mutable_linear());
negated_rhs = rhs.Negation();
@@ -9706,11 +9662,8 @@ void CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements(
// increase the objective value thanks to the `skip` test above -- the
// objective domain is non-constraining, but this only guarantees that
// singleton variables can freely *decrease* the objective).
SolutionCrush& crush = context_->solution_crush();
if (crush.LiteralSolutionHint(a) != crush.LiteralSolutionHint(b)) {
crush.UpdateLiteralSolutionHint(a, true);
crush.UpdateLiteralSolutionHint(b, true);
}
solution_crush_.UpdateLiteralsToFalseIfDifferent(NegatedRef(a),
NegatedRef(b));
context_->StoreBooleanEqualityRelation(a, b);
// We can also remove duplicate constraint now. It will be done later but
@@ -11912,15 +11865,8 @@ void CpModelPresolver::ProcessVariableOnlyUsedInEncoding(int var) {
// only guarantees that `var` can freely *decrease* the objective). The
// code below ensures this (`value2` is the 'cheapest' value the implied
// domain, and `value1` the cheapest value in the variable's domain).
bool enforcing_hint = true;
SolutionCrush& crush = context_->solution_crush();
for (const int enforcement_lit : ct.enforcement_literal()) {
if (crush.LiteralSolutionHintIs(enforcement_lit, false)) {
enforcing_hint = false;
break;
}
}
crush.UpdateVarSolutionHint(var, enforcing_hint ? value2 : value1);
solution_crush_.SetVarToConditionalValue(var, ct.enforcement_literal(),
value2, value1);
return (void)context_->IntersectDomainWith(
var, Domain::FromValues({value1, value2}));
}
@@ -13020,7 +12966,8 @@ bool ModelCopy::CopyLinear(const ConstraintProto& ct) {
}
// Constraint is false?
if (implied.IntersectionWith(new_rhs).IsEmpty()) {
const Domain tight_domain = implied.IntersectionWith(new_rhs);
if (tight_domain.IsEmpty()) {
if (ct.enforcement_literal().empty()) return false;
temp_literals_.clear();
for (const int literal : ct.enforcement_literal()) {
@@ -13051,7 +12998,7 @@ bool ModelCopy::CopyLinear(const ConstraintProto& ct) {
non_fixed_variables_.end());
linear->mutable_coeffs()->Add(non_fixed_coefficients_.begin(),
non_fixed_coefficients_.end());
FillDomainInProto(new_rhs, linear);
FillDomainInProto(tight_domain, linear);
return true;
}
@@ -13689,6 +13636,7 @@ CpModelPresolver::CpModelPresolver(PresolveContext* context,
std::vector<int>* postsolve_mapping)
: postsolve_mapping_(postsolve_mapping),
context_(context),
solution_crush_(context->solution_crush()),
logger_(context->logger()),
time_limit_(context->time_limit()),
interval_representative_(context->working_model->constraints_size(),
@@ -13896,7 +13844,7 @@ CpSolverStatus CpModelPresolver::Presolve() {
}
}
if (!context_->solution_crush().HintIsLoaded()) {
if (!solution_crush_.HintIsLoaded()) {
context_->LoadSolutionHint();
}
ExpandCpModelAndCanonicalizeConstraints();

2
ortools/sat/cp_model_presolve.h
View File

@@ -33,6 +33,7 @@
#include "ortools/sat/presolve_util.h"
#include "ortools/sat/sat_base.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/sat/solution_crush.h"
#include "ortools/sat/util.h"
#include "ortools/util/logging.h"
#include "ortools/util/sorted_interval_list.h"
@@ -329,6 +330,7 @@ class CpModelPresolver {
std::vector<int>* postsolve_mapping_;
PresolveContext* context_;
SolutionCrush& solution_crush_;
SolverLogger* logger_;
TimeLimit* time_limit_;

50
ortools/sat/cp_model_symmetries.cc
View File

@@ -931,48 +931,6 @@ std::vector<int64_t> BuildInequalityCoeffsForOrbitope(
return out;
}
void UpdateHintAfterFixingBoolToBreakSymmetry(
PresolveContext* context, int var, bool fixed_value,
absl::Span<const std::unique_ptr<SparsePermutation>> generators) {
SolutionCrush& crush = context->solution_crush();
if (!crush.VarHasSolutionHint(var)) {
return;
}
const int64_t hinted_value = crush.SolutionHint(var);
if (hinted_value == static_cast<int64_t>(fixed_value)) {
return;
}
std::vector<int> schrier_vector;
std::vector<int> orbit;
GetSchreierVectorAndOrbit(var, generators, &schrier_vector, &orbit);
bool found_target = false;
int target_var;
for (int v : orbit) {
if (crush.VarHasSolutionHint(v) &&
crush.SolutionHint(v) == static_cast<int64_t>(fixed_value)) {
found_target = true;
target_var = v;
break;
}
}
if (!found_target) {
context->UpdateRuleStats(
"hint: couldn't transform infeasible hint properly");
return;
}
const std::vector<int> generator_idx =
TracePoint(target_var, schrier_vector, generators);
for (const int i : generator_idx) {
crush.PermuteVariables(*generators[i]);
}
DCHECK(crush.VarHasSolutionHint(var));
DCHECK_EQ(crush.SolutionHint(var), fixed_value);
}
} // namespace
bool DetectAndExploitSymmetriesInPresolve(PresolveContext* context) {
@@ -1252,9 +1210,7 @@ bool DetectAndExploitSymmetriesInPresolve(PresolveContext* context) {
const int var = can_be_fixed_to_false[i];
if (orbits[var] == orbit_index) ++num_in_orbit;
context->UpdateRuleStats("symmetry: fixed to false in general orbit");
SolutionCrush& crush = context->solution_crush();
if (crush.VarHasSolutionHint(var) && crush.SolutionHint(var) == 1 &&
var_can_be_true_per_orbit[orbits[var]] != -1) {
if (var_can_be_true_per_orbit[orbits[var]] != -1) {
// We are breaking the symmetry in a way that makes the hint invalid.
// We want `var` to be false, so we would naively pick a symmetry to
// enforce that. But that will be wrong if we do this twice: after we
@@ -1263,8 +1219,8 @@ bool DetectAndExploitSymmetriesInPresolve(PresolveContext* context) {
// of those, and picking the wrong one would risk making the first one
// true again. Since this is a AMO, fixing the one that is true doesn't
// have this problem.
UpdateHintAfterFixingBoolToBreakSymmetry(
context, var_can_be_true_per_orbit[orbits[var]], true, generators);
context->solution_crush().MaybeUpdateVarWithSymmetriesToValue(
var_can_be_true_per_orbit[orbits[var]], true, generators);
}
if (!context->SetLiteralToFalse(var)) return false;
}

9
ortools/sat/presolve_context.cc
View File

@@ -1088,11 +1088,10 @@ bool PresolveContext::StoreAffineRelation(int var_x, int var_y, int64_t coeff,
DCHECK_NE(coeff, 0);
if (is_unsat_) return false;
if (!solution_crush_.MaybeSetVarToAffineEquationSolution(var_x, var_y, coeff,
offset)) {
UpdateRuleStats(
"Warning: hint didn't satisfy affine relation and was corrected");
}
// Sets var_y's value to the solution of
// "var_x's value - coeff * var_y's value = offset".
solution_crush_.SetVarToLinearConstraintSolution(1, {var_x, var_y},
{1, -coeff}, offset);
// TODO(user): I am not 100% sure why, but sometimes the representative is
// fixed but that is not propagated to var_x or var_y and this causes issues.

254
ortools/sat/solution_crush.cc
View File

@@ -15,7 +15,12 @@
#include <algorithm>
#include <cstdint>
#include <memory>
#include <optional>
#ifdef CHECK_HINT
#include <sstream>
#include <string>
#endif
#include <utility>
#include <vector>
@@ -23,9 +28,11 @@
#include "absl/log/check.h"
#include "absl/types/span.h"
#include "ortools/algorithms/sparse_permutation.h"
#include "ortools/base/logging.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/sat/symmetry_util.h"
#include "ortools/util/sorted_interval_list.h"
namespace operations_research {
@@ -64,17 +71,32 @@ void SolutionCrush::SetVarToLinearExpression(
int new_var, absl::Span<const std::pair<int, int64_t>> linear) {
// We only fill the hint of the new variable if all the variable involved
// in its definition have a value.
if (hint_is_loaded_) {
int64_t new_value = 0;
for (const auto [var, coeff] : linear) {
CHECK_GE(var, 0);
CHECK_LE(var, hint_.size());
if (!hint_has_value_[var]) return;
new_value += coeff * hint_[var];
}
hint_has_value_[new_var] = true;
hint_[new_var] = new_value;
if (!hint_is_loaded_) return;
int64_t new_value = 0;
for (const auto [var, coeff] : linear) {
CHECK_GE(var, 0);
CHECK_LE(var, hint_.size());
if (!hint_has_value_[var]) return;
new_value += coeff * hint_[var];
}
SetVarHint(new_var, new_value);
}
void SolutionCrush::SetVarToLinearExpression(int new_var,
absl::Span<const int> vars,
absl::Span<const int64_t> coeffs) {
DCHECK_EQ(vars.size(), coeffs.size());
if (!hint_is_loaded_) return;
int64_t new_value = 0;
for (int i = 0; i < vars.size(); ++i) {
const int var = vars[i];
const int64_t coeff = coeffs[i];
CHECK_GE(var, 0);
CHECK_LE(var, hint_.size());
if (!hint_has_value_[var]) return;
new_value += coeff * hint_[var];
}
SetVarHint(new_var, new_value);
}
void SolutionCrush::SetVarToClause(int new_var, absl::Span<const int> clause) {
@@ -158,6 +180,17 @@ void SolutionCrush::SetVarToValueIf(int var, int64_t value, int condition_lit) {
Domain(RefIsPositive(condition_lit) ? 0 : 1));
}
void SolutionCrush::SetVarToLinearExpressionIf(
int var, const LinearExpressionProto& expr, int condition_lit) {
if (!hint_is_loaded_) return;
if (!VarHasSolutionHint(PositiveRef(condition_lit))) return;
if (!LiteralSolutionHint(condition_lit)) return;
const std::optional<int64_t> expr_value = GetExpressionSolutionHint(expr);
if (expr_value.has_value()) {
SetVarHint(var, expr_value.value());
}
}
void SolutionCrush::SetLiteralToValueIf(int literal, bool value,
int condition_lit) {
SetLiteralToValueIfLinearConstraintViolated(
@@ -165,6 +198,21 @@ void SolutionCrush::SetLiteralToValueIf(int literal, bool value,
Domain(RefIsPositive(condition_lit) ? 0 : 1));
}
void SolutionCrush::SetVarToConditionalValue(
int var, absl::Span<const int> condition_lits, int64_t value_if_true,
int64_t value_if_false) {
if (!hint_is_loaded_) return;
bool condition_value = true;
for (const int condition_lit : condition_lits) {
if (!VarHasSolutionHint(PositiveRef(condition_lit))) return;
if (!LiteralSolutionHint(condition_lit)) {
condition_value = false;
break;
}
}
SetVarHint(var, condition_value ? value_if_true : value_if_false);
}
void SolutionCrush::MakeLiteralsEqual(int lit1, int lit2) {
if (!hint_is_loaded_) return;
if (hint_has_value_[PositiveRef(lit2)]) {
@@ -207,6 +255,42 @@ void SolutionCrush::UpdateLiteralsWithDominance(int lit, int dominating_lit) {
}
}
void SolutionCrush::MaybeUpdateVarWithSymmetriesToValue(
int var, bool value,
absl::Span<const std::unique_ptr<SparsePermutation>> generators) {
if (!hint_is_loaded_) return;
if (!VarHasSolutionHint(var)) return;
if (SolutionHint(var) == static_cast<int64_t>(value)) return;
std::vector<int> schrier_vector;
std::vector<int> orbit;
GetSchreierVectorAndOrbit(var, generators, &schrier_vector, &orbit);
bool found_target = false;
int target_var;
for (int v : orbit) {
if (VarHasSolutionHint(v) &&
SolutionHint(v) == static_cast<int64_t>(value)) {
found_target = true;
target_var = v;
break;
}
}
if (!found_target) {
VLOG(1) << "Couldn't transform hint properly";
return;
}
const std::vector<int> generator_idx =
TracePoint(target_var, schrier_vector, generators);
for (const int i : generator_idx) {
PermuteVariables(*generators[i]);
}
DCHECK(VarHasSolutionHint(var));
DCHECK_EQ(SolutionHint(var), value);
}
void SolutionCrush::UpdateRefsWithDominance(
int ref, int64_t min_value, int64_t max_value,
absl::Span<const std::pair<int, Domain>> dominating_refs) {
@@ -237,30 +321,39 @@ void SolutionCrush::UpdateRefsWithDominance(
}
}
bool SolutionCrush::MaybeSetVarToAffineEquationSolution(int var_x, int var_y,
int64_t coeff,
int64_t offset) {
if (hint_is_loaded_) {
if (!hint_has_value_[var_y] && hint_has_value_[var_x]) {
hint_has_value_[var_y] = true;
hint_[var_y] = (hint_[var_x] - offset) / coeff;
if (hint_[var_y] * coeff + offset != hint_[var_x]) {
// TODO(user): Do we implement a rounding to closest instead of
// routing towards 0.
return false;
void SolutionCrush::SetVarToLinearConstraintSolution(
std::optional<int> var_index, absl::Span<const int> vars,
absl::Span<const int64_t> coeffs, int64_t rhs) {
DCHECK_EQ(vars.size(), coeffs.size());
DCHECK(!var_index.has_value() || var_index.value() < vars.size());
if (!hint_is_loaded_) return;
int64_t term_value = rhs;
for (int i = 0; i < vars.size(); ++i) {
if (VarHasSolutionHint(vars[i])) {
if (i != var_index) {
term_value -= SolutionHint(vars[i]) * coeffs[i];
}
} else if (!var_index.has_value()) {
var_index = i;
} else if (var_index.value() != i) {
return;
}
}
if (!var_index.has_value()) return;
SetVarHint(vars[var_index.value()], term_value / coeffs[var_index.value()]);
#ifdef CHECK_HINT
const int64_t vx = hint_[var_x];
const int64_t vy = hint_[var_y];
if (model_has_hint_ && hint_is_loaded_ && vx != vy * coeff + offset) {
LOG(FATAL) << "Affine relation incompatible with hint: " << vx
<< " != " << vy << " * " << coeff << " + " << offset;
if (term_value % coeffs[var_index.value()] != 0) {
std::stringstream lhs;
for (int i = 0; i < vars.size(); ++i) {
lhs << (i == var_index ? "x" : std::to_string(SolutionHint(vars[i])));
lhs << " * " << coeffs[i];
if (i < vars.size() - 1) lhs << " + ";
}
LOG(FATAL) << "Linear constraint incompatible with solution: " << lhs
<< " != " << rhs;
}
#endif
return true;
}
void SolutionCrush::SetReservoirCircuitVars(
@@ -418,6 +511,113 @@ void SolutionCrush::SetIntProdExpandedVars(const LinearArgumentProto& int_prod,
}
}
void SolutionCrush::SetLinMaxExpandedVars(
const LinearArgumentProto& lin_max,
absl::Span<const int> enforcement_lits) {
if (!hint_is_loaded_) return;
DCHECK_EQ(enforcement_lits.size(), lin_max.exprs_size());
const std::optional<int64_t> target_hint =
GetExpressionSolutionHint(lin_max.target());
if (!target_hint.has_value()) return;
int enforcement_hint_sum = 0;
for (int i = 0; i < enforcement_lits.size(); ++i) {
const std::optional<int64_t> expr_hint =
GetExpressionSolutionHint(lin_max.exprs(i));
if (!expr_hint.has_value()) return;
if (enforcement_hint_sum == 0) {
const bool hint = target_hint.value() <= expr_hint.value();
SetLiteralHint(enforcement_lits[i], hint);
enforcement_hint_sum += hint;
} else {
SetLiteralHint(enforcement_lits[i], false);
}
}
}
void SolutionCrush::SetAutomatonExpandedVars(
const AutomatonConstraintProto& automaton,
absl::Span<const StateVar> state_vars,
absl::Span<const TransitionVar> transition_vars) {
if (!hint_is_loaded_) return;
absl::flat_hash_map<std::pair<int64_t, int64_t>, int64_t> transitions;
for (int i = 0; i < automaton.transition_tail_size(); ++i) {
transitions[{automaton.transition_tail(i), automaton.transition_label(i)}] =
automaton.transition_head(i);
}
std::vector<int64_t> label_hints;
std::vector<int64_t> state_hints;
int64_t current_state = automaton.starting_state();
state_hints.push_back(current_state);
for (int i = 0; i < automaton.exprs_size(); ++i) {
const std::optional<int64_t> label_hint =
GetExpressionSolutionHint(automaton.exprs(i));
if (!label_hint.has_value()) return;
label_hints.push_back(label_hint.value());
const auto it = transitions.find({current_state, label_hint.value()});
if (it == transitions.end()) return;
current_state = it->second;
state_hints.push_back(current_state);
}
for (const auto& [var, time, state] : state_vars) {
SetVarHint(var, state_hints[time] == state);
}
for (const auto& [var, time, transition_tail, transition_label] :
transition_vars) {
SetVarHint(var, state_hints[time] == transition_tail &&
label_hints[time] == transition_label);
}
}
void SolutionCrush::SetTableExpandedVars(
absl::Span<const int> column_vars, absl::Span<const int> existing_row_lits,
absl::Span<const TableRowLiteral> new_row_lits) {
if (!hint_is_loaded_) return;
int hint_sum = 0;
for (const int lit : existing_row_lits) {
if (!VarHasSolutionHint(PositiveRef(lit))) return;
hint_sum += LiteralSolutionHint(lit);
}
const int num_vars = column_vars.size();
for (const auto& [lit, var_values] : new_row_lits) {
if (hint_sum >= 1) {
SetLiteralHint(lit, false);
continue;
}
bool row_hint = true;
for (int var_index = 0; var_index < num_vars; ++var_index) {
const auto& values = var_values[var_index];
if (!values.empty() &&
std::find(values.begin(), values.end(),
SolutionHint(column_vars[var_index])) == values.end()) {
row_hint = false;
break;
}
}
SetLiteralHint(lit, row_hint);
hint_sum += row_hint;
}
}
void SolutionCrush::SetLinearWithComplexDomainExpandedVars(
const LinearConstraintProto& linear, absl::Span<const int> bucket_lits) {
if (!hint_is_loaded_) return;
int64_t expr_hint = 0;
for (int i = 0; i < linear.vars_size(); ++i) {
const int var = linear.vars(i);
if (!VarHasSolutionHint(var)) return;
expr_hint += linear.coeffs(i) * hint_[var];
}
DCHECK_LE(bucket_lits.size(), linear.domain_size() / 2);
for (int i = 0; i < bucket_lits.size(); ++i) {
const int64_t lb = linear.domain(2 * i);
const int64_t ub = linear.domain(2 * i + 1);
SetLiteralHint(bucket_lits[i], expr_hint >= lb && expr_hint <= ub);
}
}
void SolutionCrush::PermuteVariables(const SparsePermutation& permutation) {
CHECK(hint_is_loaded_);
permutation.ApplyToDenseCollection(hint_);

97
ortools/sat/solution_crush.h
View File

@@ -15,11 +15,13 @@
#define OR_TOOLS_SAT_SOLUTION_CRUSH_H_
#include <cstdint>
#include <memory>
#include <optional>
#include <utility>
#include <vector>
#include "absl/container/flat_hash_map.h"
#include "absl/container/inlined_vector.h"
#include "absl/log/check.h"
#include "absl/types/span.h"
#include "ortools/algorithms/sparse_permutation.h"
@@ -135,6 +137,11 @@ class SolutionCrush {
void SetVarToLinearExpression(
int var, absl::Span<const std::pair<int, int64_t>> linear);
// Sets the value of `var` to the value of the given linear expression.
// The two spans must have the same size.
void SetVarToLinearExpression(int var, absl::Span<const int> vars,
absl::Span<const int64_t> coeffs);
// Sets the value of `var` to 1 if the value of at least one literal in
// `clause` is equal to 1 (or to 0 otherwise). `clause` must be a list of
// literal indices.
@@ -162,10 +169,20 @@ class SolutionCrush {
// Sets the value of `var` to `value` if the value of `condition_lit` is true.
void SetVarToValueIf(int var, int64_t value, int condition_lit);
// Sets the value of `var` to the value `expr` if the value of `condition_lit`
// is true.
void SetVarToLinearExpressionIf(int var, const LinearExpressionProto& expr,
int condition_lit);
// Sets the value of `literal` to `value` if the value of `condition_lit` is
// true.
void SetLiteralToValueIf(int literal, bool value, int condition_lit);
// Sets the value of `var` to `value_if_true` if the value of all the
// `condition_lits` literals is true, and to `value_if_false` otherwise.
void SetVarToConditionalValue(int var, absl::Span<const int> condition_lits,
int64_t value_if_true, int64_t value_if_false);
// If one literal does not have a value, and the other one does, sets the
// value of the latter to the value of the former. If both literals have a
// value, sets the value of `lit1` to the value of `lit2`.
@@ -197,11 +214,23 @@ class SolutionCrush {
int ref, int64_t min_value, int64_t max_value,
absl::Span<const std::pair<int, Domain>> dominating_refs);
// Sets the value of `var_y` so that "`var_x`'s value = `var_y`'s value
// * `coeff` + `offset`". Does nothing if `var_y` already has a value.
// Returns whether the update was successful.
bool MaybeSetVarToAffineEquationSolution(int var_x, int var_y, int64_t coeff,
int64_t offset);
// If `var`'s value != `value` finds another variable in the orbit of `var`
// that can take that value, and permute the solution (using the symmetry
// `generators`) so that this other variable is at position var. If no other
// variable can be found, does nothing.
void MaybeUpdateVarWithSymmetriesToValue(
int var, bool value,
absl::Span<const std::unique_ptr<SparsePermutation>> generators);
// Sets the value of the i-th variable in `vars` so that the given constraint
// "dotproduct(coeffs, vars values) = rhs" is satisfied, if all the other
// variables have a value. i is equal to `var_index` if set. Otherwise it is
// the index of the variable without a value (if there is not exactly one,
// this method does nothing).
void SetVarToLinearConstraintSolution(std::optional<int> var_index,
absl::Span<const int> vars,
absl::Span<const int64_t> coeffs,
int64_t rhs);
// Sets the value of the variables in `level_vars` and in `circuit` if all the
// variables in `reservoir` have a value. This assumes that there is one level
@@ -240,7 +269,61 @@ class SolutionCrush {
void SetIntProdExpandedVars(const LinearArgumentProto& int_prod,
absl::Span<const int> prod_vars);
void PermuteVariables(const SparsePermutation& permutation);
// Sets the value of `enforcement_lits` if all the variables in `lin_max`
// have a value, assuming that the `lin_max` constraint "target = max(x_0,
// x_1, ..., x_(n-1))" is expanded into "enforcement_lits[i] => target <= x_i"
// constraints, with at most one enforcement value equal to true.
// `enforcement_lits` must have as many elements as `lin_max`.
void SetLinMaxExpandedVars(const LinearArgumentProto& lin_max,
absl::Span<const int> enforcement_lits);
// Represents `var` = "automaton is in state `state` at time `time`".
struct StateVar {
int var;
int time;
int64_t state;
};
// Represents `var` = "automaton takes the transition labeled
// `transition_label` from state `transition_tail` at time `time`".
struct TransitionVar {
int var;
int time;
int64_t transition_tail;
int64_t transition_label;
};
// Sets the value of `state_vars` and `transition_vars` if all the variables
// in `automaton` have a value.
void SetAutomatonExpandedVars(
const AutomatonConstraintProto& automaton,
absl::Span<const StateVar> state_vars,
absl::Span<const TransitionVar> transition_vars);
// Represents `lit` = "for all i, the value of the i-th column var of a table
// constraint is in the `var_values`[i] set (unless this set is empty).".
struct TableRowLiteral {
int lit;
// TODO(user): use a vector of (var, value) pairs instead?
std::vector<absl::InlinedVector<int64_t, 2>> var_values;
};
// Sets the value of the `new_row_lits` literals if all the variables in
// `column_vars` and `existing_row_lits` have a value. For each `row_lits`,
// `column_values` must have the same size as `column_vars`. This method
// assumes that exactly one of `existing_row_lits` and `new_row_lits` must be
// true.
void SetTableExpandedVars(absl::Span<const int> column_vars,
absl::Span<const int> existing_row_lits,
absl::Span<const TableRowLiteral> new_row_lits);
// Sets the value of `bucket_lits` if all the variables in `linear` have a
// value, assuming that they are expanded from the complex linear constraint
// (i.e. one whose domain has two or more intervals). The value of
// `bucket_lits`[i] is set to 1 iff the value of the linear expression is in
// the i-th interval of the domain.
void SetLinearWithComplexDomainExpandedVars(
const LinearConstraintProto& linear, absl::Span<const int> bucket_lits);
private:
void SetVarHint(int var, int64_t value) {
@@ -252,6 +335,8 @@ class SolutionCrush {
SetVarHint(PositiveRef(lit), RefIsPositive(lit) == value ? 1 : 0);
}
void PermuteVariables(const SparsePermutation& permutation);
// This contains all the hinted value or zero if the hint wasn't specified.
// We try to maintain this as we create new variable.
bool model_has_hint_ = false;