OR-Tools  8.1
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"
19 #include "ortools/base/map_util.h"
20 #include "ortools/sat/sat_solver.h"
21 #include "ortools/util/sort.h"
22 
23 namespace operations_research {
24 namespace 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
operations_research::sat::GreaterThanAtLeastOneOfPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: cp_constraints.cc:137
operations_research::sat::GenericLiteralWatcher::Register
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1910
min
int64 min
Definition: alldiff_cst.cc:138
map_util.h
operations_research::sat::IntegerTrail
Definition: integer.h:533
operations_research::sat::GenericLiteralWatcher::WatchLowerBound
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
Definition: integer.h:1356
operations_research::sat::BooleanXorPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: cp_constraints.cc:71
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
operations_research::sat::IntegerTrail::EnqueueLiteral
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:1058
operations_research::sat::VariablesAssignment::LiteralIsTrue
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
operations_research::sat::GreaterThanAtLeastOneOfPropagator::GreaterThanAtLeastOneOfPropagator
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)
Definition: cp_constraints.cc:79
operations_research::sat::IntegerLiteral::GreaterOrEqual
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1247
operations_research::sat::Literal::Negated
Literal Negated() const
Definition: sat_base.h:91
sat_solver.h
operations_research::sat::GenericLiteralWatcher
Definition: integer.h:1091
operations_research::sat::IntegerTrail::Enqueue
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
operations_research::sat::kMaxIntegerValue
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
operations_research::sat::Trail::Assignment
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
operations_research::sat::GreaterThanAtLeastOneOfPropagator::Propagate
bool Propagate() final
Definition: cp_constraints.cc:92
target_var_
IntervalVar *const target_var_
Definition: sched_constraints.cc:230
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
cp_constraints.h
operations_research::sat::Trail::MutableConflict
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::Literal
Definition: sat_base.h:64
sort.h
operations_research::sat::GenericLiteralWatcher::WatchLiteral
void WatchLiteral(Literal l, int id, int watch_index=-1)
Definition: integer.h:1348
vars_
const std::vector< IntVar * > vars_
Definition: alldiff_cst.cc:43
operations_research::sat::BooleanXorPropagator::Propagate
bool Propagate() final
Definition: cp_constraints.cc:26
operations_research::sat::IntegerTrail::LowerBound
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1283
operations_research::sat::VariablesAssignment::LiteralIsFalse
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
operations_research::sat::Trail
Definition: sat_base.h:233