31void AppendLowerBoundReasonIfValid(IntegerVariable
var,
32 const IntegerTrail& i_trail,
33 std::vector<IntegerLiteral>* reason) {
35 reason->push_back(i_trail.LowerBoundAsLiteral(
var));
44 while (propagation_trail_index_ < trail_->
Index()) {
46 if (
literal.Index() >= literal_to_new_impacted_arcs_.
size())
continue;
51 literal_to_new_impacted_arcs_[
literal.Index()]) {
52 if (--arc_counts_[arc_index] == 0) {
53 const ArcInfo& arc = arcs_[arc_index];
54 impacted_arcs_[arc.tail_var].
push_back(arc_index);
61 literal_to_new_impacted_arcs_[
literal.Index()]) {
62 if (arc_counts_[arc_index] > 0)
continue;
63 const ArcInfo& arc = arcs_[arc_index];
65 const IntegerValue new_head_lb =
66 integer_trail_->
LowerBound(arc.tail_var) + ArcOffset(arc);
67 if (new_head_lb > integer_trail_->
LowerBound(arc.head_var)) {
68 if (!EnqueueAndCheck(arc, new_head_lb, trail_))
return false;
74 InitializeBFQueueWithModifiedNodes();
75 if (!BellmanFordTarjan(trail_))
return false;
85 DCHECK(NoPropagationLeft(*trail_));
89 PropagateOptionalArcs(trail_);
98 if (
var >= impacted_arcs_.
size())
return true;
99 for (
const ArcIndex arc_index : impacted_arcs_[
var]) {
100 const ArcInfo& arc = arcs_[arc_index];
102 const IntegerValue new_head_lb =
103 integer_trail_->
LowerBound(arc.tail_var) + ArcOffset(arc);
104 if (new_head_lb > integer_trail_->
LowerBound(arc.head_var)) {
105 if (!EnqueueAndCheck(arc, new_head_lb, trail_))
return false;
120 if (
literal.Index() >= literal_to_new_impacted_arcs_.
size())
continue;
122 literal_to_new_impacted_arcs_[
literal.Index()]) {
123 if (arc_counts_[arc_index]++ == 0) {
124 const ArcInfo& arc = arcs_[arc_index];
125 impacted_arcs_[arc.tail_var].
pop_back();
136 const std::vector<IntegerVariable>& vars,
137 std::vector<IntegerPrecedences>* output) {
138 tmp_sorted_vars_.clear();
139 tmp_precedences_.clear();
141 const IntegerVariable
var = vars[
index];
143 if (
var >= impacted_arcs_.
size())
continue;
144 for (
const ArcIndex arc_index : impacted_arcs_[
var]) {
145 const ArcInfo& arc = arcs_[arc_index];
148 IntegerValue offset = arc.offset;
150 offset += integer_trail_->
LowerBound(arc.offset_var);
157 if (offset < 0)
continue;
159 if (var_to_degree_[arc.head_var] == 0) {
160 tmp_sorted_vars_.push_back(
161 {arc.head_var, integer_trail_->
LowerBound(arc.head_var)});
167 if (var_to_last_index_[arc.head_var] ==
index)
continue;
169 var_to_last_index_[arc.head_var] =
index;
170 var_to_degree_[arc.head_var]++;
171 tmp_precedences_.push_back(
172 {
index, arc.head_var, arc_index.value(), offset});
183 std::sort(tmp_sorted_vars_.begin(), tmp_sorted_vars_.end());
189 for (
const SortedVar pair : tmp_sorted_vars_) {
190 const int degree = var_to_degree_[pair.var];
192 var_to_degree_[pair.var] = start;
196 var_to_degree_[pair.var] = -1;
201 if (var_to_degree_[precedence.var] < 0)
continue;
202 (*output)[var_to_degree_[precedence.var]++] = precedence;
207 for (
const SortedVar pair : tmp_sorted_vars_) {
208 var_to_degree_[pair.var] = 0;
213 int arc_index, IntegerValue min_offset,
214 std::vector<Literal>* literal_reason,
215 std::vector<IntegerLiteral>* integer_reason)
const {
216 const ArcInfo& arc = arcs_[
ArcIndex(arc_index)];
217 for (
const Literal l : arc.presence_literals) {
223 arc.offset_var, min_offset - arc.offset));
227void PrecedencesPropagator::AdjustSizeFor(IntegerVariable i) {
242void PrecedencesPropagator::AddArc(
243 IntegerVariable
tail, IntegerVariable
head, IntegerValue offset,
244 IntegerVariable offset_var, absl::Span<const Literal> presence_literals) {
251 absl::InlinedVector<Literal, 6> enforcement_literals;
253 for (
const Literal l : presence_literals) {
254 enforcement_literals.push_back(l);
257 enforcement_literals.push_back(
261 enforcement_literals.push_back(
266 enforcement_literals.push_back(
271 for (
const Literal l : enforcement_literals) {
277 enforcement_literals[new_size++] = l;
279 enforcement_literals.resize(new_size);
286 VLOG(1) <<
"Self arc! This could be presolved. "
287 <<
"var:" <<
tail <<
" offset:" << offset
288 <<
" offset_var:" << offset_var
289 <<
" conditioned_by:" << presence_literals;
295 const IntegerValue lb = integer_trail_->
LowerBound(offset_var);
296 if (lb == integer_trail_->
UpperBound(offset_var)) {
303 if (!enforcement_literals.empty()) {
304 const OptionalArcIndex arc_index(potential_arcs_.
size());
306 {
tail,
head, offset, offset_var, enforcement_literals});
310 impacted_potential_arcs_[offset_var].
push_back(arc_index);
316 IntegerVariable tail_var;
317 IntegerVariable head_var;
318 IntegerVariable offset_var;
320 std::vector<InternalArc> to_add;
328 to_add.push_back({
tail,
head, offset_var});
329 to_add.push_back({offset_var,
head,
tail});
337 for (
const InternalArc
a : to_add) {
352 modified_vars_.
Set(
a.tail_var);
358 {
a.tail_var,
a.head_var, offset,
a.offset_var, enforcement_literals});
359 auto& presence_literals = arcs_.
back().presence_literals;
363 const Literal to_remove =
365 const auto it = std::find(presence_literals.begin(),
366 presence_literals.end(), to_remove);
367 if (it != presence_literals.end()) presence_literals.erase(it);
370 if (presence_literals.empty()) {
371 impacted_arcs_[
a.tail_var].
push_back(arc_index);
373 for (
const Literal l : presence_literals) {
374 if (l.Index() >= literal_to_new_impacted_arcs_.
size()) {
375 literal_to_new_impacted_arcs_.
resize(l.Index().value() + 1);
377 literal_to_new_impacted_arcs_[l.Index()].
push_back(arc_index);
380 arc_counts_.
push_back(presence_literals.size());
389void PrecedencesPropagator::PropagateOptionalArcs(Trail* trail) {
392 if (
var >= impacted_potential_arcs_.
size())
continue;
396 for (
const OptionalArcIndex arc_index : impacted_potential_arcs_[
var]) {
397 const ArcInfo& arc = potential_arcs_[arc_index];
398 int num_not_true = 0;
399 Literal to_propagate;
400 for (
const Literal l : arc.presence_literals) {
401 if (!trail->Assignment().LiteralIsTrue(l)) {
406 if (num_not_true != 1)
continue;
407 if (trail->Assignment().LiteralIsFalse(to_propagate))
continue;
411 const IntegerValue tail_lb = integer_trail_->
LowerBound(arc.tail_var);
412 const IntegerValue head_ub = integer_trail_->
UpperBound(arc.head_var);
413 if (tail_lb + ArcOffset(arc) > head_ub) {
414 integer_reason_.clear();
415 integer_reason_.push_back(
417 integer_reason_.push_back(
419 AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
421 literal_reason_.clear();
422 for (
const Literal l : arc.presence_literals) {
423 if (l != to_propagate) literal_reason_.push_back(l.Negated());
425 integer_trail_->
EnqueueLiteral(to_propagate.Negated(), literal_reason_,
432IntegerValue PrecedencesPropagator::ArcOffset(
const ArcInfo& arc)
const {
435 : integer_trail_->
LowerBound(arc.offset_var));
438bool PrecedencesPropagator::EnqueueAndCheck(
const ArcInfo& arc,
439 IntegerValue new_head_lb,
448 literal_reason_.clear();
449 for (
const Literal l : arc.presence_literals) {
450 literal_reason_.push_back(l.Negated());
453 integer_reason_.clear();
455 AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
466 if (new_head_lb > integer_trail_->
UpperBound(arc.head_var)) {
467 const IntegerValue slack =
468 new_head_lb - integer_trail_->
UpperBound(arc.head_var) - 1;
469 integer_reason_.push_back(
471 std::vector<IntegerValue> coeffs(integer_reason_.size(), IntegerValue(1));
474 if (!integer_trail_->
IsOptional(arc.head_var)) {
475 return integer_trail_->
ReportConflict(literal_reason_, integer_reason_);
479 if (trail->Assignment().LiteralIsFalse(l)) {
480 literal_reason_.push_back(l);
481 return integer_trail_->
ReportConflict(literal_reason_, integer_reason_);
483 integer_trail_->
EnqueueLiteral(l, literal_reason_, integer_reason_);
489 return integer_trail_->
Enqueue(
491 literal_reason_, integer_reason_);
494bool PrecedencesPropagator::NoPropagationLeft(
const Trail& trail)
const {
495 const int num_nodes = impacted_arcs_.
size();
496 for (IntegerVariable
var(0);
var < num_nodes; ++
var) {
497 for (
const ArcIndex arc_index : impacted_arcs_[
var]) {
498 const ArcInfo& arc = arcs_[arc_index];
500 if (integer_trail_->
LowerBound(arc.tail_var) + ArcOffset(arc) >
509void PrecedencesPropagator::InitializeBFQueueWithModifiedNodes() {
512 const int num_nodes = impacted_arcs_.
size();
513 bf_in_queue_.resize(num_nodes,
false);
514 for (
const int node : bf_queue_) bf_in_queue_[node] =
false;
516 DCHECK(std::none_of(bf_in_queue_.begin(), bf_in_queue_.end(),
517 [](
bool v) { return v; }));
519 if (
var >= num_nodes)
continue;
520 bf_queue_.push_back(
var.value());
521 bf_in_queue_[
var.value()] =
true;
525void PrecedencesPropagator::CleanUpMarkedArcsAndParents() {
528 const int num_nodes = impacted_arcs_.
size();
530 if (
var >= num_nodes)
continue;
531 const ArcIndex parent_arc_index = bf_parent_arc_of_[
var.value()];
532 if (parent_arc_index != -1) {
533 arcs_[parent_arc_index].is_marked =
false;
534 bf_parent_arc_of_[
var.value()] = -1;
535 bf_can_be_skipped_[
var.value()] =
false;
538 DCHECK(std::none_of(bf_parent_arc_of_.begin(), bf_parent_arc_of_.end(),
539 [](
ArcIndex v) { return v != -1; }));
540 DCHECK(std::none_of(bf_can_be_skipped_.begin(), bf_can_be_skipped_.end(),
541 [](
bool v) { return v; }));
544bool PrecedencesPropagator::DisassembleSubtree(
545 int source,
int target, std::vector<bool>* can_be_skipped) {
549 tmp_vector_.push_back(source);
550 while (!tmp_vector_.empty()) {
551 const int tail = tmp_vector_.back();
552 tmp_vector_.pop_back();
553 for (
const ArcIndex arc_index : impacted_arcs_[IntegerVariable(
tail)]) {
554 const ArcInfo& arc = arcs_[arc_index];
556 arc.is_marked =
false;
557 if (arc.head_var.value() == target)
return true;
558 DCHECK(!(*can_be_skipped)[arc.head_var.value()]);
559 (*can_be_skipped)[arc.head_var.value()] =
true;
560 tmp_vector_.push_back(arc.head_var.value());
567void PrecedencesPropagator::AnalyzePositiveCycle(
568 ArcIndex first_arc, Trail* trail, std::vector<Literal>* must_be_all_true,
569 std::vector<Literal>* literal_reason,
570 std::vector<IntegerLiteral>* integer_reason) {
571 must_be_all_true->clear();
572 literal_reason->clear();
573 integer_reason->clear();
576 const IntegerVariable first_arc_head = arcs_[first_arc].head_var;
578 std::vector<ArcIndex> arc_on_cycle;
584 const int num_nodes = impacted_arcs_.
size();
585 while (arc_on_cycle.size() <= num_nodes) {
586 arc_on_cycle.push_back(arc_index);
587 const ArcInfo& arc = arcs_[arc_index];
588 if (arc.tail_var == first_arc_head)
break;
589 arc_index = bf_parent_arc_of_[arc.tail_var.value()];
592 CHECK_NE(arc_on_cycle.size(), num_nodes + 1) <<
"Infinite loop.";
596 for (
const ArcIndex arc_index : arc_on_cycle) {
597 const ArcInfo& arc = arcs_[arc_index];
598 sum += ArcOffset(arc);
599 AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
601 for (
const Literal l : arc.presence_literals) {
602 literal_reason->push_back(l.Negated());
610 if (integer_trail_->
IsOptional(arc.head_var)) {
611 must_be_all_true->push_back(
626bool PrecedencesPropagator::BellmanFordTarjan(Trail* trail) {
627 const int num_nodes = impacted_arcs_.
size();
630 bf_can_be_skipped_.resize(num_nodes,
false);
631 bf_parent_arc_of_.resize(num_nodes,
ArcIndex(-1));
636 while (!bf_queue_.empty()) {
637 const int node = bf_queue_.front();
638 bf_queue_.pop_front();
639 bf_in_queue_[node] =
false;
649 if (bf_can_be_skipped_[node]) {
651 DCHECK(!arcs_[bf_parent_arc_of_[node]].is_marked);
655 const IntegerValue tail_lb =
656 integer_trail_->
LowerBound(IntegerVariable(node));
657 for (
const ArcIndex arc_index : impacted_arcs_[IntegerVariable(node)]) {
658 const ArcInfo& arc = arcs_[arc_index];
660 const IntegerValue candidate = tail_lb + ArcOffset(arc);
661 if (candidate > integer_trail_->
LowerBound(arc.head_var)) {
663 if (!EnqueueAndCheck(arc, candidate, trail))
return false;
671 if (DisassembleSubtree(arc.head_var.value(), arc.tail_var.value(),
672 &bf_can_be_skipped_)) {
673 std::vector<Literal> must_be_all_true;
674 AnalyzePositiveCycle(arc_index, trail, &must_be_all_true,
675 &literal_reason_, &integer_reason_);
676 if (must_be_all_true.empty()) {
681 for (
const Literal l : must_be_all_true) {
683 literal_reason_.push_back(l);
688 for (
const Literal l : must_be_all_true) {
703 if (bf_parent_arc_of_[arc.head_var.value()] != -1) {
704 arcs_[bf_parent_arc_of_[arc.head_var.value()]].is_marked =
false;
713 const IntegerValue new_bound = integer_trail_->
LowerBound(arc.head_var);
714 if (new_bound == candidate) {
715 bf_parent_arc_of_[arc.head_var.value()] = arc_index;
716 arcs_[arc_index].is_marked =
true;
720 bf_parent_arc_of_[arc.head_var.value()] = -1;
725 bf_can_be_skipped_[arc.head_var.value()] =
false;
726 if (!bf_in_queue_[arc.head_var.value()] && new_bound >= candidate) {
727 bf_queue_.push_back(arc.head_var.value());
728 bf_in_queue_[arc.head_var.value()] =
true;
736int PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraintsFromClause(
737 const absl::Span<const Literal> clause, Model*
model) {
738 CHECK_EQ(
model->GetOrCreate<Trail>()->CurrentDecisionLevel(), 0);
739 if (clause.size() < 2)
return 0;
742 std::vector<ArcInfo> infos;
743 for (
const Literal l : clause) {
744 if (l.Index() >= literal_to_new_impacted_arcs_.
size())
continue;
745 for (
const ArcIndex arc_index : literal_to_new_impacted_arcs_[l.Index()]) {
746 const ArcInfo& arc = arcs_[arc_index];
747 if (arc.presence_literals.size() != 1)
continue;
754 if (infos.size() <= 1)
return 0;
758 std::stable_sort(infos.begin(), infos.end(),
759 [](
const ArcInfo&
a,
const ArcInfo&
b) {
760 return a.head_var < b.head_var;
764 int num_added_constraints = 0;
765 auto* solver =
model->GetOrCreate<SatSolver>();
766 for (
int i = 0; i < infos.size();) {
768 const IntegerVariable head_var = infos[start].head_var;
769 for (i++; i < infos.size() && infos[i].head_var == head_var; ++i) {
771 const absl::Span<ArcInfo> arcs(&infos[start], i - start);
774 if (arcs.size() < 2)
continue;
779 if (arcs.size() + 1 < clause.size())
continue;
781 std::vector<IntegerVariable> vars;
782 std::vector<IntegerValue> offsets;
783 std::vector<Literal> selectors;
784 std::vector<Literal> enforcements;
787 for (
const Literal l : clause) {
789 for (; j < arcs.size() && l == arcs[j].presence_literals.front(); ++j) {
791 vars.push_back(arcs[j].tail_var);
792 offsets.push_back(arcs[j].offset);
799 selectors.push_back(l);
802 enforcements.push_back(l.Negated());
808 if (enforcements.size() + 1 == clause.size())
continue;
810 ++num_added_constraints;
813 if (!solver->FinishPropagation())
return num_added_constraints;
815 return num_added_constraints;
818int PrecedencesPropagator::
819 AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(Model*
model) {
821 auto* solver =
model->GetOrCreate<SatSolver>();
825 for (
ArcIndex arc_index(0); arc_index < arcs_.
size(); ++arc_index) {
826 const ArcInfo& arc = arcs_[arc_index];
830 if (arc.tail_var == arc.head_var)
continue;
831 if (arc.presence_literals.size() != 1)
continue;
833 if (arc.head_var >= incoming_arcs_.size()) {
834 incoming_arcs_.
resize(arc.head_var.value() + 1);
836 incoming_arcs_[arc.head_var].push_back(arc_index);
839 int num_added_constraints = 0;
840 for (IntegerVariable target(0); target < incoming_arcs_.size(); ++target) {
841 if (incoming_arcs_[target].size() <= 1)
continue;
842 if (
time_limit->LimitReached())
return num_added_constraints;
847 solver->Backtrack(0);
848 if (solver->IsModelUnsat())
return num_added_constraints;
849 std::vector<Literal> clause;
850 for (
const ArcIndex arc_index : incoming_arcs_[target]) {
851 const Literal
literal = arcs_[arc_index].presence_literals.
front();
852 if (solver->Assignment().LiteralIsFalse(
literal))
continue;
854 const int old_level = solver->CurrentDecisionLevel();
855 solver->EnqueueDecisionAndBacktrackOnConflict(
literal.Negated());
856 if (solver->IsModelUnsat())
return num_added_constraints;
857 const int new_level = solver->CurrentDecisionLevel();
858 if (new_level <= old_level) {
859 clause = solver->GetLastIncompatibleDecisions();
863 solver->Backtrack(0);
865 if (clause.size() > 1) {
867 const std::set<Literal> clause_set(clause.begin(), clause.end());
868 std::vector<ArcIndex> arcs_in_clause;
869 for (
const ArcIndex arc_index : incoming_arcs_[target]) {
870 const Literal
literal(arcs_[arc_index].presence_literals.front());
872 arcs_in_clause.push_back(arc_index);
876 VLOG(2) << arcs_in_clause.size() <<
"/" << incoming_arcs_[target].size();
878 ++num_added_constraints;
879 std::vector<IntegerVariable> vars;
880 std::vector<IntegerValue> offsets;
881 std::vector<Literal> selectors;
882 for (
const ArcIndex a : arcs_in_clause) {
883 vars.push_back(arcs_[
a].tail_var);
884 offsets.push_back(arcs_[
a].offset);
885 selectors.push_back(Literal(arcs_[
a].presence_literals.front()));
888 if (!solver->FinishPropagation())
return num_added_constraints;
892 return num_added_constraints;
896 VLOG(1) <<
"Detecting GreaterThanAtLeastOneOf() constraints...";
900 int num_added_constraints = 0;
908 if (clauses->AllClausesInCreationOrder().size() < 1e6) {
916 for (
const SatClause* clause : clauses->AllClausesInCreationOrder()) {
917 if (
time_limit->LimitReached())
return num_added_constraints;
918 if (solver->IsModelUnsat())
return num_added_constraints;
919 num_added_constraints += AddGreaterThanAtLeastOneOfConstraintsFromClause(
920 clause->AsSpan(),
model);
923 num_added_constraints +=
924 AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(
model);
927 VLOG(1) <<
"Added " << num_added_constraints
928 <<
" GreaterThanAtLeastOneOf() constraints.";
929 return num_added_constraints;
#define DCHECK_NE(val1, val2)
#define CHECK_EQ(val1, val2)
#define CHECK_GT(val1, val2)
#define CHECK_NE(val1, val2)
#define DCHECK_GT(val1, val2)
#define DCHECK(condition)
#define DCHECK_EQ(val1, val2)
#define VLOG(verboselevel)
void resize(size_type new_size)
void push_back(const value_type &x)
void Set(IntegerType index)
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
void ClearAndResize(IntegerType size)
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
bool IsCurrentlyIgnored(IntegerVariable i) const
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
bool ReportConflict(absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
IntegerValue UpperBound(IntegerVariable i) const
void RelaxLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const
IntegerValue LowerBound(IntegerVariable i) const
IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const
Literal IsIgnoredLiteral(IntegerVariable i) const
bool IsOptional(IntegerVariable i) const
IntegerVariable NumIntegerVariables() const
Class that owns everything related to a particular optimization model.
void AddPrecedenceReason(int arc_index, IntegerValue min_offset, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason) const
void ComputePrecedences(const std::vector< IntegerVariable > &vars, std::vector< IntegerPrecedences > *output)
int AddGreaterThanAtLeastOneOfConstraints(Model *model)
void Untrail(const Trail &trail, int trail_index) final
bool PropagateOutgoingArcs(IntegerVariable var)
int propagation_trail_index_
const VariablesAssignment & Assignment() const
int CurrentDecisionLevel() const
bool LiteralIsTrue(Literal literal) const
bool LiteralIsFalse(Literal literal) const
SharedTimeLimit * time_limit
absl::Cleanup< absl::decay_t< Callback > > MakeCleanup(Callback &&callback)
bool ContainsKey(const Collection &collection, const Key &key)
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
const IntegerVariable kNoIntegerVariable(-1)
std::function< void(Model *)> GreaterThanAtLeastOneOf(IntegerVariable target_var, const absl::Span< const IntegerVariable > vars, const absl::Span< const IntegerValue > offsets, const absl::Span< const Literal > selectors)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)