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

[CP-SAT] fix vivification bug; more work on encodings

Browse Source
This commit is contained in:
Laurent Perron
2026-01-07 13:01:43 +01:00
committed by Corentin Le Molgat
parent 74a9ed242d
commit 8d3645a6cd
19 changed files with 1224 additions and 432 deletions
Download Patch File Download Diff File Expand all files Collapse all files

28
ortools/sat/BUILD.bazel
View File

@@ -335,7 +335,9 @@ cc_library(
"//ortools/util:time_limit",
"@abseil-cpp//absl/algorithm:container",
"@abseil-cpp//absl/base:core_headers",
"@abseil-cpp//absl/cleanup",
"@abseil-cpp//absl/container:btree",
"@abseil-cpp//absl/log",
"@abseil-cpp//absl/log:check",
"@abseil-cpp//absl/types:span",
],
@@ -393,8 +395,32 @@ cc_library(
deps = [
":cp_model_utils",
":presolve_context",
"//ortools/base:stl_util",
"//ortools/util:bitset",
"//ortools/util:sorted_interval_list",
"@abseil-cpp//absl/algorithm:container",
"@abseil-cpp//absl/container:flat_hash_map",
"@abseil-cpp//absl/container:flat_hash_set",
"@abseil-cpp//absl/container:inlined_vector",
"@abseil-cpp//absl/log",
"@abseil-cpp//absl/log:check",
"@protobuf",
],
)
cc_test(
name = "presolve_encoding_test",
srcs = ["presolve_encoding_test.cc"],
deps = [
":cp_model_cc_proto",
":model",
":presolve_context",
":presolve_encoding",
"//ortools/base:gmock_main",
"//ortools/base:parse_test_proto",
"//ortools/util:sorted_interval_list",
"@abseil-cpp//absl/container:flat_hash_map",
"@abseil-cpp//absl/log:check",
],
)
@@ -975,8 +1001,10 @@ cc_library(
"//ortools/util:sigint",
"//ortools/util:sorted_interval_list",
"//ortools/util:strong_integers",
"//ortools/util:testing_utils",
"//ortools/util:time_limit",
"@abseil-cpp//absl/base:core_headers",
"@abseil-cpp//absl/base:log_severity",
"@abseil-cpp//absl/cleanup",
"@abseil-cpp//absl/container:btree",
"@abseil-cpp//absl/container:flat_hash_map",

15
ortools/sat/clause.cc
View File

@@ -529,7 +529,8 @@ bool ClauseManager::InprocessingRewriteClause(
}
const bool is_reason = ClauseIsUsedAsReason(clause);
CHECK(!is_reason || new_clause[0] == clause->PropagatedLiteral());
CHECK(!is_reason || new_clause[0] == clause->PropagatedLiteral())
<< new_clause << " old " << clause->AsSpan();
if (new_clause.empty()) return false; // UNSAT.
@@ -682,12 +683,24 @@ SatClause* ClauseManager::NextNewClauseToMinimize() {
}
SatClause* ClauseManager::NextClauseToMinimize() {
const int old = to_first_minimize_index_;
for (; to_minimize_index_ < clauses_.size(); ++to_minimize_index_) {
if (clauses_[to_minimize_index_]->IsRemoved()) continue;
if (!IsRemovable(clauses_[to_minimize_index_])) {
return clauses_[to_minimize_index_++];
}
}
// Lets reset and try once more to find one.
to_minimize_index_ = 0;
++num_to_minimize_index_resets_;
for (; to_minimize_index_ < old; ++to_minimize_index_) {
if (clauses_[to_minimize_index_]->IsRemoved()) continue;
if (!IsRemovable(clauses_[to_minimize_index_])) {
return clauses_[to_minimize_index_++];
}
}
return nullptr;
}

8
ortools/sat/clause.h
View File

@@ -308,6 +308,7 @@ class ClauseManager : public SatPropagator {
// Returns the next clause to minimize that has never been minimized before.
// Note that we only minimize clauses kept forever.
SatClause* NextNewClauseToMinimize();
// Returns the next clause to minimize, this iterator will be reset to the
// start so the clauses will be returned in round-robin order.
// Note that we only minimize clauses kept forever.
@@ -324,7 +325,10 @@ class ClauseManager : public SatPropagator {
// Restart the scans.
void ResetToProbeIndex() { to_probe_index_ = 0; }
void ResetToMinimizeIndex() { to_minimize_index_ = 0; }
int64_t NumToMinimizeIndexResets() const {
return num_to_minimize_index_resets_;
}
// Ensures that NextNewClauseToMinimize() returns only learned clauses.
// This is a noop after the first call.
void EnsureNewClauseIndexInitialized() {
@@ -499,6 +503,8 @@ class ClauseManager : public SatPropagator {
// TODO(user): If more indices are needed, switch to a generic API.
int to_minimize_index_ = 0;
int num_to_minimize_index_resets_ = 0;
int to_first_minimize_index_ = 0;
int to_probe_index_ = 0;

342
ortools/sat/cp_model_presolve.cc
View File

@@ -6815,7 +6815,8 @@ bool CpModelPresolver::PresolveNoOverlap2D(int /*c*/, ConstraintProto* ct) {
IntegerValue(context_->EndMax(y))});
}
CompactVectorVector<int> no_overlaps;
absl::c_sort(indexed_intervals, IndexedInterval::ComparatorByStart());
absl::c_stable_sort(indexed_intervals,
IndexedInterval::ComparatorByStart());
ConstructOverlappingSets(absl::MakeSpan(indexed_intervals), &no_overlaps);
for (int i = 0; i < no_overlaps.size(); ++i) {
ConstraintProto* new_ct = context_->working_model->add_constraints();
@@ -9431,341 +9432,18 @@ bool CpModelPresolver::MergeNoOverlap2DConstraints() {
return true;
}
namespace {
bool ConstraintIsEncodingBound(const ConstraintProto& ct) {
if (ct.constraint_case() != ConstraintProto::kLinear) return false;
if (ct.linear().vars_size() != 1) return false;
if (ct.linear().coeffs(0) != 1) return false;
if (ct.enforcement_literal_size() != 1) return false;
return true;
}
} // namespace
// Return true if something changed.
bool CpModelPresolver::DetectEncodedComplexDomain(
PresolveContext* context, ConstraintProto* ct,
const Bitset64<int>& pertinent_bools) {
if (context->ModelIsUnsat()) return false;
if (ct->constraint_case() != ConstraintProto::kAtMostOne &&
ct->constraint_case() != ConstraintProto::kExactlyOne &&
ct->constraint_case() != ConstraintProto::kBoolOr) {
return false;
}
// Handling exaclty_one, at_most_one and bool_or is pretty similar. If we have
// l1 <=> v \in D1
// l2 <=> v \in D2
//
// We built
// l <=> v \in (D1 U D2).
//
// Moreover, if we have exactly_one(l1, l2, ...) or at_most_one(l1, l2, ...),
// we know that v cannot be in the intersection of D1 and D2. Thus, we first
// unconditionally remove (D1 ∩ D2) from the domain of v, making
// (l1=true and l2=true) impossible and allowing us to write our clauses as
// exactly_one(l1 or l2, ...) or at_most_one(l1 or l2, ...).
//
// Thus, other than the domain reduction that should not be done for the
// bool_or, all we need is to create a variable
// (l1 or l2) == l <=> (v \in (D1 U D2)).
google::protobuf::RepeatedField<int32_t>& literals =
ct->constraint_case() == ConstraintProto::kAtMostOne
? *ct->mutable_at_most_one()->mutable_literals()
: (ct->constraint_case() == ConstraintProto::kExactlyOne
? *ct->mutable_exactly_one()->mutable_literals()
: *ct->mutable_bool_or()->mutable_literals());
if (literals.size() <= 1) return false;
if (!ct->enforcement_literal().empty()) {
// TODO(user): support this case if it any problem needs it.
return false;
}
struct Linear1Info {
int lit = -1;
int positive_linear1_ct = -1;
int negative_linear1_ct = -1;
};
absl::flat_hash_map<int, absl::InlinedVector<Linear1Info, 1>> var_to_linear1;
for (const int lit : literals) {
if (PositiveRef(lit) < pertinent_bools.size() &&
!pertinent_bools[PositiveRef(lit)]) {
continue;
}
bool or_and_single_var_linear1 = true;
Linear1Info info;
int var = -1;
for (const int c : context->VarToConstraints(PositiveRef(lit))) {
if (c < 0) {
or_and_single_var_linear1 = false;
break;
}
const ConstraintProto& other_ct = context->working_model->constraints(c);
if (&other_ct == ct) continue;
if (!ConstraintIsEncodingBound(other_ct)) {
or_and_single_var_linear1 = false;
break;
}
if (other_ct.enforcement_literal(0) != lit &&
other_ct.enforcement_literal(0) != NegatedRef(lit)) {
or_and_single_var_linear1 = false;
break;
}
if (var == -1) {
var = other_ct.linear().vars(0);
} else if (var != other_ct.linear().vars(0)) {
or_and_single_var_linear1 = false;
break;
}
info.lit = lit;
if (other_ct.enforcement_literal(0) == lit) {
info.positive_linear1_ct = c;
} else {
DCHECK_EQ(other_ct.enforcement_literal(0), NegatedRef(lit));
info.negative_linear1_ct = c;
}
}
// When we have
// lit => var in D1
// ~lit => var in D2
// we can represent this on a line:
//
// ----------------D1----------------
// ----------------D2---------------
// |+++++++++++|*********************|++++++++++|
// lit=false lit unconstrained lit=true
//
// Handling the case where the variable is unconstrained by the lit is a
// bit of a pain: we want to replace two literals in a exactly_one by a
// single one, and if they are both unconstrained we might be forced to pick
// one arbitrarily to set to true. In any case, this is not a proper
// encoding of a complex domain, so we just ignore it.
// TODO(user): This can be implemented if it turns out to be common.
if (or_and_single_var_linear1 && info.negative_linear1_ct != -1 &&
info.positive_linear1_ct != -1) {
const Domain domain_enforced_lit = ReadDomainFromProto(
context->working_model->constraints(info.positive_linear1_ct)
.linear());
// ~lit1 => var in domain_enforced_not_lit1
const Domain domain_enforced_not_lit = ReadDomainFromProto(
context->working_model->constraints(info.negative_linear1_ct)
.linear());
if (domain_enforced_lit.IntersectionWith(domain_enforced_not_lit)
.IsEmpty()) {
var_to_linear1[var].push_back(info);
}
}
}
// Ignore all variables that only appear once.
std::vector<std::pair<int, std::vector<Linear1Info>>> var_to_linear1_infos;
for (const auto& [var, linear1_infos] : var_to_linear1) {
if (linear1_infos.size() > 1) {
var_to_linear1_infos.push_back(
{var, std::vector<Linear1Info>(linear1_infos.begin(),
linear1_infos.end())});
}
}
if (var_to_linear1_infos.empty()) return false;
// We have some variables to simplify! Start by sorting to make the code
// deterministic.
absl::c_sort(var_to_linear1_infos,
[](const std::pair<int, std::vector<Linear1Info>>& a,
const std::pair<int, std::vector<Linear1Info>>& b) {
return a.first < b.first;
});
// Doing the general code is rather complex, so we will just simplify one
// variable and two literals at a time, and leave for the presolve fixpoint
// to do the rest.
for (const auto& [var, infos] : var_to_linear1_infos) {
const Linear1Info& info1 = infos[0];
const Linear1Info& info2 = infos[1];
const int lit1 = info1.lit;
const int lit2 = info2.lit;
const Domain original_var_domain = context->DomainOf(var);
DCHECK_NE(info1.positive_linear1_ct, -1);
DCHECK_NE(info2.positive_linear1_ct, -1);
DCHECK_NE(info1.negative_linear1_ct, -1);
DCHECK_NE(info2.negative_linear1_ct, -1);
// lit1 => var in domain_enforced_lit1
const Domain domain_enforced_lit1 = ReadDomainFromProto(
context->working_model->constraints(info1.positive_linear1_ct)
.linear());
// ~lit1 => var in domain_enforced_not_lit1
const Domain domain_enforced_not_lit1 = ReadDomainFromProto(
context->working_model->constraints(info1.negative_linear1_ct)
.linear());
// lit2 => var in domain_enforced_lit2
const Domain domain_enforced_lit2 = ReadDomainFromProto(
context->working_model->constraints(info2.positive_linear1_ct)
.linear());
// ~lit2 => var in domain_enforced_not_lit2
const Domain domain_enforced_not_lit2 = ReadDomainFromProto(
context->working_model->constraints(info2.negative_linear1_ct)
.linear());
DCHECK(domain_enforced_lit1.IntersectionWith(domain_enforced_not_lit1)
.IsEmpty());
DCHECK(domain_enforced_lit2.IntersectionWith(domain_enforced_not_lit2)
.IsEmpty());
// First, the variable must be in the domain of either the lit or of its
// negation.
if (!context->IntersectDomainWith(
var, domain_enforced_lit1.UnionWith(domain_enforced_not_lit1))) {
return true;
}
if (!context->IntersectDomainWith(
var, domain_enforced_lit2.UnionWith(domain_enforced_not_lit2))) {
return true;
}
if (ct->constraint_case() != ConstraintProto::kBoolOr) {
// In virtue of the AMO, var must not be in the intersection of the two
// domains where both literals are true.
if (!context->IntersectDomainWith(
var, domain_enforced_lit2.IntersectionWith(domain_enforced_lit1)
.Complement())) {
return true;
}
}
const Domain domain_new_var_false = context->DomainOf(var).IntersectionWith(
domain_enforced_not_lit1.IntersectionWith(domain_enforced_not_lit2));
const Domain domain_new_var_true = context->DomainOf(var).IntersectionWith(
domain_new_var_false.Complement());
// Now we want to build a lit3 = (lit1 or lit2) to use in the AMO/bool_or.
const int new_var = context->NewBoolVarWithClause({lit1, lit2});
if (domain_new_var_true.IsEmpty()) {
if (!context->SetLiteralToFalse(new_var)) return true;
} else if (domain_new_var_false.IsEmpty()) {
if (!context->SetLiteralToTrue(new_var)) return true;
} else {
ConstraintProto* new_ct = context->working_model->add_constraints();
new_ct->add_enforcement_literal(new_var);
new_ct->mutable_linear()->add_vars(var);
new_ct->mutable_linear()->add_coeffs(1);
FillDomainInProto(domain_new_var_true, new_ct->mutable_linear());
new_ct = context->working_model->add_constraints();
new_ct->add_enforcement_literal(NegatedRef(new_var));
new_ct->mutable_linear()->add_vars(var);
new_ct->mutable_linear()->add_coeffs(1);
FillDomainInProto(domain_new_var_false, new_ct->mutable_linear());
}
// Remove the two literals from the AMO.
int new_size = 0;
for (int i = 0; i < literals.size(); ++i) {
if (literals.Get(i) != lit1 && literals.Get(i) != lit2) {
literals.Set(new_size++, literals.Get(i));
}
}
literals.Truncate(new_size);
literals.Add(new_var);
context->UpdateNewConstraintsVariableUsage();
context->UpdateRuleStats(
"variables: detected encoding of a complex domain with multiple "
"linear1");
}
return true;
}
void CpModelPresolver::DetectEncodedComplexDomains(PresolveContext* context) {
PresolveTimer timer(__FUNCTION__, logger_, time_limit_);
// Constraints taking a list of literals that can, under some conditions,
// accept the following substitution:
// constraint(a, b, ...) => constraint(a | b, ...)
// one obvious case is bool_or. But if we can know that a and b cannot be
// both true, we can also apply this to at_most_one and exactly_one.
std::vector<int> constraint_encoding_or; // bool_or, exactly_one, at_most_one
if (context->ModelIsUnsat()) return;
if (time_limit_->LimitReached()) return;
// To make sure this is not too slow, first do a pass to gather all linear1
// constraints that shares the same variable with other three linear1.
absl::flat_hash_map<int, absl::InlinedVector<int, 1>> var_to_linear1;
for (int i = 0; i < context->working_model->constraints_size(); ++i) {
const ConstraintProto& ct = context->working_model->constraints(i);
if (ct.constraint_case() == ConstraintProto::kBoolOr ||
ct.constraint_case() == ConstraintProto::kAtMostOne ||
ct.constraint_case() == ConstraintProto::kExactlyOne) {
constraint_encoding_or.push_back(i);
continue;
std::vector<VariableEncodingLocalModel> local_models =
CreateVariableEncodingLocalModels(context);
for (VariableEncodingLocalModel& local_model : local_models) {
if (time_limit_->LimitReached()) return;
if (!DetectAllEncodedComplexDomain(context, local_model)) {
return;
}
if (!ConstraintIsEncodingBound(ct)) {
continue;
}
var_to_linear1[ct.linear().vars(0)].push_back(i);
}
absl::erase_if(var_to_linear1,
[](const auto& p) { return p.second.size() <= 3; });
// Now that we reduced cheaply our set of "interesting" linear1, let's use the
// variable->constraint graph to restrict it further.
for (auto& [var, linear1_cts] : var_to_linear1) {
int new_size = 0;
for (const int ct : linear1_cts) {
const int ref =
context->working_model->constraints(ct).enforcement_literal(0);
// We want to focus on literals that become removable once we undo the
// encoding, otherwise this whole step might just make the problem harder.
// So we want it to appear in two linear1 and a bool_or/amo/exactly_one.
if (context->VarToConstraints(PositiveRef(ref)).size() <= 3) {
linear1_cts[new_size++] = ct;
}
}
linear1_cts.resize(new_size);
}
absl::erase_if(var_to_linear1,
[](const auto& p) { return p.second.size() <= 3; });
if (var_to_linear1.empty()) return;
// Now we use the linear1 we found to see which bool_or/amo/exactly_one could
// be applied to the heuristic.
Bitset64<int> booleans_potentially_encoding_domain(
context_->working_model->variables_size());
for (const auto& [unused, linear1_cts] : var_to_linear1) {
for (const int ct : linear1_cts) {
booleans_potentially_encoding_domain.Set(PositiveRef(
context->working_model->constraints(ct).enforcement_literal(0)));
}
}
int new_encoding_or_count = 0;
for (int i = 0; i < constraint_encoding_or.size(); ++i) {
const int c = constraint_encoding_or[i];
const ConstraintProto& ct = context->working_model->constraints(c);
const BoolArgumentProto& bool_ct =
ct.constraint_case() == ConstraintProto::kAtMostOne
? ct.at_most_one()
: (ct.constraint_case() == ConstraintProto::kExactlyOne
? ct.exactly_one()
: ct.bool_or());
if (absl::c_count_if(
bool_ct.literals(),
[booleans_potentially_encoding_domain](int ref) {
return booleans_potentially_encoding_domain[PositiveRef(ref)];
}) < 2) {
continue;
}
constraint_encoding_or[new_encoding_or_count++] = c;
}
constraint_encoding_or.resize(new_encoding_or_count);
for (const int c : constraint_encoding_or) {
ConstraintProto* ct = context->working_model->mutable_constraints(c);
bool changed = false;
do {
changed = DetectEncodedComplexDomain(
context, ct, booleans_potentially_encoding_domain);
if (changed) {
context->UpdateConstraintVariableUsage(c);
}
} while (changed);
}
}

6
ortools/sat/cp_model_presolve_test.cc
View File

@@ -7859,9 +7859,11 @@ TEST(PresolveCpModelTest, DetectEncodingFromLinear) {
params.set_keep_all_feasible_solutions_in_presolve(true);
const CpModelProto presolved_model = PresolveForTest(initial_model, params);
IntegerVariableProto expected_proto;
FillDomainInProto(Domain::FromValues({3, 6, 9, 10, 12}), &expected_proto);
// The values are 10, 10-1, 10-7, 10+2, and 10-4.
EXPECT_EQ(ReadDomainFromProto(presolved_model.variables(5)).ToString(),
"[3][6][9,10][12]");
EXPECT_THAT(presolved_model.variables(),
testing::Contains(testing::EqualsProto(expected_proto)));
}
TEST(PresolveCpModelTest, ReplaceNonEqual) {

6
ortools/sat/cp_model_solver.cc
View File

@@ -31,6 +31,7 @@
#include <utility>
#include <vector>
#include "absl/base/log_severity.h"
#include "absl/base/thread_annotations.h"
#include "absl/container/btree_map.h"
#include "absl/container/btree_set.h"
@@ -97,6 +98,7 @@
#include "ortools/util/random_engine.h"
#include "ortools/util/sigint.h"
#include "ortools/util/sorted_interval_list.h"
#include "ortools/util/testing_utils.h"
#include "ortools/util/time_limit.h"
ABSL_FLAG(
@@ -2529,8 +2531,8 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
}
#endif // ORTOOLS_TARGET_OS_SUPPORTS_THREADS
if (DEBUG_MODE) {
LOG(WARNING)
if (DEBUG_MODE && !ProbablyRunningInsideUnitTest()) {
LOG_EVERY_N_SEC(WARNING, 0.1)
<< "WARNING: CP-SAT is running in debug mode. The solver will "
"be slow because we will do a lot of extra checks. Compile in "
"optimization mode to gain an order of magnitude speedup.";

17
ortools/sat/integer_base.cc
View File

@@ -238,23 +238,6 @@ RelationStatus BestBinaryRelationBounds::GetStatus(LinearExpression2 expr,
return RelationStatus::IS_UNKNOWN;
}
IntegerValue BestBinaryRelationBounds::GetUpperBound(
LinearExpression2 expr) const {
expr.SimpleCanonicalization();
const IntegerValue gcd = expr.DivideByGcd();
const bool negated = expr.NegateForCanonicalization();
const auto it = best_bounds_.find(expr);
if (it != best_bounds_.end()) {
const auto [known_lb, known_ub] = it->second;
if (negated) {
return CapProdI(gcd, -known_lb);
} else {
return CapProdI(gcd, known_ub);
}
}
return kMaxIntegerValue;
}
std::vector<std::pair<LinearExpression2, IntegerValue>>
BestBinaryRelationBounds::GetSortedNonTrivialUpperBounds() const {
std::vector<std::pair<LinearExpression2, IntegerValue>> root_relations_sorted;

5
ortools/sat/integer_base.h
View File

@@ -514,11 +514,6 @@ class BestBinaryRelationBounds {
RelationStatus GetStatus(LinearExpression2 expr, IntegerValue lb,
IntegerValue ub) const;
// Return a valid upper-bound on the given LinearExpression2. Note that we
// assume kMaxIntegerValue is always valid and returns it if we don't have an
// entry in the hash-map.
IntegerValue GetUpperBound(LinearExpression2 expr) const;
// Same as GetUpperBound() but assume the expression is already canonicalized.
// This is slightly faster.
IntegerValue UpperBoundWhenCanonicalized(LinearExpression2 expr) const;

22
ortools/sat/integer_base_test.cc
View File

@@ -94,28 +94,6 @@ TEST(BestBinaryRelationBoundsTest, Basic) {
best_bounds.GetStatus(expr, IntegerValue(-5), IntegerValue(3)));
}
TEST(BestBinaryRelationBoundsTest, UpperBound) {
LinearExpression2 expr;
expr.vars[0] = IntegerVariable(0);
expr.vars[1] = IntegerVariable(2);
expr.coeffs[0] = IntegerValue(1);
expr.coeffs[1] = IntegerValue(-1);
using AddResult = BestBinaryRelationBounds::AddResult;
BestBinaryRelationBounds best_bounds;
EXPECT_EQ(best_bounds.Add(expr, IntegerValue(0), IntegerValue(5)),
std::make_pair(AddResult::ADDED, AddResult::ADDED));
EXPECT_EQ(best_bounds.GetUpperBound(expr), IntegerValue(5));
expr.coeffs[0] *= 3;
expr.coeffs[1] *= 3;
EXPECT_EQ(best_bounds.GetUpperBound(expr), IntegerValue(15));
expr.Negate();
EXPECT_EQ(best_bounds.GetUpperBound(expr), IntegerValue(0));
}
AffineExpression OtherAffineLowerBound(LinearExpression2 expr, int var_index,
IntegerValue expr_lb,
IntegerValue other_var_lb) {

570
ortools/sat/presolve_encoding.cc
View File

@@ -17,17 +17,586 @@
#include <cstdlib>
#include <functional>
#include <limits>
#include <optional>
#include <utility>
#include <vector>
#include "absl/algorithm/container.h"
#include "absl/container/flat_hash_map.h"
#include "absl/container/flat_hash_set.h"
#include "absl/container/inlined_vector.h"
#include "absl/log/check.h"
#include "absl/log/log.h"
#include "google/protobuf/repeated_field.h"
#include "ortools/base/stl_util.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/sat/presolve_context.h"
#include "ortools/util/bitset.h"
#include "ortools/util/sorted_interval_list.h"
namespace operations_research {
namespace sat {
namespace {
bool ConstraintIsEncodingBound(const ConstraintProto& ct) {
if (ct.constraint_case() != ConstraintProto::kLinear) return false;
if (ct.linear().vars_size() != 1) return false;
if (ct.linear().coeffs(0) != 1) return false;
if (ct.enforcement_literal_size() != 1) return false;
if (PositiveRef(ct.enforcement_literal(0)) == ct.linear().vars(0)) {
return false;
}
return true;
}
} // namespace
std::vector<VariableEncodingLocalModel> CreateVariableEncodingLocalModels(
PresolveContext* context) {
// In this function we want to make sure we don't waste too much time on
// problems that do not have many linear1. Thus, the first thing we do is to
// filter out as soon and cheaply as possible the bare minimum of constraints
// that could be relevant to the final output.
// Constraints taking a list of literals that can, under some conditions,
// accept the following substitution:
// constraint(a, b, ...) => constraint(a | b, ...)
// one obvious case is bool_or. But if we can know that a and b cannot be
// both true, we can also apply this to at_most_one and exactly_one.
//
// Note that in the implementation we might for simplicity refer to the
// constraints we are interested in as "bool_or" but this is just to avoid
// mentioning all the three types over and over.
// TODO(user): this should also work for linear constraints with the two
// booleans having the same coefficient?
std::vector<int> constraint_encoding_or; // bool_or, exactly_one, at_most_one
// Do a pass to gather all linear1 constraints.
absl::flat_hash_map<int, absl::InlinedVector<int, 1>> var_to_linear1;
for (int i = 0; i < context->working_model->constraints_size(); ++i) {
const ConstraintProto& ct = context->working_model->constraints(i);
if (ct.constraint_case() == ConstraintProto::kBoolOr ||
ct.constraint_case() == ConstraintProto::kAtMostOne ||
ct.constraint_case() == ConstraintProto::kExactlyOne) {
constraint_encoding_or.push_back(i);
continue;
}
if (!ConstraintIsEncodingBound(ct)) {
continue;
}
var_to_linear1[ct.linear().vars(0)].push_back(i);
}
// Filter out the variables that do not have an interesting encoding.
absl::erase_if(var_to_linear1, [context](const auto& p) {
if (p.second.size() > 1) return false;
return context->VarToConstraints(p.first).size() > 2;
});
if (var_to_linear1.empty()) return {};
absl::flat_hash_map<int, absl::InlinedVector<int, 2>> bool_to_var_encodings;
// Now we use the linear1 we found to see which bool_or/amo/exactly_one are
// linking two encodings of the same variable. But first, since some models
// have a lot of bool_or, we use a simple heuristic to filter out all that are
// not related to the encodings. We use a bitset to keep track of all boolean
// potentially encoding a domain for any variable and we filter out all
// bool_or that are not linked to at least two of these booleans.
Bitset64<int> booleans_potentially_encoding_domain(
context->working_model->variables_size());
for (const auto& [var, linear1_cts] : var_to_linear1) {
for (const int c : linear1_cts) {
const ConstraintProto& ct = context->working_model->constraints(c);
const int bool_var = PositiveRef(ct.enforcement_literal(0));
booleans_potentially_encoding_domain.Set(bool_var);
bool_to_var_encodings[bool_var].push_back(var);
}
}
for (auto& [bool_var, var_encodings] : bool_to_var_encodings) {
// Remove the potential duplicate for the negation.
gtl::STLSortAndRemoveDuplicates(&var_encodings);
}
int new_encoding_or_count = 0;
for (int i = 0; i < constraint_encoding_or.size(); ++i) {
const int c = constraint_encoding_or[i];
const ConstraintProto& ct = context->working_model->constraints(c);
const BoolArgumentProto& bool_ct =
ct.constraint_case() == ConstraintProto::kAtMostOne
? ct.at_most_one()
: (ct.constraint_case() == ConstraintProto::kExactlyOne
? ct.exactly_one()
: ct.bool_or());
if (absl::c_count_if(
bool_ct.literals(),
[booleans_potentially_encoding_domain](int ref) {
return booleans_potentially_encoding_domain[PositiveRef(ref)];
}) < 2) {
continue;
}
constraint_encoding_or[new_encoding_or_count++] = c;
}
constraint_encoding_or.resize(new_encoding_or_count);
// Track the number of times a given boolean appears in the local model for a
// given variable.
struct VariableAndBoolInfo {
// Can only be 1 or 2 (for negation) if properly presolved.
int linear1_count = 0;
// Number of times the boolean will appear in
// `constraints_linking_two_encoding_booleans`.
int bool_or_count = 0;
};
absl::flat_hash_map<std::pair<int, int>, VariableAndBoolInfo> var_bool_counts;
// Now that we have a potentially smaller set of bool_or, we actually check
// which of them are linking two encodings of the same variable.
absl::flat_hash_map<int, std::vector<int>> var_to_constraints_encoding_or;
// Map from variable to the bools that appear in a given bool_or.
absl::flat_hash_map<int, std::vector<int>> var_to_bools;
for (const int c : constraint_encoding_or) {
var_to_bools.clear();
const ConstraintProto& ct = context->working_model->constraints(c);
const BoolArgumentProto& bool_ct =
ct.constraint_case() == ConstraintProto::kAtMostOne
? ct.at_most_one()
: (ct.constraint_case() == ConstraintProto::kExactlyOne
? ct.exactly_one()
: ct.bool_or());
for (const int ref : bool_ct.literals()) {
const int bool_var = PositiveRef(ref);
if (!booleans_potentially_encoding_domain[bool_var]) continue;
for (const int var : bool_to_var_encodings[bool_var]) {
var_to_bools[var].push_back(bool_var);
}
}
for (const auto& [var, bools] : var_to_bools) {
if (bools.size() >= 2) {
// We have two encodings of `var` in the same constraint `c`. Thus `c`
// should be part of the local model for `var`.
var_to_constraints_encoding_or[var].push_back(c);
for (const int bool_var : bools) {
var_bool_counts[{var, bool_var}].bool_or_count++;
}
}
}
}
std::vector<VariableEncodingLocalModel> local_models;
// Now that we have all the information, we can create the local models.
for (const auto& [var, linear1_cts] : var_to_linear1) {
VariableEncodingLocalModel& encoding_model = local_models.emplace_back();
encoding_model.var = var;
encoding_model.linear1_constraints.assign(linear1_cts.begin(),
linear1_cts.end());
encoding_model.constraints_linking_two_encoding_booleans =
var_to_constraints_encoding_or[var];
absl::c_sort(encoding_model.constraints_linking_two_encoding_booleans);
encoding_model.var_in_more_than_one_constraint_outside_the_local_model =
(context->VarToConstraints(var).size() - linear1_cts.size() > 1);
for (const int ct : linear1_cts) {
const int bool_var = PositiveRef(
context->working_model->constraints(ct).enforcement_literal(0));
encoding_model.bools_only_used_inside_the_local_model.insert(bool_var);
var_bool_counts[{var, bool_var}].linear1_count++;
}
absl::erase_if(encoding_model.bools_only_used_inside_the_local_model,
[context, v = var, &var_bool_counts](int bool_var) {
const auto& counts = var_bool_counts[{v, bool_var}];
return context->VarToConstraints(bool_var).size() !=
counts.linear1_count + counts.bool_or_count;
});
auto it = context->ObjectiveMap().find(var);
if (it != context->ObjectiveMap().end()) {
encoding_model.variable_coeff_in_objective = it->second;
}
}
absl::c_sort(local_models, [](const VariableEncodingLocalModel& a,
const VariableEncodingLocalModel& b) {
return a.var < b.var;
});
return local_models;
}
bool BasicPresolveAndGetFullyEncodedDomains(
PresolveContext* context, VariableEncodingLocalModel& local_model,
absl::flat_hash_map<int, Domain>* result, bool* changed) {
*changed = false;
absl::flat_hash_map<int, int> ref_to_linear1;
// Fill ref_to_linear1 and do some basic presolving.
const Domain var_domain = context->DomainOf(local_model.var);
for (const int ct : local_model.linear1_constraints) {
ConstraintProto* ct_proto = context->working_model->mutable_constraints(ct);
DCHECK(ConstraintIsEncodingBound(*ct_proto));
const int ref = ct_proto->enforcement_literal(0);
Domain domain = ReadDomainFromProto(ct_proto->linear());
if (!domain.IsIncludedIn(var_domain)) {
*changed = true;
domain = domain.IntersectionWith(context->DomainOf(local_model.var));
if (domain.IsEmpty()) {
context->UpdateRuleStats(
"variables: linear1 with domain not included in variable domain");
if (!context->SetLiteralToFalse(ref)) {
return false;
}
ct_proto->Clear();
context->UpdateConstraintVariableUsage(ct);
continue;
}
FillDomainInProto(domain, ct_proto->mutable_linear());
}
auto [it, inserted] = ref_to_linear1.insert({ref, ct});
if (!inserted) {
*changed = true;
ConstraintProto* old_ct_proto =
context->working_model->mutable_constraints(it->second);
const Domain old_ct_domain = ReadDomainFromProto(old_ct_proto->linear());
const Domain new_domain = domain.IntersectionWith(old_ct_domain);
ct_proto->Clear();
context->UpdateConstraintVariableUsage(ct);
if (new_domain.IsEmpty()) {
context->UpdateRuleStats(
"variables: linear1 with same variable and enforcement and "
"non-overlapping domain, setting enforcement to false");
if (!context->SetLiteralToFalse(ref)) {
return false;
}
old_ct_proto->Clear();
context->UpdateConstraintVariableUsage(it->second);
ref_to_linear1.erase(ref);
} else {
FillDomainInProto(new_domain, old_ct_proto->mutable_linear());
context->UpdateRuleStats(
"variables: merged two linear1 with same variable and enforcement");
}
}
}
// Remove from the local model anything that was removed in the loop above.
int new_linear1_size = 0;
for (int i = 0; i < local_model.linear1_constraints.size(); ++i) {
const int ct = local_model.linear1_constraints[i];
const ConstraintProto& ct_proto = context->working_model->constraints(ct);
if (ct_proto.constraint_case() != ConstraintProto::kLinear) continue;
if (context->IsFixed(ct_proto.enforcement_literal(0))) {
continue;
}
DCHECK(ConstraintIsEncodingBound(ct_proto));
local_model.linear1_constraints[new_linear1_size++] = ct;
}
if (new_linear1_size != local_model.linear1_constraints.size()) {
*changed = true;
local_model.linear1_constraints.resize(new_linear1_size);
// Rerun the presolve loop to recompute ref_to_linear1.
return true;
}
for (const auto& [ref, ct] : ref_to_linear1) {
auto it = ref_to_linear1.find(NegatedRef(ref));
if (it == ref_to_linear1.end()) continue;
const ConstraintProto& positive_ct =
context->working_model->constraints(ct);
const ConstraintProto& negative_ct =
context->working_model->constraints(it->second);
const Domain positive_domain = ReadDomainFromProto(positive_ct.linear());
const Domain negative_domain = ReadDomainFromProto(negative_ct.linear());
if (!positive_domain.IntersectionWith(negative_domain).IsEmpty()) {
// This is not a fully encoded domain. For example, it could be
// l => x in {-inf,inf}
// ~l => x in {-inf,inf}
// which actually means that `l` doesn't really encode anything.
continue;
}
bool domain_modified = false;
if (!context->IntersectDomainWith(
local_model.var, positive_domain.UnionWith(negative_domain),
&domain_modified)) {
return false;
}
*changed = *changed || domain_modified;
result->insert({ref, positive_domain});
result->insert({NegatedRef(ref), negative_domain});
}
// Now detect a different way of fully encoding a domain:
// l1 => x in D1
// l2 => x in D2
// l3 => x in D3
// ...
// l_n => x in D_n
// bool_or(l1, l2, l3, ..., l_n)
//
// where D1, D2, ..., D_n are non overlapping. This works too for exactly_one.
for (const int ct : local_model.constraints_linking_two_encoding_booleans) {
const ConstraintProto& ct_proto = context->working_model->constraints(ct);
if (ct_proto.constraint_case() != ConstraintProto::kBoolOr &&
ct_proto.constraint_case() != ConstraintProto::kExactlyOne) {
continue;
}
if (!ct_proto.enforcement_literal().empty()) continue;
const BoolArgumentProto& bool_or =
ct_proto.constraint_case() == ConstraintProto::kExactlyOne
? ct_proto.exactly_one()
: ct_proto.bool_or();
if (bool_or.literals().size() < 2) continue;
bool encoding_detected = true;
Domain non_overlapping_domain;
std::vector<std::pair<int, Domain>> ref_and_domains;
for (const int ref : bool_or.literals()) {
auto it = ref_to_linear1.find(ref);
if (it == ref_to_linear1.end()) {
encoding_detected = false;
break;
}
const Domain domain = ReadDomainFromProto(
context->working_model->constraints(it->second).linear());
ref_and_domains.push_back({ref, domain});
if (!non_overlapping_domain.IntersectionWith(domain).IsEmpty()) {
encoding_detected = false;
break;
}
non_overlapping_domain = non_overlapping_domain.UnionWith(domain);
}
if (encoding_detected) {
context->UpdateRuleStats("variables: detected fully encoded domain");
bool domain_modified = false;
if (!context->IntersectDomainWith(local_model.var, non_overlapping_domain,
&domain_modified)) {
return false;
}
if (domain_modified) {
context->UpdateRuleStats(
"variables: restricted domain to fully encoded domain");
}
*changed = *changed || domain_modified;
for (const auto& [ref, domain] : ref_and_domains) {
result->insert({ref, domain});
result->insert({NegatedRef(ref),
var_domain.IntersectionWith(domain.Complement())});
}
// Promote a bool_or to an exactly_one.
if (ct_proto.constraint_case() == ConstraintProto::kBoolOr) {
context->UpdateRuleStats(
"variables: promoted bool_or to exactly_one for fully encoded "
"domain");
std::vector<int> new_enforcement_literals(bool_or.literals().begin(),
bool_or.literals().end());
context->working_model->mutable_constraints(ct)->clear_bool_or();
context->working_model->mutable_constraints(ct)
->mutable_exactly_one()
->mutable_literals()
->Add(new_enforcement_literals.begin(),
new_enforcement_literals.end());
*changed = true;
}
}
}
return true;
}
// Return false on unsat
bool DetectEncodedComplexDomain(
PresolveContext* context, int ct_index,
VariableEncodingLocalModel& local_model,
absl::flat_hash_map<int, Domain>* fully_encoded_domains, bool* changed) {
ConstraintProto* ct = context->working_model->mutable_constraints(ct_index);
*changed = false;
if (context->ModelIsUnsat()) return false;
DCHECK(ct->constraint_case() == ConstraintProto::kAtMostOne ||
ct->constraint_case() == ConstraintProto::kExactlyOne ||
ct->constraint_case() == ConstraintProto::kBoolOr);
// Handling exaclty_one, at_most_one and bool_or is pretty similar. If we have
// l1 <=> v \in D1
// l2 <=> v \in D2
//
// We built
// l <=> v \in (D1 U D2).
//
// Moreover, if we have exactly_one(l1, l2, ...) or at_most_one(l1, l2, ...),
// we know that v cannot be in the intersection of D1 and D2. Thus, we first
// unconditionally remove (D1 ∩ D2) from the domain of v, making
// (l1=true and l2=true) impossible and allowing us to write our clauses as
// exactly_one(l1 or l2, ...) or at_most_one(l1 or l2, ...).
//
// Thus, other than the domain reduction that should not be done for the
// bool_or, all we need is to create a variable
// (l1 or l2) == l <=> (v \in (D1 U D2)).
google::protobuf::RepeatedField<int32_t>& literals =
ct->constraint_case() == ConstraintProto::kAtMostOne
? *ct->mutable_at_most_one()->mutable_literals()
: (ct->constraint_case() == ConstraintProto::kExactlyOne
? *ct->mutable_exactly_one()->mutable_literals()
: *ct->mutable_bool_or()->mutable_literals());
if (literals.size() <= 1) return true;
if (!ct->enforcement_literal().empty()) {
// TODO(user): support this case if it any problem needs it.
return true;
}
// When we have
// lit => var in D1
// ~lit => var in D2
// we can represent this on a line:
//
// ----------------D1----------------
// ----------------D2---------------
// |+++++++++++|*********************|++++++++++|
// lit=false lit unconstrained lit=true
//
// Handling the case where the variable is unconstrained by the lit is a
// bit of a pain: we want to replace two literals in a exactly_one by a
// single one, and if they are both unconstrained we might be forced to pick
// one arbitrarily to set to true. In any case, this is not a proper
// encoding of a complex domain, so we just ignore it.
// TODO(user): This can be implemented if it turns out to be common.
std::optional<int> maybe_lit1;
Domain domain_lit1;
std::optional<int> maybe_lit2;
Domain domain_lit2;
for (const int lit_var : literals) {
if (!local_model.bools_only_used_inside_the_local_model.contains(
PositiveRef(lit_var))) {
continue;
}
auto it = fully_encoded_domains->find(lit_var);
if (it == fully_encoded_domains->end()) {
continue;
}
if (!maybe_lit1) {
maybe_lit1 = lit_var;
domain_lit1 = it->second;
} else {
maybe_lit2 = lit_var;
domain_lit2 = it->second;
break;
}
}
if (!maybe_lit2.has_value()) return true;
DCHECK(maybe_lit1.has_value());
const int lit1 = *maybe_lit1;
const int lit2 = *maybe_lit2;
// We found two literals that each fully encodes an interval and are both only
// used in the encoding and in the bool_or/exactly_one/at_most_one. We can
// thus replace the two literals by their OR. Since this code is already
// rather complex, so we will just simplify a pair of literals at a time, and
// leave for the presolve fixpoint to do the rest.
*changed = true;
context->UpdateRuleStats(
"variables: detected encoding of a complex domain with multiple "
"linear1");
if (ct->constraint_case() != ConstraintProto::kBoolOr) {
// In virtue of the AMO, var must not be in the intersection of the two
// domains where both literals are true.
if (!context->IntersectDomainWith(
local_model.var,
domain_lit2.IntersectionWith(domain_lit1).Complement())) {
return false;
}
}
const Domain var_domain = context->DomainOf(local_model.var);
const Domain domain_new_var_false = var_domain.IntersectionWith(
domain_lit1.Complement().IntersectionWith(domain_lit2.Complement()));
const Domain domain_new_var_true =
var_domain.IntersectionWith(domain_new_var_false.Complement());
// Now we want to build a lit3 = (lit1 or lit2) to use in the AMO/bool_or.
const int new_var = context->NewBoolVarWithClause({lit1, lit2});
if (domain_new_var_true.IsEmpty()) {
CHECK(context->SetLiteralToFalse(new_var));
} else if (domain_new_var_false.IsEmpty()) {
CHECK(context->SetLiteralToTrue(new_var));
} else {
local_model.linear1_constraints.push_back(
context->working_model->constraints_size());
ConstraintProto* new_ct = context->working_model->add_constraints();
new_ct->add_enforcement_literal(new_var);
new_ct->mutable_linear()->add_vars(local_model.var);
new_ct->mutable_linear()->add_coeffs(1);
FillDomainInProto(domain_new_var_true, new_ct->mutable_linear());
local_model.linear1_constraints.push_back(
context->working_model->constraints_size());
new_ct = context->working_model->add_constraints();
new_ct->add_enforcement_literal(NegatedRef(new_var));
new_ct->mutable_linear()->add_vars(local_model.var);
new_ct->mutable_linear()->add_coeffs(1);
FillDomainInProto(domain_new_var_false, new_ct->mutable_linear());
context->UpdateNewConstraintsVariableUsage();
}
// Remove the two literals from the AMO.
int new_size = 0;
for (int i = 0; i < literals.size(); ++i) {
if (literals.Get(i) != lit1 && literals.Get(i) != lit2) {
literals.Set(new_size++, literals.Get(i));
}
}
literals.Truncate(new_size);
literals.Add(new_var);
context->UpdateConstraintVariableUsage(ct_index);
// Finally, move the four linear1 to the mapping model.
fully_encoded_domains->insert({new_var, domain_new_var_true});
fully_encoded_domains->insert({NegatedRef(new_var), domain_new_var_false});
fully_encoded_domains->erase(lit1);
fully_encoded_domains->erase(lit2);
fully_encoded_domains->erase(NegatedRef(lit1));
fully_encoded_domains->erase(NegatedRef(lit2));
context->MarkVariableAsRemoved(PositiveRef(lit1));
context->MarkVariableAsRemoved(PositiveRef(lit2));
int new_linear1_size = 0;
for (int i = 0; i < local_model.linear1_constraints.size(); ++i) {
const int ct = local_model.linear1_constraints[i];
ConstraintProto* ct_proto = context->working_model->mutable_constraints(ct);
if (PositiveRef(ct_proto->enforcement_literal(0)) == PositiveRef(lit1) ||
PositiveRef(ct_proto->enforcement_literal(0)) == PositiveRef(lit2)) {
context->NewMappingConstraint(*ct_proto, __FILE__, __LINE__);
ct_proto->Clear();
context->UpdateConstraintVariableUsage(ct);
continue;
}
local_model.linear1_constraints[new_linear1_size++] = ct;
}
local_model.linear1_constraints.resize(new_linear1_size);
return true;
}
bool DetectAllEncodedComplexDomain(PresolveContext* context,
VariableEncodingLocalModel& local_model) {
absl::flat_hash_map<int, Domain> fully_encoded_domains;
bool changed_on_basic_presolve = false;
if (!BasicPresolveAndGetFullyEncodedDomains(context, local_model,
&fully_encoded_domains,
&changed_on_basic_presolve)) {
return false;
}
if (local_model.constraints_linking_two_encoding_booleans.size() != 1) {
return true;
}
const int ct = local_model.constraints_linking_two_encoding_booleans[0];
bool changed = true;
while (changed) {
if (!DetectEncodedComplexDomain(context, ct, local_model,
&fully_encoded_domains, &changed)) {
return false;
}
}
return true;
}
bool MaybeTransferLinear1ToAnotherVariable(
VariableEncodingLocalModel& local_model, PresolveContext* context) {
if (local_model.var == -1) return true;
@@ -131,6 +700,5 @@ bool MaybeTransferLinear1ToAnotherVariable(
local_model.var = -1;
return true;
}
} // namespace sat
} // namespace operations_research

48
ortools/sat/presolve_encoding.h
View File

@@ -17,7 +17,10 @@
#include <cstdint>
#include <vector>
#include "absl/container/flat_hash_map.h"
#include "absl/container/flat_hash_set.h"
#include "ortools/sat/presolve_context.h"
#include "ortools/util/sorted_interval_list.h"
namespace operations_research {
namespace sat {
@@ -33,6 +36,13 @@ struct VariableEncodingLocalModel {
// fulfilling the conditions above will appear here.
std::vector<int> linear1_constraints;
// Constraints of the form bool_or/exactly_one/at_most_one that contains at
// least two of the encoding booleans.
std::vector<int> constraints_linking_two_encoding_booleans;
// Booleans that do not appear on any constraints outside the local model.
absl::flat_hash_set<int> bools_only_used_inside_the_local_model;
// Zero if `var` doesn't appear in the objective.
int64_t variable_coeff_in_objective = 0;
@@ -44,6 +54,44 @@ struct VariableEncodingLocalModel {
int single_constraint_using_the_var_outside_the_local_model = -1;
};
// For performance, this skips variables that appears in a single linear1 and is
// used in more than another constraint, since there is no interesting presolve
// we can do in this case.
std::vector<VariableEncodingLocalModel> CreateVariableEncodingLocalModels(
PresolveContext* context);
// Do a few simple presolve rules on the local model:
// - restrict the domain of the linear1 to the domain of the variable.
// - merge linear1 over the same enforcement,var pairs.
// - if we have a linear1 for a literal and another for its negation, do
// not allow both to be true.
//
// Also returns a list of literals that fully encodes a domain for the variable.
// Returns false if we prove unsat.
bool BasicPresolveAndGetFullyEncodedDomains(
PresolveContext* context, VariableEncodingLocalModel& local_model,
absl::flat_hash_map<int, Domain>* result, bool* changed);
// If we have a model containing:
// l1 => var in [0, 10]
// ~l1 => var in [11, 20]
// l2 => var in [50, 60]
// ~l2 => var in [70, 80]
// bool_or(l1, l2, ...)
//
// if moreover `l1` and `l2` are only used in the constraints above, we can
// replace them by:
// l3 => var in [0, 10] U [50, 60]
// ~l3 => var in [11, 20] U [70, 80]
// bool_or(l3, ...)
//
// and remove the variables `l1` and `l2`. This also works if we replace the
// bool_or for an at_most_one or an exactly_one, but requires imposing
// (unconditionally) that the variable cannot be both in the domain encoded by
// `l1` and in the domain encoded by `l2`.
bool DetectAllEncodedComplexDomain(PresolveContext* context,
VariableEncodingLocalModel& local_model);
// If we have a bunch of constraint of the form literal => Y \in domain and
// another constraint Y = f(X), we can remove Y, that constraint, and transform
// all linear1 from constraining Y to constraining X.

462
ortools/sat/presolve_encoding_test.cc Normal file
View File

@@ -0,0 +1,462 @@
// Copyright 2010-2025 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#include "ortools/sat/presolve_encoding.h"
#include <vector>
#include "absl/container/flat_hash_map.h"
#include "absl/log/check.h"
#include "gtest/gtest.h"
#include "ortools/base/gmock.h"
#include "ortools/base/parse_test_proto.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/model.h"
#include "ortools/sat/presolve_context.h"
#include "ortools/util/sorted_interval_list.h"
namespace operations_research {
namespace sat {
namespace {
using ::google::protobuf::contrib::parse_proto::ParseTestProto;
using ::testing::ElementsAre;
using ::testing::Pair;
using ::testing::UnorderedElementsAre;
TEST(CreateVariableEncodingLocalModelsTest, TrivialTest) {
CpModelProto model_proto = ParseTestProto(R"pb(
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
constraints {
enforcement_literal: 0
linear {
vars: [ 1 ]
coeffs: [ 1 ]
domain: [ 0, 1 ]
}
}
)pb");
Model model;
CpModelProto mapping_model;
PresolveContext context(&model, &model_proto, &mapping_model);
context.InitializeNewDomains();
context.ReadObjectiveFromProto();
context.UpdateNewConstraintsVariableUsage();
const std::vector<VariableEncodingLocalModel> local_models =
CreateVariableEncodingLocalModels(&context);
ASSERT_EQ(local_models.size(), 1);
ASSERT_EQ(local_models[0].var, 1);
EXPECT_THAT(local_models[0].linear1_constraints, ElementsAre(0));
}
TEST(CreateVariableEncodingLocalModelsTest, BasicTest) {
CpModelProto model_proto = ParseTestProto(R"pb(
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 2 ] }
constraints {
enforcement_literal: 0
linear {
vars: [ 2 ]
coeffs: [ 1 ]
domain: [ 0, 0 ]
}
}
constraints {
enforcement_literal: 1
linear {
vars: [ 2 ]
coeffs: [ 1 ]
domain: [ 0, 0 ]
}
}
constraints { bool_or { literals: [ 0, 1 ] } }
)pb");
Model model;
CpModelProto mapping_model;
PresolveContext context(&model, &model_proto, &mapping_model);
context.InitializeNewDomains();
context.ReadObjectiveFromProto();
context.UpdateNewConstraintsVariableUsage();
const std::vector<VariableEncodingLocalModel> local_models =
CreateVariableEncodingLocalModels(&context);
ASSERT_EQ(local_models.size(), 1);
ASSERT_EQ(local_models[0].var, 2);
EXPECT_THAT(local_models[0].linear1_constraints, ElementsAre(0, 1));
EXPECT_THAT(local_models[0].constraints_linking_two_encoding_booleans,
ElementsAre(2));
EXPECT_THAT(local_models[0].bools_only_used_inside_the_local_model,
UnorderedElementsAre(0, 1));
}
TEST(CreateVariableEncodingLocalModelsTest, OneBooleanUsedElsewhere) {
CpModelProto model_proto = ParseTestProto(R"pb(
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 2 ] }
constraints {
enforcement_literal: 0
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 0, 0 ]
}
}
constraints {
enforcement_literal: 1
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 1, 1 ]
}
}
constraints {
enforcement_literal: 2
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 2, 2 ]
}
}
constraints { bool_or { literals: [ 0, 1, 2 ] } }
constraints { at_most_one { literals: [ 0, 1, 2 ] } }
constraints {
linear {
vars: [ 2, 3 ]
coeffs: [ 1, 1 ]
domain: [ 0, 3 ]
}
}
objective {
vars: [ 1 ]
coeffs: [ 2 ]
}
)pb");
Model model;
CpModelProto mapping_model;
PresolveContext context(&model, &model_proto, &mapping_model);
context.InitializeNewDomains();
context.ReadObjectiveFromProto();
context.UpdateNewConstraintsVariableUsage();
const std::vector<VariableEncodingLocalModel> local_models =
CreateVariableEncodingLocalModels(&context);
ASSERT_EQ(local_models.size(), 1);
ASSERT_EQ(local_models[0].var, 3);
EXPECT_THAT(local_models[0].linear1_constraints, ElementsAre(0, 1, 2));
EXPECT_THAT(local_models[0].constraints_linking_two_encoding_booleans,
ElementsAre(3, 4));
EXPECT_THAT(local_models[0].bools_only_used_inside_the_local_model,
UnorderedElementsAre(0));
}
TEST(CreateVariableEncodingLocalModelsTest, TwoVars) {
CpModelProto model_proto = ParseTestProto(R"pb(
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 2 ] }
variables { domain: [ 0, 2 ] }
variables { domain: [ 0, 1 ] }
constraints {
enforcement_literal: 0
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 0, 0 ]
}
}
constraints {
enforcement_literal: -1
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 1, 1 ]
}
}
constraints {
enforcement_literal: 1
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 1, 1 ]
}
}
constraints {
enforcement_literal: 1
linear {
vars: [ 4 ]
coeffs: [ 1 ]
domain: [ 2, 2 ]
}
}
constraints {
enforcement_literal: 2
linear {
vars: [ 4 ]
coeffs: [ 1 ]
domain: [ 2, 2 ]
}
}
constraints { bool_or { literals: [ 0, 1, 5 ] } }
constraints { at_most_one { literals: [ 0, 1, 2 ] } }
constraints {
linear {
vars: [ 2, 3 ]
coeffs: [ 1, 1 ]
domain: [ 0, 3 ]
}
}
objective {
vars: [ 3 ]
coeffs: [ 2 ]
}
)pb");
Model model;
CpModelProto mapping_model;
PresolveContext context(&model, &model_proto, &mapping_model);
context.InitializeNewDomains();
context.ReadObjectiveFromProto();
context.UpdateNewConstraintsVariableUsage();
std::vector<VariableEncodingLocalModel> local_models =
CreateVariableEncodingLocalModels(&context);
ASSERT_EQ(local_models.size(), 2);
ASSERT_EQ(local_models[0].var, 3);
ASSERT_EQ(local_models[1].var, 4);
EXPECT_THAT(local_models[0].linear1_constraints, ElementsAre(0, 1, 2));
EXPECT_THAT(local_models[1].linear1_constraints, ElementsAre(3, 4));
EXPECT_THAT(local_models[0].constraints_linking_two_encoding_booleans,
ElementsAre(5, 6));
EXPECT_THAT(local_models[1].constraints_linking_two_encoding_booleans,
ElementsAre(6));
EXPECT_THAT(local_models[0].bools_only_used_inside_the_local_model,
UnorderedElementsAre(0));
EXPECT_THAT(local_models[1].bools_only_used_inside_the_local_model,
UnorderedElementsAre());
EXPECT_EQ(local_models[0].variable_coeff_in_objective, 2);
EXPECT_EQ(local_models[1].variable_coeff_in_objective, 0);
absl::flat_hash_map<int, Domain> fully_encoded_domains;
bool changed = false;
CHECK(BasicPresolveAndGetFullyEncodedDomains(
&context, local_models[0], &fully_encoded_domains, &changed));
EXPECT_THAT(
fully_encoded_domains,
UnorderedElementsAre(Pair(0, Domain(0, 0)), Pair(-1, Domain(1, 1))));
}
TEST(BasicPresolveAndGetFullyEncodedDomainsTest, EncodingWithBoolOr) {
CpModelProto model_proto = ParseTestProto(R"pb(
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 2 ] }
variables { domain: [ 0, 2 ] }
constraints {
enforcement_literal: 0
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 0, 0 ]
}
}
constraints {
enforcement_literal: 1
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 1, 1 ]
}
}
constraints {
enforcement_literal: 2
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 2, 2 ]
}
}
constraints {
enforcement_literal: 0
linear {
vars: [ 4 ]
coeffs: [ 1 ]
domain: [ 2, 2 ]
}
}
constraints { bool_or { literals: [ 0, 1, 2 ] } }
constraints {
linear {
vars: [ 2, 3 ]
coeffs: [ 1, 1 ]
domain: [ 0, 3 ]
}
}
objective {
vars: [ 3 ]
coeffs: [ 2 ]
}
)pb");
Model model;
CpModelProto mapping_model;
PresolveContext context(&model, &model_proto, &mapping_model);
context.InitializeNewDomains();
context.ReadObjectiveFromProto();
context.UpdateNewConstraintsVariableUsage();
std::vector<VariableEncodingLocalModel> local_models =
CreateVariableEncodingLocalModels(&context);
absl::flat_hash_map<int, Domain> fully_encoded_domains;
bool changed = false;
CHECK(BasicPresolveAndGetFullyEncodedDomains(
&context, local_models[0], &fully_encoded_domains, &changed));
EXPECT_THAT(fully_encoded_domains,
UnorderedElementsAre(Pair(0, Domain(0)), Pair(1, Domain(1)),
Pair(2, Domain(2)),
Pair(-1, Domain::FromValues({1, 2})),
Pair(-2, Domain::FromValues({0, 2})),
Pair(-3, Domain::FromValues({0, 1}))));
ConstraintProto expected_exactly_one = ParseTestProto(R"pb(
exactly_one { literals: [ 0, 1, 2 ] }
)pb");
EXPECT_THAT(context.working_model->constraints(),
testing::Contains(testing::EqualsProto(expected_exactly_one)));
}
TEST(DetectAllEncodedComplexDomainTest, BasicTest) {
CpModelProto model_proto = ParseTestProto(R"pb(
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 5 ] }
variables { domain: [ 0, 2 ] }
constraints {
enforcement_literal: 0
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 0, 1 ]
}
}
constraints {
enforcement_literal: -1
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 2, 5 ]
}
}
# Note that the var=3 is missing from both this encoding and its negation.
constraints {
enforcement_literal: 1
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 1, 2 ]
}
}
constraints {
enforcement_literal: -2
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 0, 0, 4, 5 ]
}
}
constraints {
enforcement_literal: 2
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 2, 2 ]
}
}
constraints { at_most_one { literals: [ 0, 1, 2 ] } }
constraints {
linear {
vars: [ 2, 3 ]
coeffs: [ 1, 1 ]
domain: [ 0, 3 ]
}
}
objective {
vars: [ 3 ]
coeffs: [ 2 ]
}
)pb");
Model model;
CpModelProto mapping_model;
PresolveContext context(&model, &model_proto, &mapping_model);
context.InitializeNewDomains();
context.ReadObjectiveFromProto();
context.UpdateNewConstraintsVariableUsage();
std::vector<VariableEncodingLocalModel> local_models =
CreateVariableEncodingLocalModels(&context);
ASSERT_TRUE(DetectAllEncodedComplexDomain(&context, local_models[0]));
context.WriteVariableDomainsToProto();
const CpModelProto expected_model = ParseTestProto(R"pb(
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
# var=1 is forbidden by the at_most_one
variables { domain: [ 0, 0, 2, 2, 4, 5 ] }
variables { domain: [ 0, 2 ] }
variables { domain: [ 0, 1 ] }
constraints {}
constraints {}
constraints {}
constraints {}
constraints {
enforcement_literal: 2
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 2, 2 ]
}
}
constraints { at_most_one { literals: [ 2, 5 ] } }
constraints {
linear {
vars: [ 2, 3 ]
coeffs: [ 1, 1 ]
domain: [ 0, 3 ]
}
}
constraints {
enforcement_literal: 5
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 0, 0, 2, 2 ]
}
}
constraints {
enforcement_literal: -6
linear {
vars: [ 3 ]
coeffs: [ 1 ]
domain: [ 4, 5 ]
}
}
objective {
vars: [ 3 ]
coeffs: [ 2 ]
}
)pb");
EXPECT_THAT(context.working_model, testing::EqualsProto(expected_model));
}
} // namespace
} // namespace sat
} // namespace operations_research

