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

[CP-SAT] limit effort in feasibility_jump; new experimental scheduling search on cumulative

Browse Source
This commit is contained in:
Laurent Perron
2023-10-29 15:31:06 +01:00
parent 79bd14424f
commit 185b77cea0
12 changed files with 129 additions and 63 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
ortools/sat/feasibility_jump.cc
View File

@@ -508,7 +508,8 @@ std::function<void()> FeasibilityJumpSolver::GenerateTask(int64_t /*task_id*/) {
double FeasibilityJumpSolver::ComputeScore(absl::Span<const double> weights,
int var, int64_t delta,
bool linear_only) const {
bool linear_only) {
++num_scores_computed_;
constexpr double kEpsilon = 1.0 / std::numeric_limits<int64_t>::max();
double score =
evaluator_->LinearEvaluator().WeightedViolationDelta(weights, var, delta);
@@ -818,10 +819,9 @@ bool FeasibilityJumpSolver::DoSomeGeneralIterations() {
RecomputeVarsToScan(general_jumps_);
InitializeCompoundWeights();
auto effort = [&]() {
return num_general_evals_ + num_linear_evals_ + num_weight_updates_ +
num_general_moves_;
return num_scores_computed_ + num_weight_updates_ + num_general_moves_;
};
const int64_t effort_limit = effort() + 20000;
const int64_t effort_limit = effort() + 100000;
while (effort() < effort_limit) {
int var;
int64_t value;

3
ortools/sat/feasibility_jump.h
View File

@@ -165,7 +165,7 @@ class FeasibilityJumpSolver : public SubSolver {
// Returns the weighted violation delta plus epsilon * the objective delta.
double ComputeScore(absl::Span<const double> weights, int var, int64_t delta,
bool linear_only) const;
bool linear_only);
// Computes the optimal value for variable v, considering only the violation
// of linear constraints.
@@ -303,6 +303,7 @@ class FeasibilityJumpSolver : public SubSolver {
int64_t num_restarts_ = 0;
int64_t num_solutions_imported_ = 0;
int64_t num_weight_updates_ = 0;
int64_t num_scores_computed_ = 0;
std::unique_ptr<CompoundMoveBuilder> move_;

58
ortools/sat/integer_search.cc
View File

@@ -679,7 +679,8 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
auto* repo = model->GetOrCreate<IntervalsRepository>();
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
auto* trail = model->GetOrCreate<Trail>();
return [repo, integer_trail, trail]() {
auto* search_helper = model->GetOrCreate<IntegerSearchHelper>();
return [repo, integer_trail, trail, search_helper]() {
SchedulingConstraintHelper* best_helper = nullptr;
int best_before = 0;
int best_after = 0;
@@ -715,6 +716,7 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
// Set their demand to zero.
while (next_end < num_tasks && by_emin[next_end].time == time) {
const int t = by_emin[next_end].task_index;
if (!helper->IsPresent(t)) continue;
if (added_demand[t] > 0) {
current_height -= added_demand[t];
added_demand[t] = 0;
@@ -730,6 +732,7 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
// TODO(user): tie-break tasks not fitting in the profile smartly.
while (next_start < num_tasks && by_smin[next_start].time == time) {
const int t = by_smin[next_start].task_index;
if (!helper->IsPresent(t)) continue;
if (added_demand[t] == -1) continue; // Corner case.
const IntegerValue demand_min = h.demand_helper->DemandMin(t);
if (current_height + demand_min <= capacity_max) {
@@ -763,6 +766,9 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
}
open_tasks.push_back(first_skipped_task);
// TODO(user): If the two box cannot overlap because of high demand, use
// repo.CreateDisjunctivePrecedenceLiteral() instead.
//
// TODO(user): Add heuristic ordering for creating interesting precedence
// first.
bool found_precedence_to_add = false;
@@ -817,10 +823,29 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
//
// TODO(user): We need to add the reason for demand_min and capacity_max.
// TODO(user): unfortunately we can't report it from here.
std::vector<IntegerLiteral> integer_reason;
if (!h.capacity.IsConstant()) {
integer_reason.push_back(
integer_trail->UpperBoundAsLiteral(h.capacity));
}
const auto& demands = h.demand_helper->Demands();
for (const int t : open_tasks) {
if (helper->IsOptional(t)) {
CHECK(trail->Assignment().LiteralIsTrue(helper->PresenceLiteral(t)));
conflict.push_back(helper->PresenceLiteral(t).Negated());
}
const AffineExpression d = demands[t];
if (!d.IsConstant()) {
integer_reason.push_back(integer_trail->LowerBoundAsLiteral(d));
}
}
integer_trail->ReportConflict(conflict, integer_reason);
search_helper->NotifyThatConflictWasFoundDuringGetDecision();
if (VLOG_IS_ON(2)) {
LOG(INFO) << "Conflict between precedences !";
for (const int t : open_tasks) LOG(INFO) << helper->TaskDebugString(t);
}
return BooleanOrIntegerLiteral();
}
// TODO(user): add heuristic criteria, right now we stop at first
@@ -1252,9 +1277,9 @@ bool IntegerSearchHelper::BeforeTakingDecision() {
return true;
}
LiteralIndex IntegerSearchHelper::GetDecision(
const std::function<BooleanOrIntegerLiteral()>& f) {
LiteralIndex decision = kNoLiteralIndex;
bool IntegerSearchHelper::GetDecision(
const std::function<BooleanOrIntegerLiteral()>& f, LiteralIndex* decision) {
*decision = kNoLiteralIndex;
while (!time_limit_->LimitReached()) {
BooleanOrIntegerLiteral new_decision;
if (integer_trail_->InPropagationLoop()) {
@@ -1267,6 +1292,12 @@ LiteralIndex IntegerSearchHelper::GetDecision(
}
if (!new_decision.HasValue()) {
new_decision = f();
if (must_process_conflict_) {
must_process_conflict_ = false;
sat_solver_->ProcessCurrentConflict();
(void)sat_solver_->FinishPropagation();
return false;
}
}
if (!new_decision.HasValue() &&
integer_trail_->CurrentBranchHadAnIncompletePropagation()) {
@@ -1283,13 +1314,13 @@ LiteralIndex IntegerSearchHelper::GetDecision(
// until we have a conflict with these decisions, but it is currently
// hard to do so.
if (new_decision.boolean_literal_index != kNoLiteralIndex) {
decision = new_decision.boolean_literal_index;
*decision = new_decision.boolean_literal_index;
} else {
decision =
*decision =
encoder_->GetOrCreateAssociatedLiteral(new_decision.integer_literal)
.Index();
}
if (sat_solver_->Assignment().LiteralIsAssigned(Literal(decision))) {
if (sat_solver_->Assignment().LiteralIsAssigned(Literal(*decision))) {
// TODO(user): It would be nicer if this can never happen. For now, it
// does because of the Propagate() not reaching the fixed point as
// mentioned in a TODO above. As a work-around, we display a message
@@ -1300,7 +1331,7 @@ LiteralIndex IntegerSearchHelper::GetDecision(
}
break;
}
return decision;
return true;
}
bool IntegerSearchHelper::TakeDecision(Literal decision) {
@@ -1382,17 +1413,22 @@ SatSolver::Status IntegerSearchHelper::SolveIntegerProblem() {
LiteralIndex decision = kNoLiteralIndex;
while (true) {
if (sat_solver_->ModelIsUnsat()) return sat_solver_->UnsatStatus();
if (heuristics.next_decision_override != nullptr) {
// Note that to properly count the num_times, we do not want to move
// this function, but actually call that copy.
decision = GetDecision(heuristics.next_decision_override);
if (!GetDecision(heuristics.next_decision_override, &decision)) {
continue;
}
if (decision == kNoLiteralIndex) {
heuristics.next_decision_override = nullptr;
}
}
if (decision == kNoLiteralIndex) {
decision =
GetDecision(heuristics.decision_policies[heuristics.policy_index]);
if (!GetDecision(heuristics.decision_policies[heuristics.policy_index],
&decision)) {
continue;
}
}
// Probing?

13
ortools/sat/integer_search.h
View File

@@ -271,7 +271,16 @@ class IntegerSearchHelper {
// Calls the decision heuristics and extract a non-fixed literal.
// Note that we do not want to copy the function here.
LiteralIndex GetDecision(const std::function<BooleanOrIntegerLiteral()>& f);
//
// Returns false if a conflict was found while trying to take a decision.
bool GetDecision(const std::function<BooleanOrIntegerLiteral()>& f,
LiteralIndex* decision);
// Functions passed to GetDecision() might call this to notify a conflict
// was detected.
void NotifyThatConflictWasFoundDuringGetDecision() {
must_process_conflict_ = true;
}
// Tries to take the current decision, this might backjump.
// Returns false if the model is UNSAT.
@@ -301,6 +310,8 @@ class IntegerSearchHelper {
TimeLimit* time_limit_;
PseudoCosts* pseudo_costs_;
IntegerVariable objective_var_ = kNoIntegerVariable;
bool must_process_conflict_ = false;
};
// This class will loop continuously on model variables and try to probe/shave

19
ortools/sat/intervals.cc
View File

@@ -127,8 +127,9 @@ void IntervalsRepository::CreateDisjunctivePrecedenceLiteral(
disjunctive_precedences_.insert({{b, a}, a_before_b.Negated()});
// Also insert it in precedences.
precedences_.insert({{a, b}, a_before_b});
precedences_.insert({{b, a}, a_before_b.Negated()});
// TODO(user): also add the reverse like start_b + 1 <= end_a if negated?
precedences_.insert({{end_a, start_b}, a_before_b});
precedences_.insert({{end_b, start_a}, a_before_b.Negated()});
enforcement_literals.push_back(a_before_b);
AddConditionalAffinePrecedence(enforcement_literals, end_a, start_b, model_);
@@ -147,12 +148,12 @@ void IntervalsRepository::CreateDisjunctivePrecedenceLiteral(
bool IntervalsRepository::CreatePrecedenceLiteral(IntervalVariable a,
IntervalVariable b) {
if (precedences_.find({a, b}) != disjunctive_precedences_.end()) return false;
const AffineExpression x = End(a);
const AffineExpression y = Start(b);
if (precedences_.find({x, y}) != precedences_.end()) return false;
// We want l => x <= y and not(l) => x > y <=> y + 1 <= x
// Do not create l if the relation is always true or false.
const AffineExpression x = End(a);
const AffineExpression y = Start(b);
if (integer_trail_->UpperBound(x) <= integer_trail_->LowerBound(y)) {
return false;
}
@@ -163,7 +164,9 @@ bool IntervalsRepository::CreatePrecedenceLiteral(IntervalVariable a,
// Create a new literal.
const BooleanVariable boolean_var = sat_solver_->NewBooleanVariable();
const Literal x_before_y = Literal(boolean_var, true);
precedences_.insert({{a, b}, x_before_y});
// TODO(user): Also add {{y_plus_one, x}, x_before_y.Negated()} ?
precedences_.insert({{x, y}, x_before_y});
AffineExpression y_plus_one = y;
y_plus_one.constant += 1;
@@ -174,7 +177,9 @@ bool IntervalsRepository::CreatePrecedenceLiteral(IntervalVariable a,
LiteralIndex IntervalsRepository::GetPrecedenceLiteral(
IntervalVariable a, IntervalVariable b) const {
const auto it = precedences_.find({a, b});
const AffineExpression x = End(a);
const AffineExpression y = Start(b);
const auto it = precedences_.find({x, y});
if (it != precedences_.end()) return it->second.Index();
return kNoLiteralIndex;
}

6
ortools/sat/intervals.h
View File

@@ -241,9 +241,13 @@ class IntervalsRepository {
demand_helper_repository_;
// Disjunctive and normal precedences.
//
// Note that for normal precedences, we use directly the affine expression so
// that if many intervals share the same start, we don't re-create Booleans
// for no reason.
absl::flat_hash_map<std::pair<IntervalVariable, IntervalVariable>, Literal>
disjunctive_precedences_;
absl::flat_hash_map<std::pair<IntervalVariable, IntervalVariable>, Literal>
absl::flat_hash_map<std::pair<AffineExpression, AffineExpression>, Literal>
precedences_;
// Disjunctive/Cumulative helpers_.

7
ortools/sat/lb_tree_search.cc
View File

@@ -538,8 +538,11 @@ SatSolver::Status LbTreeSearch::Search(
while (true) {
// TODO(user): We sometimes branch on the objective variable, this should
// probably be avoided.
const LiteralIndex decision =
search_helper_->GetDecision(search_heuristic_);
if (sat_solver_->ModelIsUnsat()) return sat_solver_->UnsatStatus();
LiteralIndex decision;
if (!search_helper_->GetDecision(search_heuristic_, &decision)) {
continue;
}
// No new decision: search done.
if (time_limit_->LimitReached()) return SatSolver::LIMIT_REACHED;

3
ortools/sat/sat_parameters.proto
View File

@@ -745,9 +745,8 @@ message SatParameters {
// Whether we try to branch on decision "interval A before interval B" rather
// than on intervals bounds. This usually works better, but slow down a bit
// the time to find first solutions.
// the time to find the first solution.
//
// Note that for cumulative, this currently seems worse.
// These parameters are still EXPERIMENTAL, the result should be correct, but
// it some corner cases, they can cause some failing CHECK in the solver.
optional bool use_dynamic_precedence_in_disjunctive = 263 [default = false];

20
ortools/sat/sat_solver.cc
View File

@@ -584,7 +584,8 @@ bool SatSolver::FinishPropagation() {
int num_loop = 0;
while (true) {
const int old_decision_level = current_decision_level_;
if (!PropagateAndStopAfterOneConflictResolution()) {
if (!Propagate()) {
ProcessCurrentConflict();
if (model_is_unsat_) return false;
if (current_decision_level_ == old_decision_level) {
CHECK(!assumptions_.empty());
@@ -682,10 +683,9 @@ bool SatSolver::ReapplyAssumptionsIfNeeded() {
return (status == SatSolver::FEASIBLE);
}
bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
void SatSolver::ProcessCurrentConflict() {
SCOPED_TIME_STAT(&stats_);
if (Propagate()) return true;
if (model_is_unsat_) return false;
if (model_is_unsat_) return;
++counters_.num_failures;
const int conflict_trail_index = trail_->Index();
@@ -703,7 +703,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
// it reduces to only one literal in which case we can just fix it.
const int highest_level =
DecisionLevel((*trail_)[max_trail_index].Variable());
if (highest_level == 1) return false;
if (highest_level == 1) return;
}
ComputeFirstUIPConflict(max_trail_index, &learned_conflict_,
@@ -711,7 +711,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
&subsumed_clauses_);
// An empty conflict means that the problem is UNSAT.
if (learned_conflict_.empty()) return SetModelUnsat();
if (learned_conflict_.empty()) return (void)SetModelUnsat();
DCHECK(IsConflictValid(learned_conflict_));
DCHECK(ClauseIsValidUnderDebugAssignment(learned_conflict_));
@@ -789,7 +789,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
int pb_backjump_level;
ComputePBConflict(max_trail_index, initial_slack, &pb_conflict_,
&pb_backjump_level);
if (pb_backjump_level == -1) return SetModelUnsat();
if (pb_backjump_level == -1) return (void)SetModelUnsat();
// Convert the conflict into the vector<LiteralWithCoeff> form.
std::vector<LiteralWithCoeff> cst;
@@ -817,7 +817,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
trail_));
CHECK_GT(trail_->Index(), last_decision_or_backtrack_trail_index_);
counters_.num_learned_pb_literals += cst.size();
return false;
return;
}
// Continue with the normal clause flow, but use the PB conflict clause
@@ -941,7 +941,6 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
learned_conflict_, is_redundant);
restart_->OnConflict(conflict_trail_index, conflict_decision_level,
conflict_lbd);
return false;
}
SatSolver::Status SatSolver::ReapplyDecisionsUpTo(
@@ -1339,8 +1338,9 @@ SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit,
}
const int old_level = current_decision_level_;
if (!PropagateAndStopAfterOneConflictResolution()) {
if (!Propagate()) {
// A conflict occurred, continue the loop.
ProcessCurrentConflict();
if (model_is_unsat_) return StatusWithLog(INFEASIBLE);
if (old_level == current_decision_level_) {
CHECK(!assumptions_.empty());

14
ortools/sat/sat_solver.h
View File

@@ -476,15 +476,15 @@ class SatSolver {
// Hack to allow to temporarily disable logging if it is enabled.
SolverLogger* mutable_logger() { return logger_; }
private:
// Calls Propagate() and returns true if no conflict occurred. Otherwise,
// learns the conflict, backtracks, enqueues the consequence of the learned
// conflict and returns false.
// Processes the current conflict from trail->FailingClause().
//
// When handling assumptions, this might return false without backtracking
// in case of ASSUMPTIONS_UNSAT.
bool PropagateAndStopAfterOneConflictResolution();
// This learns the conflict, backtracks, enqueues the consequence of the
// learned conflict and return. When handling assumptions, this might return
// false without backtracking in case of ASSUMPTIONS_UNSAT. This is only
// exposed to allow processing a conflict detected outside normal propagation.
void ProcessCurrentConflict();
private:
// All Solve() functions end up calling this one.
Status SolveInternal(TimeLimit* time_limit, int64_t max_number_of_conflicts);

39
ortools/sat/work_assignment.cc
View File

@@ -596,7 +596,7 @@ bool SharedTreeWorker::SyncWithLocalTrail() {
return true;
}
LiteralIndex SharedTreeWorker::NextDecision() {
bool SharedTreeWorker::NextDecision(LiteralIndex* decision_index) {
const auto& decision_policy =
heuristics_->decision_policies[heuristics_->policy_index];
const int next_level = sat_solver_->CurrentDecisionLevel() + 1;
@@ -608,11 +608,12 @@ LiteralIndex SharedTreeWorker::NextDecision() {
CHECK(!sat_solver_->Assignment().LiteralIsFalse(decision))
<< " at depth " << next_level << " " << parameters_->name();
CHECK(!sat_solver_->Assignment().LiteralIsTrue(decision));
return decision.Index();
*decision_index = decision.Index();
return true;
}
if (objective_ == nullptr ||
objective_->objective_var == kNoIntegerVariable) {
return helper_->GetDecision(decision_policy);
return helper_->GetDecision(decision_policy, decision_index);
}
// If the current node is close to the global lower bound, maybe try to
// improve it.
@@ -625,17 +626,21 @@ LiteralIndex SharedTreeWorker::NextDecision() {
*random_, 0, (root_obj_ub - root_obj_lb).value());
const double objective_split_probability =
parameters_->shared_tree_worker_objective_split_probability();
return helper_->GetDecision([&]() -> BooleanOrIntegerLiteral {
IntegerValue obj_lb = integer_trail_->LowerBound(objective_->objective_var);
IntegerValue obj_ub = integer_trail_->UpperBound(objective_->objective_var);
if (obj_lb > obj_split || obj_ub <= obj_split ||
next_level > assigned_tree_.MaxLevel() + 1 ||
absl::Bernoulli(*random_, 1 - objective_split_probability)) {
return decision_policy();
}
return BooleanOrIntegerLiteral(
IntegerLiteral::LowerOrEqual(objective_->objective_var, obj_split));
});
return helper_->GetDecision(
[&]() -> BooleanOrIntegerLiteral {
IntegerValue obj_lb =
integer_trail_->LowerBound(objective_->objective_var);
IntegerValue obj_ub =
integer_trail_->UpperBound(objective_->objective_var);
if (obj_lb > obj_split || obj_ub <= obj_split ||
next_level > assigned_tree_.MaxLevel() + 1 ||
absl::Bernoulli(*random_, 1 - objective_split_probability)) {
return decision_policy();
}
return BooleanOrIntegerLiteral(
IntegerLiteral::LowerOrEqual(objective_->objective_var, obj_split));
},
decision_index);
}
void SharedTreeWorker::MaybeProposeSplit() {
@@ -709,9 +714,10 @@ SatSolver::Status SharedTreeWorker::Search(
SyncWithSharedTree();
}
if (!SyncWithLocalTrail()) return sat_solver_->UnsatStatus();
Literal decision(NextDecision());
LiteralIndex decision_index;
if (!NextDecision(&decision_index)) continue;
if (time_limit_->LimitReached()) return SatSolver::LIMIT_REACHED;
if (decision.Index() == kNoLiteralIndex) {
if (decision_index == kNoLiteralIndex) {
feasible_solution_observer();
if (!has_objective) return SatSolver::FEASIBLE;
const IntegerValue objective =
@@ -726,6 +732,7 @@ SatSolver::Status SharedTreeWorker::Search(
continue;
}
const Literal decision(decision_index);
CHECK(!sat_solver_->Assignment().LiteralIsFalse(decision));
CHECK(!sat_solver_->Assignment().LiteralIsTrue(decision));
if (!helper_->TakeDecision(decision)) {

2
ortools/sat/work_assignment.h
View File

@@ -240,7 +240,7 @@ class SharedTreeWorker {
void SyncWithSharedTree();
Literal DecodeDecision(ProtoLiteral literal);
std::optional<ProtoLiteral> EncodeDecision(Literal decision);
LiteralIndex NextDecision();
bool NextDecision(LiteralIndex* decision_index);
void MaybeProposeSplit();
// Add any implications to the clause database for the current level.