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

[CP-SAT] more work on binary clauses sharing between workers

Browse Source
This commit is contained in:
Laurent Perron
2022-01-27 16:59:54 +01:00
parent 996115ac7f
commit da246501e7
6 changed files with 76 additions and 21 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
ortools/sat/cp_model.cc
View File

@@ -736,6 +736,20 @@ IntervalVar CpModelBuilder::NewOptionalFixedSizeIntervalVar(
return IntervalVar(index, this);
}
void CpModelBuilder::FixVariable(IntVar var, int64_t value) {
FillDomainInProto(Domain(value), cp_model_.mutable_variables(var.index()));
}
void CpModelBuilder::FixVariable(BoolVar var, bool value) {
const int index = var.index();
if (RefIsPositive(index)) {
FillDomainInProto(Domain(value), cp_model_.mutable_variables(index));
} else {
FillDomainInProto(Domain(!value),
cp_model_.mutable_variables(NegatedRef(index)));
}
}
Constraint CpModelBuilder::AddBoolOr(absl::Span<const BoolVar> literals) {
ConstraintProto* const proto = cp_model_.add_constraints();
for (const BoolVar& lit : literals) {

17
ortools/sat/cp_model.h
View File

@@ -23,9 +23,8 @@
IntVar rabbits = cp_model.NewIntVar(all_animals).WithName("rabbits");
IntVar pheasants = cp_model.NewIntVar(all_animals).WithName("pheasants");
cp_model.AddEquality(LinearExpr::Sum({rabbits, pheasants}), 20);
cp_model.AddEquality(LinearExpr::WeightedSum({rabbits, pheasants}, {4, 2}),
56);
cp_model.AddEquality(rabbits + pheasants, 20);
cp_model.AddEquality(4 * rabbits + 2 * pheasants, 56);
const CpSolverResponse response = Solve(cp_model.Build());
if (response.status() == CpSolverStatus::FEASIBLE) {
@@ -760,6 +759,18 @@ class CpModelBuilder {
IntervalVar NewOptionalFixedSizeIntervalVar(const LinearExpr& start,
int64_t size, BoolVar presence);
/// It is sometime convenient when building a model to create a bunch of
/// variables that will later be fixed. Instead of doing AddEquality(var,
/// value) which add a constraint, these functions modify directly the
/// underlying variable domain.
///
/// Note that this ignore completely the original variable domain and just fix
/// the given variable to the given value, even if it was outside the given
/// variable domain. You can still use AddEquality() if this is not what you
/// want.
void FixVariable(IntVar var, int64_t value);
void FixVariable(BoolVar var, bool value);
/// Adds the constraint that at least one of the literals must be true.
Constraint AddBoolOr(absl::Span<const BoolVar> literals);

17
ortools/sat/cp_model_solver.cc
View File

@@ -506,7 +506,7 @@ void FillSolutionInResponse(const CpModelProto& model_proto, const Model& model,
if (mapping->IsInteger(i)) {
const IntegerVariable var = mapping->Integer(i);
// For ignored or not fully instanciated variable, we just use the
// For ignored or not fully instantiated variable, we just use the
// lower bound.
solution.push_back(model.Get(LowerBound(var)));
} else {
@@ -2084,6 +2084,9 @@ class FullProblemSolver : public SubSolver {
*shared_->model_proto, shared_->bounds, local_model_.get());
}
// 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.
if (shared_->clauses != nullptr) {
const int id = shared_->clauses->RegisterNewId();
shared_->clauses->SetWorkerNameForId(id, local_model_->Name());
@@ -2941,26 +2944,27 @@ void SolveCpModelParallel(const CpModelProto& model_proto,
// Log statistics.
if (logger->LoggingIsEnabled()) {
if (parameters.log_subsolver_statistics()) {
SOLVER_LOG(logger, "");
SOLVER_LOG(logger, "Sub-solver search statistics:");
bool first = true;
for (const auto& subsolver : subsolvers) {
const std::string stats = subsolver->StatisticsString();
if (stats.empty()) continue;
if (first) {
SOLVER_LOG(logger, "");
SOLVER_LOG(logger, "Sub-solver search statistics:");
first = false;
}
SOLVER_LOG(logger,
absl::StrCat(" '", subsolver->name(), "':\n", stats));
}
}
SOLVER_LOG(logger, "");
shared.response->DisplayImprovementStatistics();
if (shared.bounds) {
SOLVER_LOG(logger, "");
shared.bounds->LogStatistics(logger);
}
if (shared.clauses) {
SOLVER_LOG(logger, "");
shared.clauses->LogStatistics(logger);
}
}
@@ -3557,6 +3561,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
SOLVER_LOG(logger, lp->Statistics());
}
}
SOLVER_LOG(logger, "");
}
}

41
ortools/sat/sat_solver.cc
View File

@@ -138,6 +138,9 @@ 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) {
// TODO(user): We generate in some corner cases clauses with
// literals[0].Variable() == literals[1].Variable(). Avoid doing that and
// adding such binary clauses to the graph?
if (!binary_implication_graph_->AddBinaryClauseDuringSearch(literals[0],
literals[1])) {
CHECK_EQ(CurrentDecisionLevel(), 0);
@@ -213,7 +216,17 @@ bool SatSolver::AddProblemClauseInternal(absl::Span<const Literal> literals) {
}
trail_->EnqueueWithUnitReason(literals[0]);
} else if (literals.size() == 2) {
AddBinaryClauseInternal(literals[0], literals[1]);
// TODO(user): Make sure the presolve do not generate such clauses.
if (literals[0] == literals[1]) {
// Literal must be true.
trail_->EnqueueWithUnitReason(literals[0]);
} else if (literals[0] == literals[1].Negated()) {
// Always true.
return true;
} else {
AddBinaryClauseInternal(literals[0], literals[1],
/*export_clause=*/false);
}
} else {
if (!clauses_propagator_->AddClause(literals, trail_)) {
return SetModelUnsat();
@@ -362,6 +375,7 @@ int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
if (literals.size() == 2) {
if (track_binary_clauses_) {
// This clause MUST be knew, otherwise something is wrong.
CHECK(binary_clauses_.Add(BinaryClause(literals[0], literals[1])));
}
if (shared_binary_clauses_callback_ != nullptr) {
@@ -438,10 +452,18 @@ 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);
void SatSolver::AddBinaryClauseInternal(Literal a, Literal b,
bool export_clause) {
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);
}
binary_implication_graph_->AddBinaryClause(a, b);
}
bool SatSolver::ClauseIsValidUnderDebugAssignment(
@@ -905,11 +927,7 @@ bool SatSolver::AddBinaryClauses(const std::vector<BinaryClause>& clauses) {
SCOPED_TIME_STAT(&stats_);
CHECK_EQ(CurrentDecisionLevel(), 0);
for (const BinaryClause c : clauses) {
if (trail_->Assignment().LiteralIsFalse(c.a) &&
trail_->Assignment().LiteralIsFalse(c.b)) {
return SetModelUnsat();
}
AddBinaryClauseInternal(c.a, c.b);
if (!AddBinaryClause(c.a, c.b)) return false;
}
if (!Propagate()) return SetModelUnsat();
return true;
@@ -1081,7 +1099,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]);
AddBinaryClauseInternal(candidate[0], candidate[1], /*export_clause=*/true);
clauses_propagator_->Detach(clause);
// This is needed in the corner case where this was the first binary clause
@@ -1581,7 +1599,8 @@ 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());
AddBinaryClauseInternal(clause->FirstLiteral(), clause->SecondLiteral(),
/*export_clause=*/true);
clauses_propagator_->LazyDetach(clause);
++num_binary;
continue;

5
ortools/sat/sat_solver.h
View File

@@ -452,7 +452,10 @@ class SatSolver {
// Adds a binary clause to the BinaryImplicationGraph and to the
// BinaryClauseManager when track_binary_clauses_ is true.
void AddBinaryClauseInternal(Literal a, Literal b);
//
// 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);
// See SaveDebugAssignment(). Note that these functions only consider the
// variables at the time the debug_assignment_ was saved. If new variables

3
ortools/sat/synchronization.cc
View File

@@ -688,6 +688,7 @@ void SharedResponseManager::RegisterObjectiveBoundImprovement(
void SharedResponseManager::DisplayImprovementStatistics() {
absl::MutexLock mutex_lock(&mutex_);
if (!primal_improvements_count_.empty()) {
SOLVER_LOG(logger_, "");
SOLVER_LOG(logger_, "Solutions found per subsolver:");
for (const auto& entry : primal_improvements_count_) {
SOLVER_LOG(logger_, " '", entry.first, "': ", entry.second);
@@ -842,6 +843,7 @@ void SharedBoundsManager::GetChangedBounds(
void SharedBoundsManager::LogStatistics(SolverLogger* logger) {
absl::MutexLock mutex_lock(&mutex_);
if (!bounds_exported_.empty()) {
SOLVER_LOG(logger, "");
SOLVER_LOG(logger, "Improving variable bounds shared per subsolver:");
for (const auto& entry : bounds_exported_) {
SOLVER_LOG(logger, " '", entry.first, "': ", entry.second);
@@ -906,6 +908,7 @@ void SharedClausesManager::LogStatistics(SolverLogger* logger) {
name_to_clauses[id_to_worker_name_[id]] = id_to_clauses_exported_[id];
}
if (!name_to_clauses.empty()) {
SOLVER_LOG(logger, "");
SOLVER_LOG(logger, "Clauses shared per subsolver:");
for (const auto& entry : name_to_clauses) {
SOLVER_LOG(logger, " '", entry.first, "': ", entry.second);