6
ortools/sat/sat_parameters.proto
View File

@@ -24,7 +24,7 @@ option java_multiple_files = true;
// Contains the definitions for all the sat algorithm parameters and their
// default values.
//
// NEXT TAG: 355
// NEXT TAG: 356
message SatParameters {
// In some context, like in a portfolio of search, it makes sense to name a
// given parameters set for logging purpose.
@@ -153,6 +153,10 @@ message SatParameters {
// clause with it.
optional int32 eagerly_subsume_last_n_conflicts = 343 [default = 4];
// If we remove clause that we now are "implied" by others. Note that this
// might not always be good as we might loose some propagation power.
optional bool subsume_during_vivification = 355 [default = true];
// If true, try to backtrack as little as possible on conflict and re-imply
// the clauses later.
// This means we discard less propagation than traditional backjumping, but

6
ortools/sat/stat_tables.cc
View File

@@ -120,7 +120,8 @@ void SharedStatTables::AddClausesStat(absl::string_view name, Model* model) {
if (vivify_table_.empty()) {
vivify_table_.push_back({"Vivification", "Clauses", "Decisions", "LitTrue",
"Subsumed", "LitRemoved", "DecisionReused"});
"Subsumed", "LitRemoved", "DecisionReused",
"Conflicts"});
}
vivify_table_.push_back({FormatName(name),
FormatCounter(vivify_counters.num_clauses_vivified),
@@ -128,7 +129,8 @@ void SharedStatTables::AddClausesStat(absl::string_view name, Model* model) {
FormatCounter(vivify_counters.num_true),
FormatCounter(vivify_counters.num_subsumed),
FormatCounter(vivify_counters.num_removed_literals),
FormatCounter(vivify_counters.num_reused)});
FormatCounter(vivify_counters.num_reused),
FormatCounter(vivify_counters.num_conflicts)});
// Track reductions of Boolean variables.
if (bool_var_table_.empty()) {

92
ortools/sat/vivification.cc
View File

@@ -18,8 +18,10 @@
#include <vector>
#include "absl/algorithm/container.h"
#include "absl/cleanup/cleanup.h"
#include "absl/container/btree_set.h"
#include "absl/log/check.h"
#include "absl/log/log.h"
#include "absl/types/span.h"
#include "ortools/sat/clause.h"
#include "ortools/sat/sat_base.h"
@@ -31,7 +33,7 @@ namespace operations_research::sat {
bool Vivifier::MinimizeByPropagation(bool log_info, double dtime_budget,
bool minimize_new_clauses_only) {
PresolveTimer timer("Vivification", logger_, time_limit_);
timer.OverrideLogging(log_info);
timer.OverrideLogging(log_info || VLOG_IS_ON(2));
sat_solver_->AdvanceDeterministicTime(time_limit_);
const double threshold =
@@ -44,34 +46,34 @@ bool Vivifier::MinimizeByPropagation(bool log_info, double dtime_budget,
// Tricky: we don't want TryToMinimizeClause() to delete to_minimize
// while we are processing it.
sat_solver_->BlockClauseDeletion(true);
absl::Cleanup unblock_clause_deletion = [&] {
sat_solver_->BlockClauseDeletion(false);
};
const auto old_counter = counters_;
int num_resets = 0;
while (!time_limit_->LimitReached() &&
time_limit_->GetElapsedDeterministicTime() < threshold) {
SatClause* to_minimize = clause_manager_->NextNewClauseToMinimize();
if (!minimize_new_clauses_only && to_minimize == nullptr) {
to_minimize = clause_manager_->NextClauseToMinimize();
}
if (to_minimize != nullptr) {
if (!TryToMinimizeClause(to_minimize)) {
sat_solver_->BlockClauseDeletion(false);
return false;
}
} else if (minimize_new_clauses_only) {
break;
} else {
++num_resets;
if (log_info) {
SOLVER_LOG(logger_,
"Minimized all clauses, restarting from first one.");
}
clause_manager_->ResetToMinimizeIndex();
if (num_resets > 1) break;
}
const int num_resets = clause_manager_->NumToMinimizeIndexResets();
while (!time_limit_->LimitReached()) {
// Abort if we used our budget.
sat_solver_->AdvanceDeterministicTime(time_limit_);
if (time_limit_->GetElapsedDeterministicTime() >= threshold) break;
// Also abort if we did more than one loop over all the clause.
if (clause_manager_->NumToMinimizeIndexResets() > num_resets + 1) break;
// First minimize clauses that where never minimized before.
{
SatClause* to_minimize = clause_manager_->NextNewClauseToMinimize();
if (to_minimize != nullptr) {
if (!TryToMinimizeClause(to_minimize)) return false;
continue;
}
if (minimize_new_clauses_only) break; // We are done.
}
SatClause* clause = clause_manager_->NextClauseToMinimize();
if (clause != nullptr) {
if (!TryToMinimizeClause(clause)) return false;
}
}
// Note(user): In some corner cases, the function above might find a
@@ -85,8 +87,8 @@ bool Vivifier::MinimizeByPropagation(bool log_info, double dtime_budget,
counters_.num_removed_literals - old_counter.num_removed_literals;
timer.AddCounter("num_vivifed", last_num_vivified_);
timer.AddCounter("literals_removed", last_num_literals_removed_);
timer.AddCounter("loops", clause_manager_->NumToMinimizeIndexResets());
sat_solver_->BlockClauseDeletion(false);
clause_manager_->DeleteRemovedClauses();
return result;
}
@@ -171,6 +173,7 @@ bool Vivifier::SubsumptionIsInteresting(BooleanVariable variable,
// that we can reuse the trail from previous calls in case there are overlaps.
bool Vivifier::TryToMinimizeClause(SatClause* clause) {
CHECK(clause != nullptr);
if (clause->empty()) return true;
++counters_.num_clauses_vivified;
// TODO(user): Make sure clause do not contain any redundant literal before
@@ -229,8 +232,10 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) {
}
CHECK_EQ(candidate.size(), clause->size());
if (!sat_solver_->BacktrackAndPropagateReimplications(longest_valid_prefix))
if (!sat_solver_->BacktrackAndPropagateReimplications(longest_valid_prefix)) {
return false;
}
absl::btree_set<LiteralIndex> moved_last;
while (!sat_solver_->ModelIsUnsat()) {
// We want each literal in candidate to appear last once in our propagation
@@ -240,8 +245,9 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) {
const int target_level = MoveOneUnprocessedLiteralLast(
moved_last, sat_solver_->CurrentDecisionLevel(), &candidate);
if (target_level == -1) break;
if (!sat_solver_->BacktrackAndPropagateReimplications(target_level))
if (!sat_solver_->BacktrackAndPropagateReimplications(target_level)) {
return false;
}
fixed_false_literals.clear();
fixed_true_literal = kNoLiteralIndex;
@@ -273,9 +279,8 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) {
// Replace the clause with the reason for the literal being true, plus
// the literal itself.
candidate.clear();
for (Literal lit : sat_solver_->GetDecisionsFixing(
trail_->Reason(literal.Variable()))) {
candidate.push_back(lit.Negated());
for (const Literal l : sat_solver_->GetDecisionsFixing({literal})) {
candidate.push_back(l.Negated());
}
} else {
candidate.resize(variable_level);
@@ -289,7 +294,8 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) {
// clauses. If we can subsume this clause by making only 1 additional
// clause permanent and that clause is no longer than this one, we will
// do so.
if (clause_manager_->ReasonClauseOrNull(literal.Variable()) != clause &&
if (parameters_.subsume_during_vivification() &&
clause_manager_->ReasonClauseOrNull(literal.Variable()) != clause &&
SubsumptionIsInteresting(literal.Variable(), candidate.size())) {
counters_.num_subsumed++;
counters_.num_removed_literals += clause->size();
@@ -305,7 +311,10 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) {
sat_solver_->EnqueueDecisionAndBackjumpOnConflict(literal.Negated());
if (sat_solver_->ModelIsUnsat()) return false;
if (clause->IsRemoved()) return true;
if (sat_solver_->CurrentDecisionLevel() < level) {
++counters_.num_conflicts;
// There was a conflict, consider the conflicting literal next so we
// should be able to exploit the conflict in the next iteration.
// TODO(user): I *think* this is sufficient to ensure pushing
@@ -321,6 +330,9 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) {
sat_solver_->NotifyThatModelIsUnsat();
return false;
}
// TODO(user): To use this, we need to proove and rewrite the clause
// on each of its modification.
if (!parameters_.inprocessing_minimization_use_all_orderings()) break;
moved_last.insert(candidate.back().Index());
}
@@ -396,15 +408,11 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) {
sat_solver_->NotifyThatModelIsUnsat();
return false;
}
// Adding a unit clause can cause additional propagation, but there is also an
// edge case where binary_clauses_->PropagationIsDone() may return
// false after we add the first binary clause, even if nothing has been added
// to the trail. Either way, we can just check if the implication graph thinks
// it is done to propagate only when required.
if (!binary_clauses_->PropagationIsDone(*trail_)) {
return sat_solver_->FinishPropagation();
}
return true;
// Adding a unit clause can cause additional propagation. There is also an
// edge case where we added the first binary clause of the model by
// strenghtening a normal clause.
return sat_solver_->FinishPropagation();
}
} // namespace operations_research::sat

4
ortools/sat/vivification.h
View File

@@ -45,6 +45,7 @@ class Vivifier {
trail_(model->GetOrCreate<Trail>()),
binary_clauses_(model->GetOrCreate<BinaryImplicationGraph>()),
clause_manager_(model->GetOrCreate<ClauseManager>()),
clause_id_generator_(model->GetOrCreate<ClauseIdGenerator>()),
lrat_proof_handler_(model->Mutable<LratProofHandler>()) {}
// Minimize a batch of clauses using propagation.
@@ -67,6 +68,7 @@ class Vivifier {
int64_t num_subsumed = 0;
int64_t num_removed_literals = 0;
int64_t num_reused = 0;
int64_t num_conflicts = 0;
};
Counters counters() const { return counters_; }
@@ -92,7 +94,7 @@ class Vivifier {
Trail* trail_;
BinaryImplicationGraph* binary_clauses_;
ClauseManager* clause_manager_;
ClauseIdGenerator* clause_id_generator_;
LratProofHandler* lrat_proof_handler_ = nullptr;
Counters counters_;

9
ortools/sat/work_assignment.cc
View File

@@ -301,7 +301,6 @@ bool SharedTreeManager::SyncTree(ProtoTrail& path) {
// We don't rely on these being empty, but we expect them to be.
DCHECK(to_close_.empty());
DCHECK(to_update_.empty());
path.NormalizeImplications();
int prev_level = -1;
for (const auto& [node, level] : nodes) {
if (level == prev_level) {
@@ -1367,6 +1366,8 @@ bool SharedTreeWorker::SyncWithSharedTree() {
!decision_policy_->GetBestPartialAssignment().empty()) {
assigned_tree_.ClearTargetPhase();
for (Literal lit : decision_policy_->GetBestPartialAssignment()) {
// Skip anything assigned at level 0.
if (trail_->Assignment().LiteralIsAssigned(lit)) continue;
// If `lit` was last assigned at a shared level, it is implied in the
// tree, no need to share its phase.
if (trail_->Info(lit.Variable()).level <= assigned_tree_.MaxLevel()) {
@@ -1396,6 +1397,12 @@ bool SharedTreeWorker::SyncWithSharedTree() {
decision_policy_->SetTargetPolarityIfUnassigned(DecodeDecision(lit));
}
decision_policy_->ResetActivitiesToFollowBestPartialAssignment();
// This seems bizzare after just setting the best partial assignment,
// but this makes phase sharing work even when there is no stable phase in
// the restart strategy, and makes no real difference if there is, since
// the first dive will still try to follow this assignment until the first
// conflict regardless of the restart strategy.
decision_policy_->ClearBestPartialAssignment();
}
}
// If we commit to this subtree, keep it for at least 1s of dtime.

4
ortools/util/logging.cc
View File

@@ -112,6 +112,8 @@ void SolverLogger::FlushPendingThrottledLogs(bool ignore_rates) {
PresolveTimer::~PresolveTimer() {
time_limit_->AdvanceDeterministicTime(work_);
const double dtime =
time_limit_->GetElapsedDeterministicTime() - dtime_at_start_;
std::string counter_string;
for (const auto& [counter_name, count] : counters_) {
@@ -124,7 +126,7 @@ PresolveTimer::~PresolveTimer() {
logger_->LogInfo(
__FILE__, __LINE__,
absl::StrCat(absl::StrFormat(" %.2es", timer_.Get()),
absl::StrFormat(" %.2ed", work_),
absl::StrFormat(" %.2ed", dtime),
(WorkLimitIsReached() ? " *" : " "), "[", name_, "]",
counter_string, " ", absl::StrJoin(extra_infos_, " ")));
}

6
ortools/util/logging.h
View File

@@ -127,7 +127,10 @@ class SolverLogger {
class PresolveTimer {
public:
PresolveTimer(std::string name, SolverLogger* logger, TimeLimit* time_limit)
: name_(std::move(name)), logger_(logger), time_limit_(time_limit) {
: name_(std::move(name)),
dtime_at_start_(time_limit->GetElapsedDeterministicTime()),
logger_(logger),
time_limit_(time_limit) {
timer_.Start();
}
@@ -164,6 +167,7 @@ class PresolveTimer {
private:
const std::string name_;
const double dtime_at_start_;
WallTimer timer_;
SolverLogger* logger_;