30 void AppendLowerBoundReasonIfValid(IntegerVariable
var,
31 const IntegerTrail& i_trail,
32 std::vector<IntegerLiteral>* reason) {
34 reason->push_back(i_trail.LowerBoundAsLiteral(
var));
43 while (propagation_trail_index_ < trail_->
Index()) {
45 if (
literal.Index() >= literal_to_new_impacted_arcs_.
size())
continue;
50 literal_to_new_impacted_arcs_[
literal.Index()]) {
51 if (--arc_counts_[arc_index] == 0) {
52 const ArcInfo& arc = arcs_[arc_index];
53 impacted_arcs_[arc.tail_var].
push_back(arc_index);
60 literal_to_new_impacted_arcs_[
literal.Index()]) {
61 if (arc_counts_[arc_index] > 0)
continue;
62 const ArcInfo& arc = arcs_[arc_index];
64 const IntegerValue new_head_lb =
65 integer_trail_->
LowerBound(arc.tail_var) + ArcOffset(arc);
66 if (new_head_lb > integer_trail_->
LowerBound(arc.head_var)) {
67 if (!EnqueueAndCheck(arc, new_head_lb, trail_))
return false;
73 InitializeBFQueueWithModifiedNodes();
74 if (!BellmanFordTarjan(trail_))
return false;
84 DCHECK(NoPropagationLeft(*trail_));
88 PropagateOptionalArcs(trail_);
96 for (
const ArcIndex arc_index : impacted_arcs_[
var]) {
97 const ArcInfo& arc = arcs_[arc_index];
99 const IntegerValue new_head_lb =
100 integer_trail_->
LowerBound(arc.tail_var) + ArcOffset(arc);
101 if (new_head_lb > integer_trail_->
LowerBound(arc.head_var)) {
102 if (!EnqueueAndCheck(arc, new_head_lb, trail_))
return false;
117 if (
literal.Index() >= literal_to_new_impacted_arcs_.
size())
continue;
119 literal_to_new_impacted_arcs_[
literal.Index()]) {
120 if (arc_counts_[arc_index]++ == 0) {
121 const ArcInfo& arc = arcs_[arc_index];
122 impacted_arcs_[arc.tail_var].
pop_back();
133 const std::vector<IntegerVariable>& vars,
134 std::vector<IntegerPrecedences>* output) {
135 tmp_sorted_vars_.clear();
136 tmp_precedences_.clear();
138 const IntegerVariable
var = vars[
index];
140 if (
var >= impacted_arcs_.
size())
continue;
141 for (
const ArcIndex arc_index : impacted_arcs_[
var]) {
142 const ArcInfo& arc = arcs_[arc_index];
145 IntegerValue offset = arc.offset;
147 offset += integer_trail_->
LowerBound(arc.offset_var);
154 if (offset < 0)
continue;
156 if (var_to_degree_[arc.head_var] == 0) {
157 tmp_sorted_vars_.push_back(
158 {arc.head_var, integer_trail_->
LowerBound(arc.head_var)});
164 if (var_to_last_index_[arc.head_var] ==
index)
continue;
166 var_to_last_index_[arc.head_var] =
index;
167 var_to_degree_[arc.head_var]++;
168 tmp_precedences_.push_back(
169 {
index, arc.head_var, arc_index.value(), offset});
180 std::sort(tmp_sorted_vars_.begin(), tmp_sorted_vars_.end());
186 for (
const SortedVar pair : tmp_sorted_vars_) {
187 const int degree = var_to_degree_[pair.var];
189 var_to_degree_[pair.var] = start;
193 var_to_degree_[pair.var] = -1;
196 output->resize(start);
198 if (var_to_degree_[precedence.var] < 0)
continue;
199 (*output)[var_to_degree_[precedence.var]++] = precedence;
204 for (
const SortedVar pair : tmp_sorted_vars_) {
205 var_to_degree_[pair.var] = 0;
210 int arc_index, IntegerValue min_offset,
211 std::vector<Literal>* literal_reason,
212 std::vector<IntegerLiteral>* integer_reason)
const {
213 const ArcInfo& arc = arcs_[
ArcIndex(arc_index)];
214 for (
const Literal l : arc.presence_literals) {
215 literal_reason->push_back(l.
Negated());
220 arc.offset_var, min_offset - arc.offset));
224 void PrecedencesPropagator::AdjustSizeFor(IntegerVariable i) {
239 void PrecedencesPropagator::AddArc(
240 IntegerVariable
tail, IntegerVariable
head, IntegerValue offset,
241 IntegerVariable offset_var, absl::Span<const Literal> presence_literals) {
248 absl::InlinedVector<Literal, 6> enforcement_literals;
250 for (
const Literal l : presence_literals) {
251 enforcement_literals.push_back(l);
254 enforcement_literals.push_back(
258 enforcement_literals.push_back(
263 enforcement_literals.push_back(
268 for (
const Literal l : enforcement_literals) {
274 enforcement_literals[new_size++] = l;
276 enforcement_literals.resize(new_size);
283 VLOG(1) <<
"Self arc! This could be presolved. "
284 <<
"var:" <<
tail <<
" offset:" << offset
285 <<
" offset_var:" << offset_var
286 <<
" conditioned_by:" << presence_literals;
292 const IntegerValue lb = integer_trail_->
LowerBound(offset_var);
293 if (lb == integer_trail_->
UpperBound(offset_var)) {
300 if (!enforcement_literals.empty()) {
301 const OptionalArcIndex arc_index(potential_arcs_.
size());
303 {
tail,
head, offset, offset_var, enforcement_literals});
307 impacted_potential_arcs_[offset_var].
push_back(arc_index);
313 IntegerVariable tail_var;
314 IntegerVariable head_var;
315 IntegerVariable offset_var;
317 std::vector<InternalArc> to_add;
325 to_add.push_back({
tail,
head, offset_var});
326 to_add.push_back({offset_var,
head,
tail});
334 for (
const InternalArc
a : to_add) {
349 modified_vars_.
Set(
a.tail_var);
355 {
a.tail_var,
a.head_var, offset,
a.offset_var, enforcement_literals});
356 auto& presence_literals = arcs_.
back().presence_literals;
360 const Literal to_remove =
362 const auto it = std::find(presence_literals.begin(),
363 presence_literals.end(), to_remove);
364 if (it != presence_literals.end()) presence_literals.erase(it);
367 if (presence_literals.empty()) {
368 impacted_arcs_[
a.tail_var].
push_back(arc_index);
370 for (
const Literal l : presence_literals) {
371 if (l.Index() >= literal_to_new_impacted_arcs_.
size()) {
372 literal_to_new_impacted_arcs_.
resize(l.Index().value() + 1);
374 literal_to_new_impacted_arcs_[l.Index()].
push_back(arc_index);
377 arc_counts_.
push_back(presence_literals.size());
386 void PrecedencesPropagator::PropagateOptionalArcs(Trail* trail) {
389 if (
var >= impacted_potential_arcs_.
size())
continue;
393 for (
const OptionalArcIndex arc_index : impacted_potential_arcs_[
var]) {
394 const ArcInfo& arc = potential_arcs_[arc_index];
395 int num_not_true = 0;
396 Literal to_propagate;
397 for (
const Literal l : arc.presence_literals) {
398 if (!trail->Assignment().LiteralIsTrue(l)) {
403 if (num_not_true != 1)
continue;
404 if (trail->Assignment().LiteralIsFalse(to_propagate))
continue;
408 const IntegerValue tail_lb = integer_trail_->
LowerBound(arc.tail_var);
409 const IntegerValue head_ub = integer_trail_->
UpperBound(arc.head_var);
410 if (tail_lb + ArcOffset(arc) > head_ub) {
411 integer_reason_.clear();
412 integer_reason_.push_back(
414 integer_reason_.push_back(
416 AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
418 literal_reason_.clear();
419 for (
const Literal l : arc.presence_literals) {
420 if (l != to_propagate) literal_reason_.push_back(l.Negated());
422 integer_trail_->
EnqueueLiteral(to_propagate.Negated(), literal_reason_,
429 IntegerValue PrecedencesPropagator::ArcOffset(
const ArcInfo& arc)
const {
432 : integer_trail_->
LowerBound(arc.offset_var));
435 bool PrecedencesPropagator::EnqueueAndCheck(
const ArcInfo& arc,
436 IntegerValue new_head_lb,
445 literal_reason_.clear();
446 for (
const Literal l : arc.presence_literals) {
447 literal_reason_.push_back(l.Negated());
450 integer_reason_.clear();
452 AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
463 if (new_head_lb > integer_trail_->
UpperBound(arc.head_var)) {
464 const IntegerValue slack =
465 new_head_lb - integer_trail_->
UpperBound(arc.head_var) - 1;
466 integer_reason_.push_back(
468 std::vector<IntegerValue> coeffs(integer_reason_.size(), IntegerValue(1));
471 if (!integer_trail_->
IsOptional(arc.head_var)) {
472 return integer_trail_->
ReportConflict(literal_reason_, integer_reason_);
476 if (trail->Assignment().LiteralIsFalse(l)) {
477 literal_reason_.push_back(l);
478 return integer_trail_->
ReportConflict(literal_reason_, integer_reason_);
480 integer_trail_->
EnqueueLiteral(l, literal_reason_, integer_reason_);
486 return integer_trail_->
Enqueue(
488 literal_reason_, integer_reason_);
491 bool PrecedencesPropagator::NoPropagationLeft(
const Trail& trail)
const {
492 const int num_nodes = impacted_arcs_.
size();
493 for (IntegerVariable
var(0);
var < num_nodes; ++
var) {
494 for (
const ArcIndex arc_index : impacted_arcs_[
var]) {
495 const ArcInfo& arc = arcs_[arc_index];
497 if (integer_trail_->
LowerBound(arc.tail_var) + ArcOffset(arc) >
506 void PrecedencesPropagator::InitializeBFQueueWithModifiedNodes() {
509 const int num_nodes = impacted_arcs_.
size();
510 bf_in_queue_.resize(num_nodes,
false);
511 for (
const int node : bf_queue_) bf_in_queue_[node] =
false;
513 DCHECK(std::none_of(bf_in_queue_.begin(), bf_in_queue_.end(),
514 [](
bool v) { return v; }));
516 if (
var >= num_nodes)
continue;
517 bf_queue_.push_back(
var.value());
518 bf_in_queue_[
var.value()] =
true;
522 void PrecedencesPropagator::CleanUpMarkedArcsAndParents() {
525 const int num_nodes = impacted_arcs_.
size();
527 if (
var >= num_nodes)
continue;
528 const ArcIndex parent_arc_index = bf_parent_arc_of_[
var.value()];
529 if (parent_arc_index != -1) {
530 arcs_[parent_arc_index].is_marked =
false;
531 bf_parent_arc_of_[
var.value()] = -1;
532 bf_can_be_skipped_[
var.value()] =
false;
535 DCHECK(std::none_of(bf_parent_arc_of_.begin(), bf_parent_arc_of_.end(),
536 [](
ArcIndex v) { return v != -1; }));
537 DCHECK(std::none_of(bf_can_be_skipped_.begin(), bf_can_be_skipped_.end(),
538 [](
bool v) { return v; }));
541 bool PrecedencesPropagator::DisassembleSubtree(
542 int source,
int target, std::vector<bool>* can_be_skipped) {
546 tmp_vector_.push_back(source);
547 while (!tmp_vector_.empty()) {
548 const int tail = tmp_vector_.back();
549 tmp_vector_.pop_back();
550 for (
const ArcIndex arc_index : impacted_arcs_[IntegerVariable(
tail)]) {
551 const ArcInfo& arc = arcs_[arc_index];
553 arc.is_marked =
false;
554 if (arc.head_var.value() == target)
return true;
555 DCHECK(!(*can_be_skipped)[arc.head_var.value()]);
556 (*can_be_skipped)[arc.head_var.value()] =
true;
557 tmp_vector_.push_back(arc.head_var.value());
564 void PrecedencesPropagator::AnalyzePositiveCycle(
565 ArcIndex first_arc, Trail* trail, std::vector<Literal>* must_be_all_true,
566 std::vector<Literal>* literal_reason,
567 std::vector<IntegerLiteral>* integer_reason) {
568 must_be_all_true->clear();
569 literal_reason->clear();
570 integer_reason->clear();
573 const IntegerVariable first_arc_head = arcs_[first_arc].head_var;
575 std::vector<ArcIndex> arc_on_cycle;
581 const int num_nodes = impacted_arcs_.
size();
582 while (arc_on_cycle.size() <= num_nodes) {
583 arc_on_cycle.push_back(arc_index);
584 const ArcInfo& arc = arcs_[arc_index];
585 if (arc.tail_var == first_arc_head)
break;
586 arc_index = bf_parent_arc_of_[arc.tail_var.value()];
589 CHECK_NE(arc_on_cycle.size(), num_nodes + 1) <<
"Infinite loop.";
593 for (
const ArcIndex arc_index : arc_on_cycle) {
594 const ArcInfo& arc = arcs_[arc_index];
595 sum += ArcOffset(arc);
596 AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
598 for (
const Literal l : arc.presence_literals) {
599 literal_reason->push_back(l.Negated());
607 if (integer_trail_->
IsOptional(arc.head_var)) {
608 must_be_all_true->push_back(
623 bool PrecedencesPropagator::BellmanFordTarjan(Trail* trail) {
624 const int num_nodes = impacted_arcs_.
size();
627 bf_can_be_skipped_.resize(num_nodes,
false);
628 bf_parent_arc_of_.resize(num_nodes,
ArcIndex(-1));
633 while (!bf_queue_.empty()) {
634 const int node = bf_queue_.front();
635 bf_queue_.pop_front();
636 bf_in_queue_[node] =
false;
646 if (bf_can_be_skipped_[node]) {
648 DCHECK(!arcs_[bf_parent_arc_of_[node]].is_marked);
652 const IntegerValue tail_lb =
653 integer_trail_->
LowerBound(IntegerVariable(node));
654 for (
const ArcIndex arc_index : impacted_arcs_[IntegerVariable(node)]) {
655 const ArcInfo& arc = arcs_[arc_index];
657 const IntegerValue candidate = tail_lb + ArcOffset(arc);
658 if (candidate > integer_trail_->
LowerBound(arc.head_var)) {
660 if (!EnqueueAndCheck(arc, candidate, trail))
return false;
668 if (DisassembleSubtree(arc.head_var.value(), arc.tail_var.value(),
669 &bf_can_be_skipped_)) {
670 std::vector<Literal> must_be_all_true;
671 AnalyzePositiveCycle(arc_index, trail, &must_be_all_true,
672 &literal_reason_, &integer_reason_);
673 if (must_be_all_true.empty()) {
678 for (
const Literal l : must_be_all_true) {
680 literal_reason_.push_back(l);
685 for (
const Literal l : must_be_all_true) {
700 if (bf_parent_arc_of_[arc.head_var.value()] != -1) {
701 arcs_[bf_parent_arc_of_[arc.head_var.value()]].is_marked =
false;
710 const IntegerValue new_bound = integer_trail_->
LowerBound(arc.head_var);
711 if (new_bound == candidate) {
712 bf_parent_arc_of_[arc.head_var.value()] = arc_index;
713 arcs_[arc_index].is_marked =
true;
717 bf_parent_arc_of_[arc.head_var.value()] = -1;
722 bf_can_be_skipped_[arc.head_var.value()] =
false;
723 if (!bf_in_queue_[arc.head_var.value()] && new_bound >= candidate) {
724 bf_queue_.push_back(arc.head_var.value());
725 bf_in_queue_[arc.head_var.value()] =
true;
733 int PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraintsFromClause(
734 const absl::Span<const Literal> clause, Model*
model) {
735 CHECK_EQ(
model->GetOrCreate<Trail>()->CurrentDecisionLevel(), 0);
736 if (clause.size() < 2)
return 0;
739 std::vector<ArcInfo> infos;
740 for (
const Literal l : clause) {
741 if (l.Index() >= literal_to_new_impacted_arcs_.
size())
continue;
742 for (
const ArcIndex arc_index : literal_to_new_impacted_arcs_[l.Index()]) {
743 const ArcInfo& arc = arcs_[arc_index];
744 if (arc.presence_literals.size() != 1)
continue;
748 infos.push_back(arc);
751 if (infos.size() <= 1)
return 0;
755 std::stable_sort(infos.begin(), infos.end(),
756 [](
const ArcInfo&
a,
const ArcInfo&
b) {
757 return a.head_var < b.head_var;
761 int num_added_constraints = 0;
762 auto* solver =
model->GetOrCreate<SatSolver>();
763 for (
int i = 0; i < infos.size();) {
765 const IntegerVariable head_var = infos[start].head_var;
766 for (i++; i < infos.size() && infos[i].head_var == head_var; ++i) {
768 const absl::Span<ArcInfo> arcs(&infos[start], i - start);
771 if (arcs.size() < 2)
continue;
776 if (arcs.size() + 1 < clause.size())
continue;
778 std::vector<IntegerVariable> vars;
779 std::vector<IntegerValue> offsets;
780 std::vector<Literal> selectors;
781 std::vector<Literal> enforcements;
784 for (
const Literal l : clause) {
786 for (; j < arcs.size() && l == arcs[j].presence_literals.front(); ++j) {
788 vars.push_back(arcs[j].tail_var);
789 offsets.push_back(arcs[j].offset);
796 selectors.push_back(l);
799 enforcements.push_back(l.Negated());
805 if (enforcements.size() + 1 == clause.size())
continue;
807 ++num_added_constraints;
810 if (!solver->FinishPropagation())
return num_added_constraints;
812 return num_added_constraints;
815 int PrecedencesPropagator::
816 AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(Model*
model) {
818 auto* solver =
model->GetOrCreate<SatSolver>();
822 for (
ArcIndex arc_index(0); arc_index < arcs_.
size(); ++arc_index) {
823 const ArcInfo& arc = arcs_[arc_index];
827 if (arc.tail_var == arc.head_var)
continue;
828 if (arc.presence_literals.size() != 1)
continue;
830 if (arc.head_var >= incoming_arcs_.size()) {
831 incoming_arcs_.
resize(arc.head_var.value() + 1);
833 incoming_arcs_[arc.head_var].push_back(arc_index);
836 int num_added_constraints = 0;
837 for (IntegerVariable target(0); target < incoming_arcs_.size(); ++target) {
838 if (incoming_arcs_[target].size() <= 1)
continue;
839 if (
time_limit->LimitReached())
return num_added_constraints;
844 solver->Backtrack(0);
845 if (solver->IsModelUnsat())
return num_added_constraints;
846 std::vector<Literal> clause;
847 for (
const ArcIndex arc_index : incoming_arcs_[target]) {
848 const Literal
literal = arcs_[arc_index].presence_literals.
front();
849 if (solver->Assignment().LiteralIsFalse(
literal))
continue;
851 const int old_level = solver->CurrentDecisionLevel();
852 solver->EnqueueDecisionAndBacktrackOnConflict(
literal.Negated());
853 if (solver->IsModelUnsat())
return num_added_constraints;
854 const int new_level = solver->CurrentDecisionLevel();
855 if (new_level <= old_level) {
856 clause = solver->GetLastIncompatibleDecisions();
860 solver->Backtrack(0);
862 if (clause.size() > 1) {
864 const std::set<Literal> clause_set(clause.begin(), clause.end());
865 std::vector<ArcIndex> arcs_in_clause;
866 for (
const ArcIndex arc_index : incoming_arcs_[target]) {
867 const Literal
literal(arcs_[arc_index].presence_literals.front());
869 arcs_in_clause.push_back(arc_index);
873 VLOG(2) << arcs_in_clause.size() <<
"/" << incoming_arcs_[target].size();
875 ++num_added_constraints;
876 std::vector<IntegerVariable> vars;
877 std::vector<IntegerValue> offsets;
878 std::vector<Literal> selectors;
879 for (
const ArcIndex a : arcs_in_clause) {
880 vars.push_back(arcs_[
a].tail_var);
881 offsets.push_back(arcs_[
a].offset);
882 selectors.push_back(Literal(arcs_[
a].presence_literals.front()));
885 if (!solver->FinishPropagation())
return num_added_constraints;
889 return num_added_constraints;
893 VLOG(1) <<
"Detecting GreaterThanAtLeastOneOf() constraints...";
897 int num_added_constraints = 0;
905 if (clauses->AllClausesInCreationOrder().size() < 1e6) {
913 for (
const SatClause* clause : clauses->AllClausesInCreationOrder()) {
914 if (
time_limit->LimitReached())
return num_added_constraints;
915 if (solver->IsModelUnsat())
return num_added_constraints;
916 num_added_constraints += AddGreaterThanAtLeastOneOfConstraintsFromClause(
917 clause->AsSpan(),
model);
920 num_added_constraints +=
921 AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(
model);
924 VLOG(1) <<
"Added " << num_added_constraints
925 <<
" GreaterThanAtLeastOneOf() constraints.";
926 return num_added_constraints;