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

[CP-SAT] code cleaning; add probing info to the log

Browse Source
This commit is contained in:
Laurent Perron
2022-01-26 15:54:33 +01:00
parent efba255b7c
commit f339e626bd
13 changed files with 170 additions and 132 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
ortools/sat/clause.cc
View File

@@ -508,7 +508,11 @@ void BinaryImplicationGraph::AddBinaryClause(Literal a, Literal b) {
bool BinaryImplicationGraph::AddBinaryClauseDuringSearch(Literal a, Literal b) {
SCOPED_TIME_STAT(&stats_);
if (num_implications_ == 0) propagation_trail_index_ = trail_->Index();
// Tricky: If this is the first clause, the propagator will be added and
// assumed to be in a "propagated" state. This makes sure this is the case.
if (IsEmpty()) propagation_trail_index_ = trail_->Index();
AddBinaryClause(a, b);
const auto& assignment = trail_->Assignment();

12
ortools/sat/clause.h
View File

@@ -51,10 +51,10 @@ namespace sat {
// indirection.
class SatClause {
public:
// Creates a sat clause. There must be at least 2 literals. Smaller clause are
// treated separatly and never constructed. In practice, we do use
// BinaryImplicationGraph for the clause of size 2, so this is mainly used for
// size at least 3.
// Creates a sat clause. There must be at least 2 literals.
// Clause with one literal fix variable directly and are never constructed.
// Note that in practice, we use BinaryImplicationGraph for the clause of size
// 2, so this is used for size at least 3.
static SatClause* Create(absl::Span<const Literal> literals);
// Non-sized delete because this is a tail-padded class.
@@ -357,9 +357,7 @@ class LiteralWatchers : public SatPropagator {
// pointers. We currently do not use std::unique_ptr<SatClause> because it
// can't be used with some STL algorithms like std::partition.
//
// Note that the unit clauses are not kept here and if the parameter
// treat_binary_clauses_separately is true, the binary clause are not kept
// here either.
// Note that the unit clauses and binary clause are not kept here.
std::vector<SatClause*> clauses_;
int to_minimize_index_ = 0;

1
ortools/sat/cp_model_lns.cc
View File

@@ -312,6 +312,7 @@ void NeighborhoodGeneratorHelper::RecomputeHelperData() {
}
}
shared_response_->LogMessage(
"Model",
absl::StrCat("var:", active_variables_.size(), "/", num_variables,
" constraints:", simplied_model_proto_.constraints().size(),
"/", model_proto_.constraints().size(), compo_message));

4
ortools/sat/cp_model_solver.cc
View File

@@ -2048,6 +2048,10 @@ class FullProblemSolver : public SubSolver {
shared->incomplete_solutions);
}
if (shared->bounds != nullptr) {
local_model_->Register<SharedBoundsManager>(shared->bounds);
}
if (shared->clauses != nullptr) {
local_model_->Register<SharedClausesManager>(shared->clauses);
}

20
ortools/sat/integer_search.cc
View File

@@ -19,6 +19,7 @@
#include <vector>
#include "absl/container/flat_hash_set.h"
#include "absl/time/time.h"
#include "absl/types/span.h"
#include "ortools/sat/cp_model_mapping.h"
#include "ortools/sat/implied_bounds.h"
@@ -1094,14 +1095,29 @@ SatSolver::Status ContinuousProbing(
const SatParameters& sat_parameters = *(model->GetOrCreate<SatParameters>());
auto* level_zero_callbacks = model->GetOrCreate<LevelZeroCallbackHelper>();
Prober* prober = model->GetOrCreate<Prober>();
auto* shared_response_manager = model->Mutable<SharedResponseManager>();
auto* shared_bounds_manager = model->Mutable<SharedBoundsManager>();
std::vector<BooleanVariable> active_vars;
std::vector<BooleanVariable> integer_bounds;
absl::flat_hash_set<BooleanVariable> integer_bounds_set;
int loop = 0;
int iteration = 1;
absl::Time last_check = absl::Now();
while (!time_limit->LimitReached()) {
VLOG(2) << "Probing loop " << loop++;
if (shared_response_manager != nullptr &&
shared_bounds_manager != nullptr &&
absl::Now() - last_check >= absl::Seconds(10)) {
shared_response_manager->LogMessage(
"Probe",
absl::StrCat("#iterations:", iteration,
" #literals_fixed:", prober->num_new_literals_fixed(),
" #new_integer_bounds:",
shared_bounds_manager->NumBoundsExported("probing")));
last_check = absl::Now();
}
iteration++;
// Sync the bounds first.
auto SyncBounds = [solver, &level_zero_callbacks]() {

1
ortools/sat/integer_search.h
View File

@@ -30,6 +30,7 @@
#include "ortools/sat/pseudo_costs.h"
#include "ortools/sat/sat_base.h"
#include "ortools/sat/sat_solver.h"
#include "ortools/sat/synchronization.h"
namespace operations_research {
namespace sat {

26
ortools/sat/probing.cc
View File

@@ -13,6 +13,7 @@
#include "ortools/sat/probing.h"
#include <algorithm>
#include <cstdint>
#include <set>
@@ -179,11 +180,6 @@ bool Prober::ProbeOneVariableInternal(BooleanVariable b) {
}
bool Prober::ProbeOneVariable(BooleanVariable b) {
// Reset statistics.
num_new_binary_ = 0;
num_new_holes_ = 0;
num_new_integer_bounds_ = 0;
// Resize the propagated sparse bitset.
const int num_variables = sat_solver_->NumVariables();
propagated_.ClearAndResize(LiteralIndex(2 * num_variables));
@@ -192,7 +188,13 @@ bool Prober::ProbeOneVariable(BooleanVariable b) {
sat_solver_->SetAssumptionLevel(0);
if (!sat_solver_->RestoreSolverToAssumptionLevel()) return false;
return ProbeOneVariableInternal(b);
const int initial_num_fixed = sat_solver_->LiteralTrail().Index();
if (!ProbeOneVariableInternal(b)) return false;
// Statistics
const int num_fixed = sat_solver_->LiteralTrail().Index();
num_new_literals_fixed_ += num_fixed - initial_num_fixed;
return true;
}
bool Prober::ProbeBooleanVariables(
@@ -205,6 +207,7 @@ bool Prober::ProbeBooleanVariables(
num_new_binary_ = 0;
num_new_holes_ = 0;
num_new_integer_bounds_ = 0;
num_new_literals_fixed_ = 0;
// Resize the propagated sparse bitset.
const int num_variables = sat_solver_->NumVariables();
@@ -243,19 +246,22 @@ bool Prober::ProbeBooleanVariables(
}
}
// Update stats.
const int num_fixed = sat_solver_->LiteralTrail().Index();
num_new_literals_fixed_ = num_fixed - initial_num_fixed;
// Display stats.
if (logger_->LoggingIsEnabled()) {
const double time_diff =
time_limit_->GetElapsedDeterministicTime() - initial_deterministic_time;
const int num_fixed = sat_solver_->LiteralTrail().Index();
const int num_newly_fixed = num_fixed - initial_num_fixed;
SOLVER_LOG(logger_, "[Probing] deterministic_time: ", time_diff,
" (limit: ", deterministic_time_limit,
") wall_time: ", wall_timer.Get(), " (",
(limit_reached ? "Aborted " : ""), num_probed, "/",
bool_vars.size(), ")");
if (num_newly_fixed > 0) {
SOLVER_LOG(logger_, "[Probing] - new fixed Boolean: ", num_newly_fixed,
if (num_new_literals_fixed_ > 0) {
SOLVER_LOG(logger_,
"[Probing] - new fixed Boolean: ", num_new_literals_fixed_,
" (", num_fixed, "/", sat_solver_->NumVariables(), ")");
}
if (num_new_holes_ > 0) {

6
ortools/sat/probing.h
View File

@@ -72,6 +72,11 @@ class Prober {
bool ProbeOneVariable(BooleanVariable b);
// Statistics.
// They are reset each time ProbleBooleanVariables() is called.
// Note however that we do not reset them on a call to ProbeOneVariable().
int num_new_literals_fixed() const { return num_new_literals_fixed_; }
private:
bool ProbeOneVariableInternal(BooleanVariable b);
@@ -98,6 +103,7 @@ class Prober {
int num_new_holes_ = 0;
int num_new_binary_ = 0;
int num_new_integer_bounds_ = 0;
int num_new_literals_fixed_ = 0;
// Logger.
SolverLogger* logger_;

6
ortools/sat/sat_parameters.proto
View File

@@ -129,7 +129,6 @@ message SatParameters {
[default = RECURSIVE];
// Whether to expoit the binary clause to minimize learned clauses further.
// This will have an effect only if treat_binary_clauses_separately is true.
enum BinaryMinizationAlgorithm {
NO_BINARY_MINIMIZATION = 0;
BINARY_MINIMIZATION_FIRST = 1;
@@ -360,11 +359,6 @@ message SatParameters {
// Other parameters
// ==========================================================================
// If true, the binary clauses are treated separately from the others. This
// should be faster and uses less memory. However it changes the propagation
// order.
optional bool treat_binary_clauses_separately = 33 [default = true];
// At the beginning of each solve, the random number generator used in some
// part of the solver is reinitialized to this seed. If you change the random
// seed, the solver may make different choices during the solving process.

185
ortools/sat/sat_solver.cc
View File

@@ -138,16 +138,11 @@ bool SatSolver::AddClauseDuringSearch(absl::Span<const Literal> literals) {
if (literals.empty()) return SetModelUnsat();
if (literals.size() == 1) return AddUnitClause(literals[0]);
if (literals.size() == 2) {
const bool init = binary_implication_graph_->num_implications() == 0;
if (!binary_implication_graph_->AddBinaryClauseDuringSearch(literals[0],
literals[1])) {
CHECK_EQ(CurrentDecisionLevel(), 0);
return SetModelUnsat();
}
if (init) {
// This is needed because we just added the first binary clause.
InitializePropagators();
}
} else {
if (!clauses_propagator_->AddClause(literals)) {
CHECK_EQ(CurrentDecisionLevel(), 0);
@@ -163,82 +158,68 @@ bool SatSolver::AddClauseDuringSearch(absl::Span<const Literal> literals) {
}
bool SatSolver::AddUnitClause(Literal true_literal) {
SCOPED_TIME_STAT(&stats_);
CHECK_EQ(CurrentDecisionLevel(), 0);
if (model_is_unsat_) return false;
if (trail_->Assignment().LiteralIsFalse(true_literal)) return SetModelUnsat();
if (trail_->Assignment().LiteralIsTrue(true_literal)) return true;
if (drat_proof_handler_ != nullptr) {
// Note that we will output problem unit clauses twice, but that is a small
// price to pay for having a single variable fixing API.
drat_proof_handler_->AddClause({true_literal});
}
trail_->EnqueueWithUnitReason(true_literal);
if (!Propagate()) return SetModelUnsat();
return true;
return AddProblemClause({true_literal});
}
bool SatSolver::AddBinaryClause(Literal a, Literal b) {
SCOPED_TIME_STAT(&stats_);
tmp_pb_constraint_.clear();
tmp_pb_constraint_.push_back(LiteralWithCoeff(a, 1));
tmp_pb_constraint_.push_back(LiteralWithCoeff(b, 1));
return AddLinearConstraint(
/*use_lower_bound=*/true, /*lower_bound=*/Coefficient(1),
/*use_upper_bound=*/false, /*upper_bound=*/Coefficient(0),
&tmp_pb_constraint_);
return AddProblemClause({a, b});
}
bool SatSolver::AddTernaryClause(Literal a, Literal b, Literal c) {
SCOPED_TIME_STAT(&stats_);
tmp_pb_constraint_.clear();
tmp_pb_constraint_.push_back(LiteralWithCoeff(a, 1));
tmp_pb_constraint_.push_back(LiteralWithCoeff(b, 1));
tmp_pb_constraint_.push_back(LiteralWithCoeff(c, 1));
return AddLinearConstraint(
/*use_lower_bound=*/true, /*lower_bound=*/Coefficient(1),
/*use_upper_bound=*/false, /*upper_bound=*/Coefficient(0),
&tmp_pb_constraint_);
return AddProblemClause({a, b, c});
}
bool SatSolver::AddProblemClause(absl::Span<const Literal> literals) {
SCOPED_TIME_STAT(&stats_);
CHECK_EQ(CurrentDecisionLevel(), 0);
if (model_is_unsat_) return false;
// TODO(user): To avoid duplication, we currently just call
// AddLinearConstraint(). Make a faster specific version if that becomes a
// performance issue.
tmp_pb_constraint_.clear();
for (Literal lit : literals) {
tmp_pb_constraint_.push_back(LiteralWithCoeff(lit, 1));
// Filter already assigned literals.
literals_scratchpad_.clear();
for (const Literal l : literals) {
if (trail_->Assignment().LiteralIsTrue(l)) return true;
if (trail_->Assignment().LiteralIsFalse(l)) continue;
literals_scratchpad_.push_back(l);
}
return AddLinearConstraint(
/*use_lower_bound=*/true, /*lower_bound=*/Coefficient(1),
/*use_upper_bound=*/false, /*upper_bound=*/Coefficient(0),
&tmp_pb_constraint_);
AddProblemClauseInternal(literals_scratchpad_);
// Tricky: The PropagationIsDone() condition shouldn't change anything for a
// pure SAT problem, however in the CP-SAT context, calling Propagate() can
// tigger computation (like the LP) even if no domain changed since the last
// call. We do not want to do that.
if (!PropagationIsDone() && !Propagate()) {
return SetModelUnsat();
}
return true;
}
bool SatSolver::AddProblemClauseInternal(absl::Span<const Literal> literals) {
SCOPED_TIME_STAT(&stats_);
CHECK_EQ(CurrentDecisionLevel(), 0);
// Deals with clause of size 0 (always false) and 1 (set a literal) right away
// so we guarantee that a SatClause is always of size greater than one. This
// simplifies the code.
CHECK_GT(literals.size(), 0);
if (literals.size() == 1) {
if (trail_->Assignment().LiteralIsFalse(literals[0])) return false;
if (trail_->Assignment().LiteralIsTrue(literals[0])) return true;
trail_->EnqueueWithUnitReason(literals[0]); // Not assigned.
return true;
if (DEBUG_MODE) {
CHECK_EQ(CurrentDecisionLevel(), 0);
for (const Literal l : literals) {
CHECK(!trail_->Assignment().LiteralIsAssigned(l));
}
}
if (parameters_->treat_binary_clauses_separately() && literals.size() == 2) {
if (literals.empty()) return SetModelUnsat();
if (literals.size() == 1) {
if (drat_proof_handler_ != nullptr) {
// Note that we will output problem unit clauses twice, but that is a
// small price to pay for having a single variable fixing API.
drat_proof_handler_->AddClause({literals[0]});
}
trail_->EnqueueWithUnitReason(literals[0]);
} else if (literals.size() == 2) {
AddBinaryClauseInternal(literals[0], literals[1]);
} else {
if (!clauses_propagator_->AddClause(literals, trail_)) {
return SetModelUnsat();
}
}
return true;
}
@@ -271,8 +252,7 @@ bool SatSolver::AddLinearConstraintInternal(
// Detect at most one constraints. Note that this use the fact that the
// coefficient are sorted.
if (parameters_->treat_binary_clauses_separately() &&
!parameters_->use_pb_resolution() && max_coeff <= rhs &&
if (!parameters_->use_pb_resolution() && max_coeff <= rhs &&
2 * min_coeff > rhs) {
literals_scratchpad_.clear();
for (const LiteralWithCoeff& term : cst) {
@@ -281,10 +261,6 @@ bool SatSolver::AddLinearConstraintInternal(
if (!binary_implication_graph_->AddAtMostOne(literals_scratchpad_)) {
return SetModelUnsat();
}
// In case this is the first constraint in the binary_implication_graph_.
// TODO(user): refactor so this is not needed!
InitializePropagators();
return true;
}
@@ -292,20 +268,12 @@ bool SatSolver::AddLinearConstraintInternal(
// TODO(user): If this constraint forces all its literal to false (when rhs is
// zero for instance), we still add it. Optimize this?
const bool result = pb_constraints_->AddConstraint(cst, rhs, trail_);
InitializePropagators();
return result;
return pb_constraints_->AddConstraint(cst, rhs, trail_);
}
bool SatSolver::AddLinearConstraint(bool use_lower_bound,
Coefficient lower_bound,
bool use_upper_bound,
Coefficient upper_bound,
std::vector<LiteralWithCoeff>* cst) {
SCOPED_TIME_STAT(&stats_);
CHECK_EQ(CurrentDecisionLevel(), 0);
if (model_is_unsat_) return false;
void SatSolver::CanonicalizeLinear(std::vector<LiteralWithCoeff>* cst,
Coefficient* bound_shift,
Coefficient* max_value) {
// This block removes assigned literals from the constraint.
Coefficient fixed_variable_shift(0);
{
@@ -322,22 +290,43 @@ bool SatSolver::AddLinearConstraint(bool use_lower_bound,
cst->resize(index);
}
// Canonicalize the constraint.
// Now we canonicalize.
// TODO(user): fix variables that must be true/false and remove them.
Coefficient bound_shift;
Coefficient max_value;
CHECK(ComputeBooleanLinearExpressionCanonicalForm(cst, &bound_shift,
&max_value));
CHECK(SafeAddInto(fixed_variable_shift, &bound_shift));
Coefficient bound_delta(0);
CHECK(ComputeBooleanLinearExpressionCanonicalForm(cst, &bound_delta,
max_value));
CHECK(SafeAddInto(bound_delta, bound_shift));
CHECK(SafeAddInto(fixed_variable_shift, bound_shift));
}
bool SatSolver::AddLinearConstraint(bool use_lower_bound,
Coefficient lower_bound,
bool use_upper_bound,
Coefficient upper_bound,
std::vector<LiteralWithCoeff>* cst) {
SCOPED_TIME_STAT(&stats_);
CHECK_EQ(CurrentDecisionLevel(), 0);
if (model_is_unsat_) return false;
Coefficient bound_shift(0);
if (use_upper_bound) {
Coefficient max_value(0);
CanonicalizeLinear(cst, &bound_shift, &max_value);
const Coefficient rhs =
ComputeCanonicalRhs(upper_bound, bound_shift, max_value);
if (!AddLinearConstraintInternal(*cst, rhs, max_value)) {
return SetModelUnsat();
}
}
if (use_lower_bound) {
// We need to "re-canonicalize" in case some literal were fixed while we
// processed one direction.
Coefficient max_value(0);
CanonicalizeLinear(cst, &bound_shift, &max_value);
// We transform the constraint into an upper-bounded one.
for (int i = 0; i < cst->size(); ++i) {
(*cst)[i].literal = (*cst)[i].literal.Negated();
@@ -371,7 +360,7 @@ int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
return /*lbd=*/1;
}
if (literals.size() == 2 && parameters_->treat_binary_clauses_separately()) {
if (literals.size() == 2) {
if (track_binary_clauses_) {
CHECK(binary_clauses_.Add(BinaryClause(literals[0], literals[1])));
}
@@ -380,8 +369,6 @@ int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
}
CHECK(binary_implication_graph_->AddBinaryClauseDuringSearch(literals[0],
literals[1]));
// In case this is the first binary clauses.
InitializePropagators();
return /*lbd=*/2;
}
@@ -454,9 +441,6 @@ void SatSolver::SaveDebugAssignment() {
void SatSolver::AddBinaryClauseInternal(Literal a, Literal b) {
if (!track_binary_clauses_ || binary_clauses_.Add(BinaryClause(a, b))) {
binary_implication_graph_->AddBinaryClause(a, b);
// In case this is the first binary clauses.
InitializePropagators();
}
}
@@ -683,8 +667,6 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
if (!conflict_is_a_clause) {
// Use the PB conflict.
// Note that we don't need to call InitializePropagators() since when we
// are here, we are sure we have at least one pb constraint.
DCHECK_GT(pb_constraints_->NumberOfConstraints(), 0);
CHECK_LT(pb_backjump_level, CurrentDecisionLevel());
Backtrack(pb_backjump_level);
@@ -922,7 +904,7 @@ void SatSolver::Backtrack(int target_level) {
bool SatSolver::AddBinaryClauses(const std::vector<BinaryClause>& clauses) {
SCOPED_TIME_STAT(&stats_);
CHECK_EQ(CurrentDecisionLevel(), 0);
for (BinaryClause c : clauses) {
for (const BinaryClause c : clauses) {
if (trail_->Assignment().LiteralIsFalse(c.a) &&
trail_->Assignment().LiteralIsFalse(c.b)) {
return SetModelUnsat();
@@ -1095,7 +1077,7 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) {
return;
}
if (parameters_->treat_binary_clauses_separately() && candidate.size() == 2) {
if (candidate.size() == 2) {
counters_.minimization_num_removed_literals += clause->size() - 2;
// The order is important for the drat proof.
@@ -1595,7 +1577,7 @@ void SatSolver::ProcessNewlyFixedVariables() {
drat_proof_handler_->DeleteClause({clause->begin(), old_size});
}
if (new_size == 2 && parameters_->treat_binary_clauses_separately()) {
if (new_size == 2) {
// 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.
@@ -1625,6 +1607,14 @@ void SatSolver::ProcessNewlyFixedVariables() {
// part or the full integer part...
bool SatSolver::Propagate() {
SCOPED_TIME_STAT(&stats_);
// If new binary or pb constraint were added for the first time, we need
// to "re-initialize" the list of propagators.
if ((!propagate_binary_ && !binary_implication_graph_->IsEmpty()) ||
(!propagate_pb_ && pb_constraints_->NumberOfConstraints() > 0)) {
InitializePropagators();
}
while (true) {
// The idea here is to abort the inspection as soon as at least one
// propagation occurs so we can loop over and test again the highest
@@ -1649,18 +1639,19 @@ void SatSolver::InitializePropagators() {
// To make Propagate() as fast as possible, we only add the
// binary_implication_graph_/pb_constraints_ propagators if there is anything
// to propagate. Because of this, it is important to call
// InitializePropagators() after the first constraint of this kind is added.
// to propagate.
//
// TODO(user): uses the Model classes here to only call
// model.GetOrCreate<BinaryImplicationGraph>() when the first binary
// constraint is needed, and have a mecanism to always make this propagator
// first. Same for the linear constraints.
if (!binary_implication_graph_->IsEmpty()) {
propagate_binary_ = true;
propagators_.push_back(binary_implication_graph_);
}
propagators_.push_back(clauses_propagator_);
if (pb_constraints_->NumberOfConstraints() > 0) {
propagate_pb_ = true;
propagators_.push_back(pb_constraints_);
}
for (int i = 0; i < external_propagators_.size(); ++i) {
@@ -1762,6 +1753,12 @@ void SatSolver::EnqueueNewDecision(Literal literal) {
void SatSolver::Untrail(int target_trail_index) {
SCOPED_TIME_STAT(&stats_);
DCHECK_LT(target_trail_index, trail_->Index());
if ((!propagate_binary_ && !binary_implication_graph_->IsEmpty()) ||
(!propagate_pb_ && pb_constraints_->NumberOfConstraints() > 0)) {
InitializePropagators();
}
for (SatPropagator* propagator : propagators_) {
propagator->Untrail(*trail_, target_trail_index);
}

18
ortools/sat/sat_solver.h
View File

@@ -97,16 +97,15 @@ class SatSolver {
bool AddUnitClause(Literal true_literal);
// Same as AddProblemClause() below, but for small clauses.
//
// TODO(user): Remove this and AddUnitClause() when initializer lists can be
// used in the open-source code like in AddClause({a, b}).
bool AddBinaryClause(Literal a, Literal b);
bool AddTernaryClause(Literal a, Literal b, Literal c);
// Adds a clause to the problem. Returns false if the problem is detected to
// be UNSAT.
//
// TODO(user): Rename this to AddClause().
// TODO(user): Rename this to AddClause(), also get rid of the specialized
// AddUnitClause(), AddBinaryClause() and AddTernaryClause() since they
// just end up calling this?
bool AddProblemClause(absl::Span<const Literal> literals);
// Adds a pseudo-Boolean constraint to the problem. Returns false if the
@@ -542,6 +541,10 @@ class SatSolver {
bool AddLinearConstraintInternal(const std::vector<LiteralWithCoeff>& cst,
Coefficient rhs, Coefficient max_value);
// Makes sure a pseudo boolean constraint is in canonical form.
void CanonicalizeLinear(std::vector<LiteralWithCoeff>* cst,
Coefficient* bound_shift, Coefficient* max_value);
// Adds a learned clause to the problem. This should be called after
// Backtrack(). The backtrack is such that after it is applied, all the
// literals of the learned close except one will be false. Thus the last one
@@ -692,6 +695,8 @@ class SatSolver {
// Internal propagators. We keep them here because we need more than the
// SatPropagator interface for them.
bool propagate_binary_ = false;
bool propagate_pb_ = false;
BinaryImplicationGraph* binary_implication_graph_;
LiteralWatchers* clauses_propagator_;
PbConstraints* pb_constraints_;
@@ -794,7 +799,7 @@ class SatSolver {
std::vector<BooleanVariable> dfs_stack_;
std::vector<BooleanVariable> variable_to_process_;
// Temporary member used by AddLinearConstraintInternal().
// Temporary member used when adding clauses.
std::vector<Literal> literals_scratchpad_;
// A boolean vector used to temporarily mark decision levels.
@@ -818,9 +823,6 @@ class SatSolver {
// analysis.
VariableWithSameReasonIdentifier same_reason_identifier_;
// Temporary vector used by AddProblemClause().
std::vector<LiteralWithCoeff> tmp_pb_constraint_;
// Boolean used to include/exclude constraints from the core computation.
bool is_relevant_for_core_computation_;

14
ortools/sat/synchronization.cc
View File

@@ -133,10 +133,11 @@ std::string SatProgressMessage(const std::string& event_or_solution_count,
} // namespace
void SharedResponseManager::LogMessage(std::string message) {
void SharedResponseManager::LogMessage(const std::string& prefix,
const std::string& message) {
absl::MutexLock mutex_lock(&mutex_);
SOLVER_LOG(logger_,
absl::StrFormat("#Model %6.2fs %s", wall_timer_.Get(), message));
SOLVER_LOG(logger_, absl::StrFormat("#%-5s %6.2fs %s", prefix,
wall_timer_.Get(), message));
}
void SharedResponseManager::InitializeObjective(const CpModelProto& cp_model) {
@@ -848,6 +849,13 @@ void SharedBoundsManager::LogStatistics(SolverLogger* logger) {
}
}
int SharedBoundsManager::NumBoundsExported(const std::string& worker_name) {
absl::MutexLock mutex_lock(&mutex_);
const auto it = bounds_exported_.find(worker_name);
if (it == bounds_exported_.end()) return 0;
return it->second;
}
int SharedClausesManager::RegisterNewId() {
absl::MutexLock mutex_lock(&mutex_);
const int id = id_to_last_processed_binary_clause_.size();

3
ortools/sat/synchronization.h
View File

@@ -327,7 +327,7 @@ class SharedResponseManager {
// Display improvement stats.
void DisplayImprovementStatistics();
void LogMessage(std::string message);
void LogMessage(const std::string& prefix, const std::string& message);
// This is here for the few codepath that needs to modify the returned
// response directly. Note that this do not work in parallel.
@@ -448,6 +448,7 @@ class SharedBoundsManager {
void Synchronize();
void LogStatistics(SolverLogger* logger);
int NumBoundsExported(const std::string& worker_name);
private:
const int num_variables_;