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

[CP-SAT] fix sharing bug where some fixed Boolean variables were not shared; use new no_overlap_2d propagator in scheduling workers; improve probing code

Browse Source
This commit is contained in:
Laurent Perron
2023-12-06 14:15:16 +01:00
parent e91de5dac5
commit 47fcebdea6
14 changed files with 214 additions and 100 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
ortools/sat/clause.cc
View File

@@ -535,6 +535,8 @@ bool BinaryImplicationGraph::AddBinaryClause(Literal a, Literal b) {
is_dag_ = false;
num_implications_ += 2;
if (enable_sharing_ && add_callback_ != nullptr) add_callback_(a, b);
const auto& assignment = trail_->Assignment();
if (trail_->CurrentDecisionLevel() == 0) {
DCHECK(!assignment.LiteralIsAssigned(a));

16
ortools/sat/clause.h
View File

@@ -526,6 +526,19 @@ class BinaryImplicationGraph : public SatPropagator {
return AddBinaryClause(a.Negated(), b);
}
// When set, the callback will be called on ALL newly added binary clauses.
//
// The EnableSharing() function can be used to disable sharing temporarily for
// the clauses that are imported from the Shared repository already.
//
// TODO(user): this is meant to share clause between workers, hopefully the
// contention will not be too high. Double check and maybe add a batch version
// were we keep new implication and add them in batches.
void EnableSharing(bool enable) { enable_sharing_ = enable; }
void SetAdditionCallback(std::function<void(Literal, Literal)> f) {
add_callback_ = f;
}
// An at most one constraint of size n is a compact way to encode n * (n - 1)
// implications. This must only be called at level zero.
//
@@ -892,6 +905,9 @@ class BinaryImplicationGraph : public SatPropagator {
// For RemoveFixedVariables().
int num_processed_fixed_variables_ = 0;
bool enable_sharing_ = true;
std::function<void(Literal, Literal)> add_callback_ = nullptr;
};
extern template std::vector<Literal>

1
ortools/sat/cp_model_search.cc
View File

@@ -168,6 +168,7 @@ void AddDualSchedulingHeuristics(SatParameters& new_params) {
new_params.set_use_pairwise_reasoning_in_no_overlap_2d(true);
new_params.set_use_timetabling_in_no_overlap_2d(true);
new_params.set_use_energetic_reasoning_in_no_overlap_2d(true);
new_params.set_use_area_energetic_reasoning_in_no_overlap_2d(true);
}
// We want a random tie breaking among variables with equivalent values.

50
ortools/sat/cp_model_solver.cc
View File

@@ -35,7 +35,6 @@
#include "ortools/base/timer.h"
#include "ortools/sat/intervals.h"
#if !defined(__PORTABLE_PLATFORM__)
#include "ortools/base/file.h"
#include "ortools/base/helpers.h"
#include "ortools/base/options.h"
#endif // __PORTABLE_PLATFORM__
@@ -1128,6 +1127,7 @@ void RegisterVariableBoundsLevelZeroExport(
std::vector<int64_t> new_lower_bounds;
std::vector<int64_t> new_upper_bounds;
absl::flat_hash_set<int> visited_variables;
const std::string name = model->Name();
auto broadcast_level_zero_bounds =
[=](const std::vector<IntegerVariable>& modified_vars) mutable {
@@ -1218,12 +1218,15 @@ void RegisterVariableBoundsLevelZeroImport(
const CpModelProto& model_proto, SharedBoundsManager* shared_bounds_manager,
Model* model) {
CHECK(shared_bounds_manager != nullptr);
const std::string name = model->Name();
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
CpModelMapping* const mapping = model->GetOrCreate<CpModelMapping>();
auto* sat_solver = model->GetOrCreate<SatSolver>();
auto* mapping = model->GetOrCreate<CpModelMapping>();
const int id = shared_bounds_manager->RegisterNewId();
const auto& import_level_zero_bounds = [&model_proto, shared_bounds_manager,
model, integer_trail, id, mapping]() {
name, sat_solver, integer_trail, id,
mapping]() {
std::vector<int> model_variables;
std::vector<int64_t> new_lower_bounds;
std::vector<int64_t> new_upper_bounds;
@@ -1232,8 +1235,19 @@ void RegisterVariableBoundsLevelZeroImport(
bool new_bounds_have_been_imported = false;
for (int i = 0; i < model_variables.size(); ++i) {
const int model_var = model_variables[i];
// This can happen if a boolean variables is forced to have an
// integer view in one thread, and not in another thread.
// If this is a Boolean, fix it if not already done.
if (mapping->IsBoolean(model_var)) {
Literal lit = mapping->Literal(model_var);
if (new_upper_bounds[i] == 0) lit = lit.Negated();
if (!sat_solver->Assignment().LiteralIsAssigned(lit)) {
new_bounds_have_been_imported = true;
}
if (!sat_solver->AddUnitClause(lit)) return false;
continue;
}
// Deal with integer.
if (!mapping->IsInteger(model_var)) continue;
const IntegerVariable var = mapping->Integer(model_var);
const IntegerValue new_lb(new_lower_bounds[i]);
@@ -1252,9 +1266,9 @@ void RegisterVariableBoundsLevelZeroImport(
var_proto.name().empty()
? absl::StrCat("anonymous_var(", model_var, ")")
: var_proto.name();
LOG(INFO) << " '" << model->Name() << "' imports new bounds for "
<< var_name << ": from [" << old_lb << ", " << old_ub
<< "] to [" << new_lb << ", " << new_ub << "]";
LOG(INFO) << " '" << name << "' imports new bounds for " << var_name
<< ": from [" << old_lb << ", " << old_ub << "] to ["
<< new_lb << ", " << new_ub << "]";
}
if (changed_lb &&
@@ -1268,8 +1282,7 @@ void RegisterVariableBoundsLevelZeroImport(
return false;
}
}
if (new_bounds_have_been_imported &&
!model->GetOrCreate<SatSolver>()->FinishPropagation()) {
if (new_bounds_have_been_imported && !sat_solver->FinishPropagation()) {
return false;
}
return true;
@@ -1361,12 +1374,11 @@ void RegisterObjectiveBoundsImport(
import_objective_bounds);
}
// Registers a callback that will export non-problem clauses added during
// Registers a callback that will export binary clauses discovered during
// search.
void RegisterClausesExport(int id, SharedClausesManager* shared_clauses_manager,
Model* model) {
auto* mapping = model->GetOrCreate<CpModelMapping>();
auto* sat_solver = model->GetOrCreate<SatSolver>();
const auto& share_binary_clause = [mapping, id, shared_clauses_manager](
Literal l1, Literal l2) {
const int var1 =
@@ -1379,7 +1391,8 @@ void RegisterClausesExport(int id, SharedClausesManager* shared_clauses_manager,
const int lit2 = l2.IsPositive() ? var2 : NegatedRef(var2);
shared_clauses_manager->AddBinaryClause(id, lit1, lit2);
};
sat_solver->SetShareBinaryClauseCallback(share_binary_clause);
model->GetOrCreate<BinaryImplicationGraph>()->SetAdditionCallback(
share_binary_clause);
}
// Registers a callback to import new clauses stored in the
@@ -1393,11 +1406,13 @@ int RegisterClausesLevelZeroImport(int id,
Model* model) {
CHECK(shared_clauses_manager != nullptr);
CpModelMapping* const mapping = model->GetOrCreate<CpModelMapping>();
SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
auto* sat_solver = model->GetOrCreate<SatSolver>();
auto* implications = model->GetOrCreate<BinaryImplicationGraph>();
const auto& import_level_zero_clauses = [shared_clauses_manager, id, mapping,
sat_solver]() {
sat_solver, implications]() {
std::vector<std::pair<int, int>> new_binary_clauses;
shared_clauses_manager->GetUnseenBinaryClauses(id, &new_binary_clauses);
implications->EnableSharing(false);
for (const auto& [ref1, ref2] : new_binary_clauses) {
const Literal l1 = mapping->Literal(ref1);
const Literal l2 = mapping->Literal(ref2);
@@ -1405,6 +1420,7 @@ int RegisterClausesLevelZeroImport(int id,
return false;
}
}
implications->EnableSharing(true);
return true;
};
model->GetOrCreate<LevelZeroCallbackHelper>()->callbacks.push_back(
@@ -2366,8 +2382,7 @@ class FullProblemSolver : public SubSolver {
}
// Note that this is done after the loading, so we will never export
// problem clauses. We currently also never export binary clauses added
// by the initial probing.
// problem clauses.
if (shared_->clauses != nullptr) {
const int id = shared_->clauses->RegisterNewId();
shared_->clauses->SetWorkerNameForId(id, local_model_.Name());
@@ -3118,6 +3133,7 @@ void SolveCpModelParallel(const CpModelProto& model_proto,
if (params.share_level_zero_bounds()) {
shared.bounds = std::make_unique<SharedBoundsManager>(model_proto);
shared.bounds->set_dump_prefix(absl::GetFlag(FLAGS_cp_model_dump_prefix));
shared.bounds->LoadDebugSolution(
global_model->GetOrCreate<SharedResponseManager>()->DebugSolution());
}

118
ortools/sat/integer_search.cc
View File

@@ -1618,11 +1618,17 @@ SatSolver::Status ContinuousProber::Probe() {
sat_solver_->NotifyThatModelIsUnsat();
return sat_solver_->UnsatStatus();
}
if (parameters_.minimize_with_propagation_ratio() > 0.0 &&
!sat_solver_->MinimizeByPropagation()) {
sat_solver_->NotifyThatModelIsUnsat();
return sat_solver_->UnsatStatus();
}
// Store current statistics to detect an iteration without any improvement.
const int64_t initial_num_literals_fixed =
prober_->num_new_literals_fixed();
const int64_t initial_num_bounds_shaved = num_bounds_shaved_;
const auto& assignment = sat_solver_->Assignment();
// Probe variable bounds.
// TODO(user): Probe optional variables.
@@ -1672,7 +1678,7 @@ SatSolver::Status ContinuousProber::Probe() {
for (; current_bool_var_ < bool_vars_.size(); ++current_bool_var_) {
const BooleanVariable& bool_var = bool_vars_[current_bool_var_];
if (sat_solver_->Assignment().VariableIsAssigned(bool_var)) continue;
if (assignment.VariableIsAssigned(bool_var)) continue;
const auto [_, inserted] = probed_bool_vars_.insert(bool_var);
if (!inserted) continue;
@@ -1683,8 +1689,7 @@ SatSolver::Status ContinuousProber::Probe() {
num_literals_probed_++;
const Literal literal(bool_var, true);
if (use_shaving_ &&
!sat_solver_->Assignment().LiteralIsAssigned(literal)) {
if (use_shaving_ && !assignment.LiteralIsAssigned(literal)) {
const SatSolver::Status true_status = ShaveLiteral(literal);
if (ReportStatus(true_status)) return true_status;
if (true_status == SatSolver::ASSUMPTIONS_UNSAT) continue;
@@ -1698,9 +1703,9 @@ SatSolver::Status ContinuousProber::Probe() {
if (parameters_.use_extended_probing()) {
const auto at_least_one_literal_is_true =
[this](absl::Span<const Literal> literals) {
[&assignment](absl::Span<const Literal> literals) {
for (const Literal literal : literals) {
if (sat_solver_->Assignment().LiteralIsTrue(literal)) {
if (assignment.LiteralIsTrue(literal)) {
return true;
}
}
@@ -1715,7 +1720,7 @@ SatSolver::Status ContinuousProber::Probe() {
tmp_dnf_.clear();
for (const Literal literal : clause->AsSpan()) {
if (sat_solver_->Assignment().LiteralIsAssigned(literal)) continue;
if (assignment.LiteralIsAssigned(literal)) continue;
tmp_dnf_.push_back({literal});
}
++num_at_least_one_probed_;
@@ -1736,7 +1741,7 @@ SatSolver::Status ContinuousProber::Probe() {
tmp_dnf_.clear();
tmp_literals_.clear();
for (const Literal literal : at_most_one) {
if (sat_solver_->Assignment().LiteralIsAssigned(literal)) continue;
if (assignment.LiteralIsAssigned(literal)) continue;
tmp_dnf_.push_back({literal});
tmp_literals_.push_back(literal.Negated());
}
@@ -1750,15 +1755,19 @@ SatSolver::Status ContinuousProber::Probe() {
}
// Probe combinations of Booleans variables.
// TODO(user): Probe until something is imported, or learned.
if (bool_vars_.size() < 1000) {
const int limit = parameters_.probing_num_combinations_limit();
const bool max_num_bool_vars_for_pairs_probing =
static_cast<int>(std::sqrt(2 * limit));
const int num_bool_vars = bool_vars_.size();
if (num_bool_vars < max_num_bool_vars_for_pairs_probing) {
for (; current_bv1_ + 1 < bool_vars_.size(); ++current_bv1_) {
const BooleanVariable bv1 = bool_vars_[current_bv1_];
if (sat_solver_->Assignment().VariableIsAssigned(bv1)) continue;
if (assignment.VariableIsAssigned(bv1)) continue;
current_bv2_ = std::max(current_bv1_ + 1, current_bv2_);
for (; current_bv2_ < bool_vars_.size(); ++current_bv2_) {
const BooleanVariable& bv2 = bool_vars_[current_bv2_];
if (sat_solver_->Assignment().VariableIsAssigned(bv2)) continue;
if (assignment.VariableIsAssigned(bv2)) continue;
if (!prober_->ProbeDnf(
"pair_of_bool_vars",
{{Literal(bv1, true), Literal(bv2, true)},
@@ -1772,14 +1781,14 @@ SatSolver::Status ContinuousProber::Probe() {
current_bv2_ = 0;
}
} else {
for (; random_pair_of_bool_vars_probed_ < 5000;
for (; random_pair_of_bool_vars_probed_ < 10000;
++random_pair_of_bool_vars_probed_) {
const BooleanVariable bv1 =
bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
if (sat_solver_->Assignment().VariableIsAssigned(bv1)) continue;
if (assignment.VariableIsAssigned(bv1)) continue;
const BooleanVariable bv2 =
bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
if (sat_solver_->Assignment().VariableIsAssigned(bv2) || bv1 == bv2) {
if (assignment.VariableIsAssigned(bv2) || bv1 == bv2) {
continue;
}
if (!prober_->ProbeDnf(
@@ -1794,22 +1803,56 @@ SatSolver::Status ContinuousProber::Probe() {
RETURN_IF_NOT_FEASIBLE(PeriodicSyncAndCheck());
}
}
// Note that the product is always >= 0.
const bool max_num_bool_vars_for_triplet_probing =
static_cast<int>(std::cbrt(2 * limit));
// We use a limit to make sure we do not overflow.
const int loop_limit =
num_bool_vars < max_num_bool_vars_for_triplet_probing
? num_bool_vars * (num_bool_vars - 1) * (num_bool_vars - 2) / 2
: limit;
for (; random_triplet_of_bool_vars_probed_ < loop_limit;
++random_triplet_of_bool_vars_probed_) {
const BooleanVariable bv1 =
bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
if (assignment.VariableIsAssigned(bv1)) continue;
const BooleanVariable bv2 =
bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
if (assignment.VariableIsAssigned(bv2) || bv1 == bv2) {
continue;
}
const BooleanVariable bv3 =
bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
if (assignment.VariableIsAssigned(bv3) || bv1 == bv3 || bv2 == bv3) {
continue;
}
tmp_dnf_.clear();
for (int i = 0; i < 8; ++i) {
tmp_dnf_.push_back({Literal(bv1, (i & 1) > 0),
Literal(bv2, (i & 2) > 0),
Literal(bv3, (i & 4) > 0)});
}
if (!prober_->ProbeDnf("rnd_triplet_of_bool_vars", tmp_dnf_)) {
return SatSolver::INFEASIBLE;
}
RETURN_IF_NOT_FEASIBLE(PeriodicSyncAndCheck());
}
}
// Adjust the active_limit.
{
if (use_shaving_) {
const double deterministic_time =
parameters_.shaving_search_deterministic_time();
const bool something_has_been_detected =
num_bounds_shaved_ != initial_num_bounds_shaved ||
prober_->num_new_literals_fixed() != initial_num_literals_fixed;
if (something_has_been_detected) { // Reset the limit.
active_limit_ = deterministic_time;
} else if (active_limit_ <
25 * deterministic_time) { // Bump the limit.
active_limit_ += deterministic_time;
}
if (use_shaving_) {
const double deterministic_time =
parameters_.shaving_search_deterministic_time();
const bool something_has_been_detected =
num_bounds_shaved_ != initial_num_bounds_shaved ||
prober_->num_new_literals_fixed() != initial_num_literals_fixed;
if (something_has_been_detected) { // Reset the limit.
active_limit_ = deterministic_time;
} else if (active_limit_ < 25 * deterministic_time) { // Bump the limit.
active_limit_ += deterministic_time;
}
}
@@ -1820,10 +1863,11 @@ SatSolver::Status ContinuousProber::Probe() {
current_bv1_ = 0;
current_bv2_ = 1;
random_pair_of_bool_vars_probed_ = 0;
random_triplet_of_bool_vars_probed_ = 0;
binary_implication_graph_->ResetAtMostOneIterator();
literal_watchers_->ResetToProbeIndex();
probed_bool_vars_.clear();
probed_literals_.clear();
shaved_literals_.clear();
const int new_trail_index = trail_->Index();
const int new_integer_trail_index = integer_trail_->Index();
@@ -1837,22 +1881,22 @@ SatSolver::Status ContinuousProber::Probe() {
integer_trail_index_at_start_of_iteration_ = new_integer_trail_index;
// Remove fixed Boolean variables.
int size = 0;
int new_size = 0;
for (int i = 0; i < bool_vars_.size(); ++i) {
if (!sat_solver_->Assignment().VariableIsAssigned(bool_vars_[i])) {
bool_vars_[size++] = bool_vars_[i];
bool_vars_[new_size++] = bool_vars_[i];
}
}
bool_vars_.resize(size);
bool_vars_.resize(new_size);
// Remove fixed integer variables.
size = 0;
new_size = 0;
for (int i = 0; i < int_vars_.size(); ++i) {
if (!integer_trail_->IsFixed(int_vars_[i])) {
int_vars_[size++] = int_vars_[i];
int_vars_[new_size++] = int_vars_[i];
}
}
int_vars_.resize(size);
int_vars_.resize(new_size);
}
return SatSolver::LIMIT_REACHED;
}
@@ -1861,8 +1905,8 @@ SatSolver::Status ContinuousProber::Probe() {
SatSolver::Status ContinuousProber::PeriodicSyncAndCheck() {
// Check limit.
if (--num_probes_remaining_ <= 0) {
num_probes_remaining_ = kTestLimitPeriod;
if (--num_test_limit_remaining_ <= 0) {
num_test_limit_remaining_ = kTestLimitPeriod;
if (time_limit_->LimitReached()) return SatSolver::LIMIT_REACHED;
}
@@ -1888,7 +1932,7 @@ SatSolver::Status ContinuousProber::PeriodicSyncAndCheck() {
}
SatSolver::Status ContinuousProber::ShaveLiteral(Literal literal) {
const auto [_, inserted] = probed_literals_.insert(literal.Index());
const auto [_, inserted] = shaved_literals_.insert(literal.Index());
if (trail_->Assignment().LiteralIsAssigned(literal) || !inserted) {
return SatSolver::LIMIT_REACHED;
}

7
ortools/sat/integer_search.h
View File

@@ -328,7 +328,7 @@ class ContinuousProber {
SatSolver::Status Probe();
private:
static const int kTestLimitPeriod = 50;
static const int kTestLimitPeriod = 20;
static const int kLogPeriod = 1000;
static const int kSyncPeriod = 50;
@@ -368,7 +368,7 @@ class ContinuousProber {
// Period counters;
int num_logs_remaining_ = 0;
int num_syncs_remaining_ = 0;
int num_probes_remaining_ = 0;
int num_test_limit_remaining_ = 0;
// Shaving management.
bool use_shaving_ = false;
@@ -379,13 +379,14 @@ class ContinuousProber {
double active_limit_;
// TODO(user): use 2 vector<bool>.
absl::flat_hash_set<BooleanVariable> probed_bool_vars_;
absl::flat_hash_set<LiteralIndex> probed_literals_;
absl::flat_hash_set<LiteralIndex> shaved_literals_;
int iteration_ = 1;
int current_int_var_ = 0;
int current_bool_var_ = 0;
int current_bv1_ = 0;
int current_bv2_ = 0;
int random_pair_of_bool_vars_probed_ = 0;
int random_triplet_of_bool_vars_probed_ = 0;
std::vector<std::vector<Literal>> tmp_dnf_;
std::vector<Literal> tmp_literals_;
};

4
ortools/sat/max_hs.cc
View File

@@ -33,7 +33,7 @@
#include "ortools/base/strong_vector.h"
#include "ortools/sat/presolve_util.h"
#if !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP)
#include "ortools/linear_solver/linear_solver.h"
#include "ortools/linear_solver/solve_mp_model.h"
#endif // __PORTABLE_PLATFORM__
#include "ortools/linear_solver/linear_solver.pb.h"
#include "ortools/sat/cp_model.pb.h"
@@ -577,7 +577,7 @@ SatSolver::Status HittingSetOptimizer::Optimize() {
TightenMpModel();
// TODO(user): C^c is broken when using SCIP.
MPSolver::SolveWithProto(request_, &response_);
response_ = SolveMPModel(request_);
if (response_.status() != MPSolverResponseStatus::MPSOLVER_OPTIMAL) {
// We currently abort if we have a non-optimal result.
// This is correct if we had a limit reached, but not in the other

2
ortools/sat/probing.cc
View File

@@ -501,7 +501,7 @@ bool LookForTrivialSatSolution(double deterministic_time_limit, Model* model,
bool FailedLiteralProbingRound(ProbingOptions options, Model* model) {
WallTimer wall_timer;
wall_timer.Start();
options.log_info |= VLOG_IS_ON(1);
options.log_info |= VLOG_IS_ON(2);
// Reset the solver in case it was already used.
auto* sat_solver = model->GetOrCreate<SatSolver>();

7
ortools/sat/sat_parameters.proto
View File

@@ -23,7 +23,7 @@ option csharp_namespace = "Google.OrTools.Sat";
// Contains the definitions for all the sat algorithm parameters and their
// default values.
//
// NEXT TAG: 272
// NEXT TAG: 273
message SatParameters {
// In some context, like in a portfolio of search, it makes sense to name a
// given parameters set for logging purpose.
@@ -441,7 +441,7 @@ message SatParameters {
//
// TODO(user): Clean up. The first one is used in CP-SAT, the other in pure
// SAT presolve.
optional double probing_deterministic_time_limit = 226 [default = 1];
optional double probing_deterministic_time_limit = 226 [default = 1.0];
optional double presolve_probing_deterministic_time_limit = 57
[default = 30.0];
@@ -1044,6 +1044,9 @@ message SatParameters {
// Use extended probing (probe bool_or, at_most_one, exactly_one).
optional bool use_extended_probing = 269 [default = true];
// How many combinations of pairs or triplets of variables we want to scan.
optional int32 probing_num_combinations_limit = 272 [default = 20000];
// Add a shaving phase (where the solver tries to prove that the lower or
// upper bound of a variable are infeasible) to the probing search.
optional bool use_shaving_in_probing_search = 204 [default = true];

30
ortools/sat/sat_runner.cc
View File

@@ -22,6 +22,7 @@
#include "absl/log/initialize.h"
#include "absl/strings/match.h"
#include "absl/strings/string_view.h"
#include "google/protobuf/arena.h"
#include "google/protobuf/text_format.h"
#include "ortools/base/helpers.h"
#include "ortools/base/logging.h"
@@ -43,6 +44,11 @@ ABSL_FLAG(
".cnf (sat, max-sat, weighted max-sat), .opb (pseudo-boolean sat/optim) "
"and by default the CpModelProto proto (binary or text).");
ABSL_FLAG(
std::string, hint_file, "",
"Protobuf file containing a CpModelResponse. The solution will be used as a"
" hint to bootstrap the search.");
ABSL_FLAG(std::string, output, "",
"If non-empty, write the response there. By default it uses the "
"binary format except if the file extension is '.txt'.");
@@ -77,7 +83,8 @@ std::string ExtractName(absl::string_view full_filename) {
return filename;
}
bool LoadProblem(const std::string& filename, CpModelProto* cp_model) {
bool LoadProblem(const std::string& filename, const std::string& hint_file,
CpModelProto* cp_model) {
if (absl::EndsWith(filename, ".opb") ||
absl::EndsWith(filename, ".opb.bz2")) {
OpbReader reader;
@@ -100,9 +107,27 @@ bool LoadProblem(const std::string& filename, CpModelProto* cp_model) {
LOG(INFO) << "Reading a CpModelProto.";
CHECK_OK(ReadFileToProto(filename, cp_model));
}
// Read the hint file.
if (!hint_file.empty()) {
CpSolverResponse response;
LOG(INFO) << "Reading a CpSolverResponse.";
CHECK_OK(ReadFileToProto(hint_file, &response));
CHECK_EQ(response.solution_size(), cp_model->variables_size())
<< "The hint proto is not compatible with the model proto";
cp_model->clear_solution_hint();
for (int i = 0; i < cp_model->variables_size(); ++i) {
cp_model->mutable_solution_hint()->add_vars(i);
cp_model->mutable_solution_hint()->add_values(response.solution(i));
}
}
// Set the name if not present.
if (cp_model->name().empty()) {
cp_model->set_name(ExtractName(filename));
}
return true;
}
@@ -124,7 +149,8 @@ int Run() {
google::protobuf::Arena arena;
CpModelProto* cp_model =
google::protobuf::Arena::CreateMessage<CpModelProto>(&arena);
if (!LoadProblem(absl::GetFlag(FLAGS_input), cp_model)) {
if (!LoadProblem(absl::GetFlag(FLAGS_input), absl::GetFlag(FLAGS_hint_file),
cp_model)) {
CpSolverResponse response;
response.set_status(CpSolverStatus::MODEL_INVALID);
return EXIT_SUCCESS;

19
ortools/sat/sat_solver.cc
View File

@@ -270,8 +270,7 @@ bool SatSolver::AddProblemClauseInternal(absl::Span<const Literal> literals) {
// Always true.
return true;
} else {
AddBinaryClauseInternal(literals[0], literals[1],
/*export_clause=*/false);
AddBinaryClauseInternal(literals[0], literals[1]);
}
} else {
if (!clauses_propagator_->AddClause(literals, trail_)) {
@@ -424,9 +423,6 @@ int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
// This clause MUST be knew, otherwise something is wrong.
CHECK(binary_clauses_.Add(BinaryClause(literals[0], literals[1])));
}
if (shared_binary_clauses_callback_ != nullptr) {
shared_binary_clauses_callback_(literals[0], literals[1]);
}
CHECK(binary_implication_graph_->AddBinaryClause(literals[0], literals[1]));
return /*lbd=*/2;
}
@@ -497,17 +493,12 @@ void SatSolver::SaveDebugAssignment() {
}
}
void SatSolver::AddBinaryClauseInternal(Literal a, Literal b,
bool export_clause) {
void SatSolver::AddBinaryClauseInternal(Literal a, Literal b) {
if (track_binary_clauses_) {
// Abort if this clause was already added.
if (!binary_clauses_.Add(BinaryClause(a, b))) return;
}
if (export_clause && shared_binary_clauses_callback_ != nullptr) {
shared_binary_clauses_callback_(a, b);
}
if (!binary_implication_graph_->AddBinaryClause(a, b)) {
CHECK_EQ(CurrentDecisionLevel(), 0);
SetModelUnsat();
@@ -1202,6 +1193,7 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) {
if (target_level == -1) break;
Backtrack(target_level);
while (CurrentDecisionLevel() < candidate.size()) {
if (time_limit_->LimitReached()) return;
const int level = CurrentDecisionLevel();
const Literal literal = candidate[level];
if (Assignment().LiteralIsFalse(literal)) {
@@ -1278,7 +1270,7 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) {
counters_.minimization_num_removed_literals += clause->size() - 2;
// The order is important for the drat proof.
AddBinaryClauseInternal(candidate[0], candidate[1], /*export_clause=*/true);
AddBinaryClauseInternal(candidate[0], candidate[1]);
clauses_propagator_->Detach(clause);
// This is needed in the corner case where this was the first binary clause
@@ -1787,8 +1779,7 @@ void SatSolver::ProcessNewlyFixedVariables() {
// This clause is now a binary clause, treat it separately. Note that
// it is safe to do that because this clause can't be used as a reason
// since we are at level zero and the clause is not satisfied.
AddBinaryClauseInternal(clause->FirstLiteral(), clause->SecondLiteral(),
/*export_clause=*/true);
AddBinaryClauseInternal(clause->FirstLiteral(), clause->SecondLiteral());
clauses_propagator_->LazyDetach(clause);
++num_binary;
continue;

14
ortools/sat/sat_solver.h
View File

@@ -482,12 +482,6 @@ class SatSolver {
void ResetMinimizationByPropagationThreshold();
bool MinimizeByPropagation();
// Sets the export function to the shared clauses manager.
void SetShareBinaryClauseCallback(const std::function<void(Literal, Literal)>&
shared_binary_clauses_callback) {
shared_binary_clauses_callback_ = shared_binary_clauses_callback;
}
// Advance the given time limit with all the deterministic time that was
// elapsed since last call.
void AdvanceDeterministicTime(TimeLimit* limit) {
@@ -523,10 +517,7 @@ class SatSolver {
// Adds a binary clause to the BinaryImplicationGraph and to the
// BinaryClauseManager when track_binary_clauses_ is true.
//
// If export_clause is true, then we will also export_clause that to a
// potential shared_binary_clauses_callback_.
void AddBinaryClauseInternal(Literal a, Literal b, bool export_clause);
void AddBinaryClauseInternal(Literal a, Literal b);
// See SaveDebugAssignment(). Note that these functions only consider the
// variables at the time the debug_assignment_ was saved. If new variables
@@ -886,9 +877,6 @@ class SatSolver {
DratProofHandler* drat_proof_handler_;
mutable StatsGroup stats_;
std::function<void(Literal, Literal)> shared_binary_clauses_callback_ =
nullptr;
};
// Tries to minimize the given UNSAT core with a really simple heuristic.

35
ortools/sat/synchronization.cc
View File

@@ -40,8 +40,6 @@
#include "absl/strings/str_format.h"
#include "absl/strings/string_view.h"
#include "absl/synchronization/mutex.h"
#include "absl/time/clock.h"
#include "absl/time/time.h"
#include "absl/types/span.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_utils.h"
@@ -59,6 +57,10 @@
ABSL_FLAG(bool, cp_model_dump_solutions, false,
"DEBUG ONLY. If true, all the intermediate solution will be dumped "
"under '\"FLAGS_cp_model_dump_prefix\" + \"solution_xxx.pb.txt\"'.");
ABSL_FLAG(bool, cp_model_dump_tightened_models, false,
"DEBUG ONLY. If true, dump tightened models incoporating all bounds "
"changes under '\"FLAGS_cp_model_dump_prefix\" + "
"\"tight_model_xxx.pb.txt\"'.");
namespace operations_research {
namespace sat {
@@ -304,7 +306,7 @@ void SharedResponseManager::UpdateInnerObjectiveBounds(
if (lb > inner_objective_lower_bound_) {
// When the improving problem is infeasible, it is possible to report
// arbitrary high inner_objective_lower_bound_. We make sure it never cross
// the current best solution, so that we always report globablly valid lower
// the current best solution, so that we always report globally valid lower
// bound.
DCHECK_LE(inner_objective_upper_bound_, best_solution_objective_value_);
inner_objective_lower_bound_ =
@@ -686,7 +688,7 @@ void SharedResponseManager::NewSolution(
absl::StrCat(dump_prefix_, "solution_", num_solutions_, ".pb.txt");
LOG(INFO) << "Dumping solution to '" << file << "'.";
// Note that here we only want to dump the non-postsolved solution.
// Note that here we only want to dump the non-post-solved solution.
// This is only used for debugging.
CpSolverResponse response;
response.mutable_solution()->Assign(solution_values.begin(),
@@ -819,7 +821,24 @@ void SharedBoundsManager::ReportPotentialNewBounds(
num_improvements++;
}
if (num_improvements > 0) {
total_num_improvements_ += num_improvements;
VLOG(3) << total_num_improvements_ << "/" << num_variables_;
bounds_exported_[worker_name] += num_improvements;
if (absl::GetFlag(FLAGS_cp_model_dump_tightened_models)) {
CpModelProto tight_model = model_proto_;
for (int i = 0; i < num_variables_; ++i) {
IntegerVariableProto* var_proto = tight_model.mutable_variables(i);
const Domain domain =
ReadDomainFromProto(*var_proto)
.IntersectionWith(Domain(lower_bounds_[i], upper_bounds_[i]));
FillDomainInProto(domain, var_proto);
}
const std::string filename = absl::StrCat(dump_prefix_, "tighened_model_",
export_counter_, ".pb.txt");
LOG(INFO) << "Dumping tightened model proto to '" << filename << "'.";
export_counter_++;
CHECK(WriteModelProtoToFile(tight_model, filename));
}
}
}
@@ -964,15 +983,16 @@ void SharedClausesManager::SetWorkerNameForId(int id,
}
void SharedClausesManager::AddBinaryClause(int id, int lit1, int lit2) {
absl::MutexLock mutex_lock(&mutex_);
if (lit2 < lit1) std::swap(lit1, lit2);
const auto p = std::make_pair(lit1, lit2);
absl::MutexLock mutex_lock(&mutex_);
const auto [unused_it, inserted] = added_binary_clauses_set_.insert(p);
if (inserted) {
added_binary_clauses_.push_back(p);
if (always_synchronize_) ++last_visible_clause_;
id_to_clauses_exported_[id]++;
// Small optim. If the worker is already up to date with clauses to import,
// we can mark this new clause as already seen.
if (id_to_last_processed_binary_clause_[id] ==
@@ -987,9 +1007,6 @@ void SharedClausesManager::GetUnseenBinaryClauses(
new_clauses->clear();
absl::MutexLock mutex_lock(&mutex_);
const int last_binary_clause_seen = id_to_last_processed_binary_clause_[id];
// Protects against the optim that increase the last_binary_clause_seen in
// AddBinaryClause(). Checks is nothing needs to be done.
if (last_binary_clause_seen >= last_visible_clause_) return;
new_clauses->assign(added_binary_clauses_.begin() + last_binary_clause_seen,

9
ortools/sat/synchronization.h
View File

@@ -510,6 +510,11 @@ class SharedBoundsManager {
debug_solution_.assign(solution.begin(), solution.end());
}
// Debug only. Set dump prefix for solutions written to file.
void set_dump_prefix(absl::string_view dump_prefix) {
dump_prefix_ = dump_prefix;
}
private:
const int num_variables_;
const CpModelProto& model_proto_;
@@ -521,6 +526,7 @@ class SharedBoundsManager {
std::vector<int64_t> upper_bounds_ ABSL_GUARDED_BY(mutex_);
SparseBitset<int> changed_variables_since_last_synchronize_
ABSL_GUARDED_BY(mutex_);
int64_t total_num_improvements_ ABSL_GUARDED_BY(mutex_) = 0;
// These are only updated on Synchronize().
std::vector<int64_t> synchronized_lower_bounds_ ABSL_GUARDED_BY(mutex_);
@@ -530,6 +536,8 @@ class SharedBoundsManager {
absl::btree_map<std::string, int> bounds_exported_ ABSL_GUARDED_BY(mutex_);
std::vector<int64_t> debug_solution_;
std::string dump_prefix_;
int export_counter_ = 0;
};
// This class holds all the binary clauses that were found and shared by the
@@ -563,6 +571,7 @@ class SharedClausesManager {
private:
absl::Mutex mutex_;
// Cache to avoid adding the same clause twice.
absl::flat_hash_set<std::pair<int, int>> added_binary_clauses_set_
ABSL_GUARDED_BY(mutex_);