OR-Tools  8.2
cp_constraints.cc
Go to the documentation of this file.
1// Copyright 2010-2018 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include <algorithm>
17
18#include "absl/container/flat_hash_map.h"
21#include "ortools/util/sort.h"
22
23namespace operations_research {
24namespace sat {
25
27 bool sum = false;
28 int unassigned_index = -1;
29 for (int i = 0; i < literals_.size(); ++i) {
30 const Literal l = literals_[i];
31 if (trail_->Assignment().LiteralIsFalse(l)) {
32 sum ^= false;
33 } else if (trail_->Assignment().LiteralIsTrue(l)) {
34 sum ^= true;
35 } else {
36 // If we have more than one unassigned literal, we can't deduce anything.
37 if (unassigned_index != -1) return true;
38 unassigned_index = i;
39 }
40 }
41
42 // Propagates?
43 if (unassigned_index != -1) {
44 literal_reason_.clear();
45 for (int i = 0; i < literals_.size(); ++i) {
46 if (i == unassigned_index) continue;
47 const Literal l = literals_[i];
48 literal_reason_.push_back(
49 trail_->Assignment().LiteralIsFalse(l) ? l : l.Negated());
50 }
51 const Literal u = literals_[unassigned_index];
52 integer_trail_->EnqueueLiteral(sum == value_ ? u.Negated() : u,
53 literal_reason_, {});
54 return true;
55 }
56
57 // Ok.
58 if (sum == value_) return true;
59
60 // Conflict.
61 std::vector<Literal>* conflict = trail_->MutableConflict();
62 conflict->clear();
63 for (int i = 0; i < literals_.size(); ++i) {
64 const Literal l = literals_[i];
65 conflict->push_back(trail_->Assignment().LiteralIsFalse(l) ? l
66 : l.Negated());
67 }
68 return false;
69}
70
72 const int id = watcher->Register(this);
73 for (const Literal& l : literals_) {
74 watcher->WatchLiteral(l, id);
75 watcher->WatchLiteral(l.Negated(), id);
76 }
77}
78
80 IntegerVariable target_var, const absl::Span<const IntegerVariable> vars,
81 const absl::Span<const IntegerValue> offsets,
82 const absl::Span<const Literal> selectors,
83 const absl::Span<const Literal> enforcements, Model* model)
84 : target_var_(target_var),
85 vars_(vars.begin(), vars.end()),
86 offsets_(offsets.begin(), offsets.end()),
87 selectors_(selectors.begin(), selectors.end()),
88 enforcements_(enforcements.begin(), enforcements.end()),
89 trail_(model->GetOrCreate<Trail>()),
90 integer_trail_(model->GetOrCreate<IntegerTrail>()) {}
91
93 // TODO(user): In case of a conflict, we could push one of them to false if
94 // it is the only one.
95 for (const Literal l : enforcements_) {
96 if (!trail_->Assignment().LiteralIsTrue(l)) return true;
97 }
98
99 // Compute the min of the lower-bound for the still possible variables.
100 // TODO(user): This could be optimized by keeping more info from the last
101 // Propagate() calls.
102 IntegerValue target_min = kMaxIntegerValue;
103 const IntegerValue current_min = integer_trail_->LowerBound(target_var_);
104 for (int i = 0; i < vars_.size(); ++i) {
105 if (trail_->Assignment().LiteralIsTrue(selectors_[i])) return true;
106 if (trail_->Assignment().LiteralIsFalse(selectors_[i])) continue;
107 target_min = std::min(target_min,
108 integer_trail_->LowerBound(vars_[i]) + offsets_[i]);
109
110 // Abort if we can't get a better bound.
111 if (target_min <= current_min) return true;
112 }
113 if (target_min == kMaxIntegerValue) {
114 // All false, conflit.
115 *(trail_->MutableConflict()) = selectors_;
116 return false;
117 }
118
119 literal_reason_.clear();
120 integer_reason_.clear();
121 for (const Literal l : enforcements_) {
122 literal_reason_.push_back(l.Negated());
123 }
124 for (int i = 0; i < vars_.size(); ++i) {
125 if (trail_->Assignment().LiteralIsFalse(selectors_[i])) {
126 literal_reason_.push_back(selectors_[i]);
127 } else {
128 integer_reason_.push_back(
129 IntegerLiteral::GreaterOrEqual(vars_[i], target_min - offsets_[i]));
130 }
131 }
132 return integer_trail_->Enqueue(
133 IntegerLiteral::GreaterOrEqual(target_var_, target_min), literal_reason_,
134 integer_reason_);
135}
136
138 GenericLiteralWatcher* watcher) {
139 const int id = watcher->Register(this);
140 for (const Literal l : selectors_) watcher->WatchLiteral(l.Negated(), id);
141 for (const Literal l : enforcements_) watcher->WatchLiteral(l, id);
142 for (const IntegerVariable v : vars_) watcher->WatchLowerBound(v, id);
143}
144
145} // namespace sat
146} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
const std::vector< IntVar * > vars_
Definition: alldiff_cst.cc:43
void RegisterWith(GenericLiteralWatcher *watcher)
void WatchLiteral(Literal l, int id, int watch_index=-1)
Definition: integer.h:1365
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
Definition: integer.h:1373
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1939
GreaterThanAtLeastOneOfPropagator(IntegerVariable target_var, const absl::Span< const IntegerVariable > vars, const absl::Span< const IntegerValue > offsets, const absl::Span< const Literal > selectors, const absl::Span< const Literal > enforcements, Model *model)
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:989
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:1087
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
GRBmodel * model
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
IntervalVar *const target_var_
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264