always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
ed397541f451dc19ac866b7e382174faee8ed839
ortools-clone/ortools/sat/old_precedences_propagator.cc

668 lines
27 KiB
C++
Raw Blame History

// Copyright 2010-2025 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#include "ortools/sat/old_precedences_propagator.h"
#include <stdint.h>
#include <algorithm>
#include <deque>
#include <string>
#include <utility>
#include <vector>
#include "absl/cleanup/cleanup.h"
#include "absl/container/inlined_vector.h"
#include "absl/log/check.h"
#include "absl/log/log.h"
#include "absl/log/vlog_is_on.h"
#include "absl/types/span.h"
#include "ortools/base/logging.h"
#include "ortools/base/stl_util.h"
#include "ortools/base/strong_vector.h"
#include "ortools/sat/integer.h"
#include "ortools/sat/integer_base.h"
#include "ortools/sat/sat_base.h"
#include "ortools/sat/synchronization.h"
#include "ortools/util/bitset.h"
#include "ortools/util/strong_integers.h"
namespace operations_research {
namespace sat {
namespace {
void AppendLowerBoundReasonIfValid(IntegerVariable var,
const IntegerTrail& i_trail,
std::vector<IntegerLiteral>* reason) {
if (var != kNoIntegerVariable) {
reason->push_back(i_trail.LowerBoundAsLiteral(var));
}
}
} // namespace
PrecedencesPropagator::~PrecedencesPropagator() {
if (!VLOG_IS_ON(1)) return;
if (shared_stats_ == nullptr) return;
std::vector<std::pair<std::string, int64_t>> stats;
stats.push_back({"precedences/num_cycles", num_cycles_});
stats.push_back({"precedences/num_pushes", num_pushes_});
stats.push_back(
{"precedences/num_enforcement_pushes", num_enforcement_pushes_});
shared_stats_->AddStats(stats);
}
bool PrecedencesPropagator::Propagate(Trail* trail) { return Propagate(); }
bool PrecedencesPropagator::Propagate() {
while (propagation_trail_index_ < trail_->Index()) {
const Literal literal = (*trail_)[propagation_trail_index_++];
if (literal.Index() >= literal_to_new_impacted_arcs_.size()) continue;
// IMPORTANT: Because of the way Untrail() work, we need to add all the
// potential arcs before we can abort. It is why we iterate twice here.
for (const ArcIndex arc_index :
literal_to_new_impacted_arcs_[literal.Index()]) {
if (--arc_counts_[arc_index] == 0) {
const ArcInfo& arc = arcs_[arc_index];
PushConditionalRelations(arc);
impacted_arcs_[arc.tail_var].push_back(arc_index);
}
}
// Iterate again to check for a propagation and indirectly update
// modified_vars_.
for (const ArcIndex arc_index :
literal_to_new_impacted_arcs_[literal.Index()]) {
if (arc_counts_[arc_index] > 0) continue;
const ArcInfo& arc = arcs_[arc_index];
const IntegerValue new_head_lb =
integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc);
if (new_head_lb > integer_trail_->LowerBound(arc.head_var)) {
if (!EnqueueAndCheck(arc, new_head_lb, trail_)) return false;
}
}
}
// Do the actual propagation of the IntegerVariable bounds.
InitializeBFQueueWithModifiedNodes();
if (!BellmanFordTarjan(trail_)) return false;
// We can only test that no propagation is left if we didn't enqueue new
// literal in the presence of optional variables.
//
// TODO(user): Because of our code to deal with InPropagationLoop(), this is
// not always true. Find a cleaner way to DCHECK() while not failing in this
// corner case.
if (/*DISABLES CODE*/ (false) &&
propagation_trail_index_ == trail_->Index()) {
DCHECK(NoPropagationLeft(*trail_));
}
// Propagate the presence literals of the arcs that can't be added.
PropagateOptionalArcs(trail_);
// Clean-up modified_vars_ to do as little as possible on the next call.
modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
return true;
}
bool PrecedencesPropagator::PropagateOutgoingArcs(IntegerVariable var) {
CHECK_NE(var, kNoIntegerVariable);
if (var >= impacted_arcs_.size()) return true;
for (const ArcIndex arc_index : impacted_arcs_[var]) {
const ArcInfo& arc = arcs_[arc_index];
const IntegerValue new_head_lb =
integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc);
if (new_head_lb > integer_trail_->LowerBound(arc.head_var)) {
if (!EnqueueAndCheck(arc, new_head_lb, trail_)) return false;
}
}
return true;
}
// TODO(user): Remove literal fixed at level zero from there.
void PrecedencesPropagator::PushConditionalRelations(const ArcInfo& arc) {
// We currently do not handle variable size in the reasons.
// TODO(user): we could easily take a level zero ArcOffset() instead, or
// add this to the reason though.
if (arc.offset_var != kNoIntegerVariable) return;
const IntegerValue offset = ArcOffset(arc);
relations_->PushConditionalRelation(
arc.presence_literals,
LinearExpression2::Difference(arc.tail_var, arc.head_var), -offset);
}
void PrecedencesPropagator::Untrail(const Trail& trail, int trail_index) {
if (propagation_trail_index_ > trail_index) {
// This means that we already propagated all there is to propagate
// at the level trail_index, so we can safely clear modified_vars_ in case
// it wasn't already done.
modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
}
while (propagation_trail_index_ > trail_index) {
const Literal literal = trail[--propagation_trail_index_];
if (literal.Index() >= literal_to_new_impacted_arcs_.size()) continue;
for (const ArcIndex arc_index :
literal_to_new_impacted_arcs_[literal.Index()]) {
if (arc_counts_[arc_index]++ == 0) {
const ArcInfo& arc = arcs_[arc_index];
impacted_arcs_[arc.tail_var].pop_back();
}
}
}
}
void PrecedencesPropagator::AdjustSizeFor(IntegerVariable i) {
const int index = std::max(i.value(), NegationOf(i).value());
if (index >= impacted_arcs_.size()) {
// TODO(user): only watch lower bound of the relevant variable instead
// of watching everything in [0, max_index_of_variable_used_in_this_class).
for (IntegerVariable var(impacted_arcs_.size()); var <= index; ++var) {
watcher_->WatchLowerBound(var, watcher_id_);
}
impacted_arcs_.resize(index + 1);
impacted_potential_arcs_.resize(index + 1);
}
}
void PrecedencesPropagator::AddArc(
IntegerVariable tail, IntegerVariable head, IntegerValue offset,
IntegerVariable offset_var, absl::Span<const Literal> presence_literals) {
AdjustSizeFor(tail);
AdjustSizeFor(head);
if (offset_var != kNoIntegerVariable) AdjustSizeFor(offset_var);
// This arc is present iff all the literals here are true.
absl::InlinedVector<Literal, 6> enforcement_literals;
{
for (const Literal l : presence_literals) {
enforcement_literals.push_back(l);
}
gtl::STLSortAndRemoveDuplicates(&enforcement_literals);
if (trail_->CurrentDecisionLevel() == 0) {
int new_size = 0;
for (const Literal l : enforcement_literals) {
if (trail_->Assignment().LiteralIsTrue(Literal(l))) {
continue; // At true, ignore this literal.
} else if (trail_->Assignment().LiteralIsFalse(Literal(l))) {
return; // At false, ignore completely this arc.
}
enforcement_literals[new_size++] = l;
}
enforcement_literals.resize(new_size);
}
}
if (head == tail) {
// A self-arc is either plain SAT or plain UNSAT or it forces something on
// the given offset_var or presence_literal_index. In any case it could be
// presolved in something more efficient.
VLOG(1) << "Self arc! This could be presolved. "
<< "var:" << tail << " offset:" << offset
<< " offset_var:" << offset_var
<< " conditioned_by:" << presence_literals;
}
// Remove the offset_var if it is fixed.
// TODO(user): We should also handle the case where tail or head is fixed.
if (offset_var != kNoIntegerVariable) {
const IntegerValue lb = integer_trail_->LevelZeroLowerBound(offset_var);
if (lb == integer_trail_->LevelZeroUpperBound(offset_var)) {
offset += lb;
offset_var = kNoIntegerVariable;
}
}
// Deal first with impacted_potential_arcs_/potential_arcs_.
if (!enforcement_literals.empty()) {
const OptionalArcIndex arc_index(potential_arcs_.size());
potential_arcs_.push_back(
{tail, head, offset, offset_var, enforcement_literals});
impacted_potential_arcs_[tail].push_back(arc_index);
impacted_potential_arcs_[NegationOf(head)].push_back(arc_index);
if (offset_var != kNoIntegerVariable) {
impacted_potential_arcs_[offset_var].push_back(arc_index);
}
}
// Now deal with impacted_arcs_/arcs_.
struct InternalArc {
IntegerVariable tail_var;
IntegerVariable head_var;
IntegerVariable offset_var;
};
std::vector<InternalArc> to_add;
if (offset_var == kNoIntegerVariable) {
// a + offset <= b and -b + offset <= -a
to_add.push_back({tail, head, kNoIntegerVariable});
to_add.push_back({NegationOf(head), NegationOf(tail), kNoIntegerVariable});
} else {
// tail (a) and offset_var (b) are symmetric, so we add:
// - a + b + offset <= c
to_add.push_back({tail, head, offset_var});
to_add.push_back({offset_var, head, tail});
// - a - c + offset <= -b
to_add.push_back({tail, NegationOf(offset_var), NegationOf(head)});
to_add.push_back({NegationOf(head), NegationOf(offset_var), tail});
// - b - c + offset <= -a
to_add.push_back({offset_var, NegationOf(tail), NegationOf(head)});
to_add.push_back({NegationOf(head), NegationOf(tail), offset_var});
}
for (const InternalArc a : to_add) {
// Since we add a new arc, we will need to consider its tail during the next
// propagation. Note that the size of modified_vars_ will be automatically
// updated when new integer variables are created since we register it with
// IntegerTrail in this class constructor.
//
// TODO(user): Adding arcs and then calling Untrail() before Propagate()
// will cause this mecanism to break. Find a more robust implementation.
//
// TODO(user): In some rare corner case, rescanning the whole list of arc
// leaving tail_var can make AddVar() have a quadratic complexity where it
// shouldn't. A better solution would be to see if this new arc currently
// propagate something, and if it does, just update the lower bound of
// a.head_var and let the normal "is modified" mecanism handle any eventual
// follow up propagations.
modified_vars_.Set(a.tail_var);
// If a.head_var is optional, we can potentially remove some literal from
// enforcement_literals.
const ArcIndex arc_index(arcs_.size());
arcs_.push_back(
{a.tail_var, a.head_var, offset, a.offset_var, enforcement_literals});
auto& presence_literals = arcs_.back().presence_literals;
if (presence_literals.empty()) {
impacted_arcs_[a.tail_var].push_back(arc_index);
} else {
for (const Literal l : presence_literals) {
if (l.Index() >= literal_to_new_impacted_arcs_.size()) {
literal_to_new_impacted_arcs_.resize(l.Index().value() + 1);
}
literal_to_new_impacted_arcs_[l.Index()].push_back(arc_index);
}
}
if (trail_->CurrentDecisionLevel() == 0) {
arc_counts_.push_back(presence_literals.size());
} else {
arc_counts_.push_back(0);
for (const Literal l : presence_literals) {
if (!trail_->Assignment().LiteralIsTrue(l)) {
++arc_counts_.back();
}
}
CHECK(presence_literals.empty() || arc_counts_.back() > 0);
}
}
}
bool PrecedencesPropagator::AddPrecedenceWithOffsetIfNew(IntegerVariable i1,
IntegerVariable i2,
IntegerValue offset) {
DCHECK_EQ(trail_->CurrentDecisionLevel(), 0);
if (i1 < impacted_arcs_.size() && i2 < impacted_arcs_.size()) {
for (const ArcIndex index : impacted_arcs_[i1]) {
const ArcInfo& arc = arcs_[index];
if (arc.head_var == i2) {
const IntegerValue current = ArcOffset(arc);
if (offset <= current) {
return false;
} else {
// TODO(user): Modify arc in place!
}
break;
}
}
}
AddPrecedenceWithOffset(i1, i2, offset);
return true;
}
// TODO(user): On jobshop problems with a lot of tasks per machine (500), this
// takes up a big chunk of the running time even before we find a solution.
// This is because, for each lower bound changed, we inspect 500 arcs even
// though they will never be propagated because the other bound is still at the
// horizon. Find an even sparser algorithm?
void PrecedencesPropagator::PropagateOptionalArcs(Trail* trail) {
for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
// The variables are not in increasing order, so we need to continue.
if (var >= impacted_potential_arcs_.size()) continue;
// Note that we can currently check the same ArcInfo up to 3 times, one for
// each of the arc variables: tail, NegationOf(head) and offset_var.
for (const OptionalArcIndex arc_index : impacted_potential_arcs_[var]) {
const ArcInfo& arc = potential_arcs_[arc_index];
int num_not_true = 0;
Literal to_propagate;
for (const Literal l : arc.presence_literals) {
if (!trail->Assignment().LiteralIsTrue(l)) {
++num_not_true;
to_propagate = l;
}
}
if (num_not_true != 1) continue;
if (trail->Assignment().LiteralIsFalse(to_propagate)) continue;
// Test if this arc can be present or not.
// Important arc.tail_var can be different from var here.
const IntegerValue tail_lb = integer_trail_->LowerBound(arc.tail_var);
const IntegerValue head_ub = integer_trail_->UpperBound(arc.head_var);
if (tail_lb + ArcOffset(arc) > head_ub) {
integer_reason_.clear();
integer_reason_.push_back(
integer_trail_->LowerBoundAsLiteral(arc.tail_var));
integer_reason_.push_back(
integer_trail_->UpperBoundAsLiteral(arc.head_var));
AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
&integer_reason_);
literal_reason_.clear();
for (const Literal l : arc.presence_literals) {
if (l != to_propagate) literal_reason_.push_back(l.Negated());
}
++num_enforcement_pushes_;
integer_trail_->EnqueueLiteral(to_propagate.Negated(), literal_reason_,
integer_reason_);
}
}
}
}
IntegerValue PrecedencesPropagator::ArcOffset(const ArcInfo& arc) const {
return arc.offset + (arc.offset_var == kNoIntegerVariable
? IntegerValue(0)
: integer_trail_->LowerBound(arc.offset_var));
}
bool PrecedencesPropagator::EnqueueAndCheck(const ArcInfo& arc,
IntegerValue new_head_lb,
Trail* trail) {
++num_pushes_;
DCHECK_GT(new_head_lb, integer_trail_->LowerBound(arc.head_var));
// Compute the reason for new_head_lb.
//
// TODO(user): do like for clause and keep the negation of
// arc.presence_literals? I think we could change the integer.h API to accept
// true literal like for IntegerVariable, it is really confusing currently.
literal_reason_.clear();
for (const Literal l : arc.presence_literals) {
literal_reason_.push_back(l.Negated());
}
integer_reason_.clear();
integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(arc.tail_var));
AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
&integer_reason_);
// The code works without this block since Enqueue() below can already take
// care of conflicts. However, it is better to deal with the conflict
// ourselves because we can be smarter about the reason this way.
//
// The reason for a "precedence" conflict is always a linear reason
// involving the tail lower_bound, the head upper bound and eventually the
// size lower bound. Because of that, we can use the RelaxLinearReason()
// code.
if (new_head_lb > integer_trail_->UpperBound(arc.head_var)) {
const IntegerValue slack =
new_head_lb - integer_trail_->UpperBound(arc.head_var) - 1;
integer_reason_.push_back(
integer_trail_->UpperBoundAsLiteral(arc.head_var));
std::vector<IntegerValue> coeffs(integer_reason_.size(), IntegerValue(1));
integer_trail_->RelaxLinearReason(slack, coeffs, &integer_reason_);
return integer_trail_->ReportConflict(literal_reason_, integer_reason_);
}
return integer_trail_->Enqueue(
IntegerLiteral::GreaterOrEqual(arc.head_var, new_head_lb),
literal_reason_, integer_reason_);
}
bool PrecedencesPropagator::NoPropagationLeft(const Trail& trail) const {
const int num_nodes = impacted_arcs_.size();
for (IntegerVariable var(0); var < num_nodes; ++var) {
for (const ArcIndex arc_index : impacted_arcs_[var]) {
const ArcInfo& arc = arcs_[arc_index];
if (integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc) >
integer_trail_->LowerBound(arc.head_var)) {
return false;
}
}
}
return true;
}
void PrecedencesPropagator::InitializeBFQueueWithModifiedNodes() {
// Sparse clear of the queue. TODO(user): only use the sparse version if
// queue.size() is small or use SparseBitset.
const int num_nodes = impacted_arcs_.size();
bf_in_queue_.resize(num_nodes, false);
for (const int node : bf_queue_) bf_in_queue_[node] = false;
bf_queue_.clear();
DCHECK(std::none_of(bf_in_queue_.begin(), bf_in_queue_.end(),
[](bool v) { return v; }));
for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
if (var >= num_nodes) continue;
bf_queue_.push_back(var.value());
bf_in_queue_[var.value()] = true;
}
}
void PrecedencesPropagator::CleanUpMarkedArcsAndParents() {
// To be sparse, we use the fact that each node with a parent must be in
// modified_vars_.
const int num_nodes = impacted_arcs_.size();
for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
if (var >= num_nodes) continue;
const ArcIndex parent_arc_index = bf_parent_arc_of_[var.value()];
if (parent_arc_index != -1) {
arcs_[parent_arc_index].is_marked = false;
bf_parent_arc_of_[var.value()] = -1;
bf_can_be_skipped_[var.value()] = false;
}
}
DCHECK(std::none_of(bf_parent_arc_of_.begin(), bf_parent_arc_of_.end(),
[](ArcIndex v) { return v != -1; }));
DCHECK(std::none_of(bf_can_be_skipped_.begin(), bf_can_be_skipped_.end(),
[](bool v) { return v; }));
}
bool PrecedencesPropagator::DisassembleSubtree(
int source, int target, std::vector<bool>* can_be_skipped) {
// Note that we explore a tree, so we can do it in any order, and the one
// below seems to be the fastest.
tmp_vector_.clear();
tmp_vector_.push_back(source);
while (!tmp_vector_.empty()) {
const int tail = tmp_vector_.back();
tmp_vector_.pop_back();
for (const ArcIndex arc_index : impacted_arcs_[IntegerVariable(tail)]) {
const ArcInfo& arc = arcs_[arc_index];
if (arc.is_marked) {
arc.is_marked = false; // mutable.
if (arc.head_var.value() == target) return true;
DCHECK(!(*can_be_skipped)[arc.head_var.value()]);
(*can_be_skipped)[arc.head_var.value()] = true;
tmp_vector_.push_back(arc.head_var.value());
}
}
}
return false;
}
void PrecedencesPropagator::AnalyzePositiveCycle(
ArcIndex first_arc, Trail* trail, std::vector<Literal>* must_be_all_true,
std::vector<Literal>* literal_reason,
std::vector<IntegerLiteral>* integer_reason) {
must_be_all_true->clear();
literal_reason->clear();
integer_reason->clear();
// Follow bf_parent_arc_of_[] to find the cycle containing first_arc.
const IntegerVariable first_arc_head = arcs_[first_arc].head_var;
ArcIndex arc_index = first_arc;
std::vector<ArcIndex> arc_on_cycle;
// Just to be safe and avoid an infinite loop we use the fact that the maximum
// cycle size on a graph with n nodes is of size n. If we have more in the
// code below, it means first_arc is not part of a cycle according to
// bf_parent_arc_of_[], which should never happen.
const int num_nodes = impacted_arcs_.size();
while (arc_on_cycle.size() <= num_nodes) {
arc_on_cycle.push_back(arc_index);
const ArcInfo& arc = arcs_[arc_index];
if (arc.tail_var == first_arc_head) break;
arc_index = bf_parent_arc_of_[arc.tail_var.value()];
CHECK_NE(arc_index, ArcIndex(-1));
}
CHECK_NE(arc_on_cycle.size(), num_nodes + 1) << "Infinite loop.";
// Compute the reason for this cycle.
IntegerValue sum(0);
for (const ArcIndex arc_index : arc_on_cycle) {
const ArcInfo& arc = arcs_[arc_index];
sum += ArcOffset(arc);
AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
integer_reason);
for (const Literal l : arc.presence_literals) {
literal_reason->push_back(l.Negated());
}
}
// TODO(user): what if the sum overflow? this is just a check so I guess
// we don't really care, but fix the issue.
CHECK_GT(sum, 0);
}
// Note that in our settings it is important to use an algorithm that tries to
// minimize the number of integer_trail_->Enqueue() as much as possible.
//
// TODO(user): The current algorithm is quite efficient, but there is probably
// still room for improvements.
bool PrecedencesPropagator::BellmanFordTarjan(Trail* trail) {
const int num_nodes = impacted_arcs_.size();
// These vector are reset by CleanUpMarkedArcsAndParents() so resize is ok.
bf_can_be_skipped_.resize(num_nodes, false);
bf_parent_arc_of_.resize(num_nodes, ArcIndex(-1));
const auto cleanup =
::absl::MakeCleanup([this]() { CleanUpMarkedArcsAndParents(); });
// The queue initialization is done by InitializeBFQueueWithModifiedNodes().
while (!bf_queue_.empty()) {
const int node = bf_queue_.front();
bf_queue_.pop_front();
bf_in_queue_[node] = false;
// TODO(user): we don't need bf_can_be_skipped_ since we can detect this
// if this node has a parent arc which is not marked. Investigate if it is
// faster without the vector<bool>.
//
// TODO(user): An alternative algorithm is to remove all these nodes from
// the queue instead of simply marking them. This should also lead to a
// better "relaxation" order of the arcs. It is however a bit more work to
// remove them since we need to track their position.
if (bf_can_be_skipped_[node]) {
DCHECK_NE(bf_parent_arc_of_[node], -1);
DCHECK(!arcs_[bf_parent_arc_of_[node]].is_marked);
continue;
}
const IntegerValue tail_lb =
integer_trail_->LowerBound(IntegerVariable(node));
for (const ArcIndex arc_index : impacted_arcs_[IntegerVariable(node)]) {
const ArcInfo& arc = arcs_[arc_index];
DCHECK_EQ(arc.tail_var, node);
const IntegerValue candidate = tail_lb + ArcOffset(arc);
if (candidate > integer_trail_->LowerBound(arc.head_var)) {
if (!EnqueueAndCheck(arc, candidate, trail)) return false;
// This is the Tarjan contribution to Bellman-Ford. This code detect
// positive cycle, and because it disassemble the subtree while doing
// so, the cost is amortized during the algorithm execution. Another
// advantages is that it will mark the node explored here as skippable
// which will avoid to propagate them too early (knowing that they will
// need to be propagated again later).
if (DisassembleSubtree(arc.head_var.value(), arc.tail_var.value(),
&bf_can_be_skipped_)) {
std::vector<Literal> must_be_all_true;
AnalyzePositiveCycle(arc_index, trail, &must_be_all_true,
&literal_reason_, &integer_reason_);
if (must_be_all_true.empty()) {
++num_cycles_;
return integer_trail_->ReportConflict(literal_reason_,
integer_reason_);
} else {
gtl::STLSortAndRemoveDuplicates(&must_be_all_true);
for (const Literal l : must_be_all_true) {
if (trail_->Assignment().LiteralIsFalse(l)) {
literal_reason_.push_back(l);
return integer_trail_->ReportConflict(literal_reason_,
integer_reason_);
}
}
for (const Literal l : must_be_all_true) {
if (trail_->Assignment().LiteralIsTrue(l)) continue;
integer_trail_->EnqueueLiteral(l, literal_reason_,
integer_reason_);
}
// We just marked some optional variable as ignored, no need
// to update bf_parent_arc_of_[].
continue;
}
}
// We need to enforce the invariant that only the arc_index in
// bf_parent_arc_of_[] are marked (but not necessarily all of them
// since we unmark some in DisassembleSubtree()).
if (bf_parent_arc_of_[arc.head_var.value()] != -1) {
arcs_[bf_parent_arc_of_[arc.head_var.value()]].is_marked = false;
}
// Tricky: We just enqueued the fact that the lower-bound of head is
// candidate. However, because the domain of head may be discrete, it is
// possible that the lower-bound of head is now higher than candidate!
// If this is the case, we don't update bf_parent_arc_of_[] so that we
// don't wrongly detect a positive weight cycle because of this "extra
// push".
const IntegerValue new_bound = integer_trail_->LowerBound(arc.head_var);
if (new_bound == candidate) {
bf_parent_arc_of_[arc.head_var.value()] = arc_index;
arcs_[arc_index].is_marked = true;
} else {
// We still unmark any previous dependency, since we have pushed the
// value of arc.head_var further.
bf_parent_arc_of_[arc.head_var.value()] = -1;
}
// We do not re-enqueue if we are in a propagation loop and new_bound
// was not pushed to candidate or higher.
bf_can_be_skipped_[arc.head_var.value()] = false;
if (!bf_in_queue_[arc.head_var.value()] && new_bound >= candidate) {
bf_queue_.push_back(arc.head_var.value());
bf_in_queue_[arc.head_var.value()] = true;
}
}
}
}
return true;
}
} // namespace sat
} // namespace operations_research
Reference in New Issue View Git Blame Copy Permalink