always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

renamed sat code

Browse Source
This commit is contained in:
Laurent Perron
2016-09-12 13:51:04 +02:00
parent cb98b1fa71
commit 293d224c9f
4 changed files with 475 additions and 154 deletions
Download Patch File Download Diff File Expand all files Collapse all files

247
src/sat/integer_expr.cc Normal file
View File

@@ -0,0 +1,247 @@
// Copyright 2010-2014 Google
// 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 "sat/integer_expr.h"
namespace operations_research {
namespace sat {
IntegerSum::IntegerSum(const std::vector<IntegerVariable>& vars,
const std::vector<int>& coeffs, IntegerVariable sum,
IntegerTrail* integer_trail)
: vars_(vars), coeffs_(coeffs), sum_(sum), integer_trail_(integer_trail) {
// Handle negative coefficients.
for (int i = 0; i < vars.size(); ++i) {
if (coeffs_[i] < 0) {
vars_[i] = NegationOf(vars_[i]);
coeffs_[i] = -coeffs_[i];
}
}
}
bool IntegerSum::Propagate(Trail* trail) {
if (vars_.empty()) return true;
IntegerValue new_lb = integer_trail_->LowerBound(vars_[0]) * coeffs_[0];
for (int i = 1; i < vars_.size(); ++i) {
new_lb += integer_trail_->LowerBound(vars_[i]) * coeffs_[i];
}
// Update the sum lower-bound.
if (new_lb > integer_trail_->LowerBound(sum_)) {
integer_reason_.clear();
for (const IntegerVariable& var : vars_) {
integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(var));
}
if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(sum_, new_lb),
literal_reason_, integer_reason_)) {
return false;
}
}
// Update the variables upper-bound.
const IntegerValue sum_upper_bound = integer_trail_->UpperBound(sum_);
for (int i = 0; i < vars_.size(); ++i) {
const IntegerValue new_term_ub =
sum_upper_bound - new_lb +
integer_trail_->LowerBound(vars_[i]) * coeffs_[i];
const IntegerValue new_ub = new_term_ub / coeffs_[i];
if (new_ub < integer_trail_->UpperBound(vars_[i])) {
integer_reason_.clear();
for (int j = 0; j < vars_.size(); ++j) {
if (i == j) continue;
integer_reason_.push_back(
integer_trail_->LowerBoundAsLiteral(vars_[j]));
}
integer_reason_.push_back(integer_trail_->UpperBoundAsLiteral(sum_));
if (!integer_trail_->Enqueue(
IntegerLiteral::LowerOrEqual(vars_[i], new_ub), literal_reason_,
integer_reason_)) {
return false;
}
}
}
return true;
}
void IntegerSum::RegisterWith(GenericLiteralWatcher* watcher) {
const int id = watcher->Register(this);
for (const IntegerVariable& var : vars_) {
watcher->WatchIntegerVariable(var, id);
}
watcher->WatchIntegerVariable(sum_, id);
}
MinPropagator::MinPropagator(const std::vector<IntegerVariable>& vars,
IntegerVariable min_var,
IntegerTrail* integer_trail)
: vars_(vars), min_var_(min_var), integer_trail_(integer_trail) {}
bool MinPropagator::Propagate(Trail* trail) {
if (vars_.empty()) return true;
// Count the number of interval that are possible candidate for the min.
// Only the intervals for which lb > current_min_ub cannot.
const IntegerLiteral min_ub_literal =
integer_trail_->UpperBoundAsLiteral(min_var_);
const IntegerValue current_min_ub = integer_trail_->UpperBound(min_var_);
int num_intervals_that_can_be_min = 0;
int last_possible_min_interval = 0;
IntegerValue min = kMaxIntegerValue;
for (int i = 0; i < vars_.size(); ++i) {
const IntegerValue lb = integer_trail_->LowerBound(vars_[i]);
min = std::min(min, lb);
if (lb <= current_min_ub) {
++num_intervals_that_can_be_min;
last_possible_min_interval = i;
}
}
// Propagation a)
if (min > integer_trail_->LowerBound(min_var_)) {
literal_reason_.clear();
integer_reason_.clear();
for (const IntegerVariable var : vars_) {
integer_reason_.push_back(IntegerLiteral::GreaterOrEqual(var, min));
}
if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(min_var_, min),
literal_reason_, integer_reason_)) {
return false;
}
}
// Propagation b)
if (num_intervals_that_can_be_min == 1) {
const IntegerValue ub_of_only_candidate =
integer_trail_->UpperBound(vars_[last_possible_min_interval]);
if (current_min_ub < ub_of_only_candidate) {
literal_reason_.clear();
integer_reason_.clear();
// The reason is that all the other interval start after current_min_ub.
// And that min_ub has its current value.
integer_reason_.push_back(min_ub_literal);
for (const IntegerVariable var : vars_) {
if (var == vars_[last_possible_min_interval]) continue;
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(var, current_min_ub + 1));
}
if (!integer_trail_->Enqueue(
IntegerLiteral::LowerOrEqual(vars_[last_possible_min_interval],
current_min_ub),
literal_reason_, integer_reason_)) {
return false;
}
}
}
// Conflict.
//
// TODO(user): Not sure this code is useful since this will be detected
// by the fact that the [lb, ub] of the min is empty. It depends on the
// propagation order though, but probably the precedences propagator would
// propagate before this one. So change this to a CHECK?
if (num_intervals_that_can_be_min == 0) {
integer_reason_.clear();
// Almost the same as propagation b).
integer_reason_.push_back(min_ub_literal);
for (const IntegerVariable var : vars_) {
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(var, current_min_ub + 1));
}
std::vector<Literal>* conflict = trail->MutableConflict();
integer_trail_->MergeReasonInto(integer_reason_, conflict);
return false;
}
return true;
}
void MinPropagator::RegisterWith(GenericLiteralWatcher* watcher) {
const int id = watcher->Register(this);
for (const IntegerVariable& var : vars_) {
watcher->WatchLowerBound(var, id);
}
watcher->WatchUpperBound(min_var_, id);
}
IsOneOfPropagator::IsOneOfPropagator(IntegerVariable var,
const std::vector<Literal>& selectors,
const std::vector<IntegerValue>& values,
IntegerTrail* integer_trail)
: var_(var),
selectors_(selectors),
values_(values),
integer_trail_(integer_trail) {}
bool IsOneOfPropagator::Propagate(Trail* trail) {
const IntegerValue current_min = integer_trail_->LowerBound(var_);
const IntegerValue current_max = integer_trail_->UpperBound(var_);
IntegerValue min = kMaxIntegerValue;
IntegerValue max = kMinIntegerValue;
literal_reason_.clear();
for (int i = 0; i < selectors_.size(); ++i) {
if (trail->Assignment().LiteralIsFalse(selectors_[i])) {
literal_reason_.push_back(selectors_[i]);
} else {
min = std::min(min, values_[i]);
max = std::max(max, values_[i]);
if (!trail->Assignment().LiteralIsTrue(selectors_[i])) {
// Propagate selector to false?
std::vector<Literal>* literal_reason;
std::vector<IntegerLiteral>* integer_reason;
if (current_min > values_[i]) {
integer_trail_->EnqueueLiteral(
selectors_[i].Negated(), &literal_reason, &integer_reason, trail);
integer_reason->push_back(integer_trail_->LowerBoundAsLiteral(var_));
} else if (current_max < values_[i]) {
integer_trail_->EnqueueLiteral(
selectors_[i].Negated(), &literal_reason, &integer_reason, trail);
integer_reason->push_back(integer_trail_->UpperBoundAsLiteral(var_));
}
}
}
}
// Propagate new min/max.
if (min > current_min) {
if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(var_, min),
literal_reason_, integer_reason_)) {
return false;
}
}
if (max < current_max) {
if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(var_, max),
literal_reason_, integer_reason_)) {
return false;
}
}
return true;
}
void IsOneOfPropagator::RegisterWith(GenericLiteralWatcher* watcher) {
const int id = watcher->Register(this);
for (const Literal& lit : selectors_) {
watcher->WatchLiteral(lit.Negated(), id);
}
watcher->WatchIntegerVariable(var_, id);
}
} // namespace sat
} // namespace operations_research

228
src/sat/integer_expr.h Normal file
View File

@@ -0,0 +1,228 @@
// Copyright 2010-2014 Google
// 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.
#ifndef OR_TOOLS_SAT_INTEGER_EXPR_H_
#define OR_TOOLS_SAT_INTEGER_EXPR_H_
#include "sat/integer.h"
#include "sat/model.h"
#include "sat/precedences.h"
#include "sat/sat_base.h"
namespace operations_research {
namespace sat {
// A really basic implementation of a sum of integer variables.
// The complexity is in O(num_variables) at each propagation.
//
// TODO(user): Propagate all the bounds.
// TODO(user): If one has many such constraint, it will be more efficient to
// propagate all of them at once rather than doing it one at the time.
class IntegerSum : public PropagatorInterface {
public:
IntegerSum(const std::vector<IntegerVariable>& vars,
const std::vector<int>& coefficients, IntegerVariable sum,
IntegerTrail* integer_trail);
// Currently we only propagates the directions:
// * vars lower-bound -> sum lower-bound.
// * for all vars i,
// vars lower-bound (excluding i) + sum upper_bound -> i upper-bound.
bool Propagate(Trail* trail) final;
void RegisterWith(GenericLiteralWatcher* watcher);
private:
std::vector<IntegerVariable> vars_;
std::vector<int> coeffs_;
IntegerVariable sum_;
IntegerTrail* integer_trail_;
std::vector<Literal> literal_reason_;
std::vector<IntegerLiteral> integer_reason_;
DISALLOW_COPY_AND_ASSIGN(IntegerSum);
};
// A min (resp max) contraint of the form min == MIN(vars) can be decomposed
// into two inequalities:
// 1/ min <= MIN(vars), which is the same as for all v in vars, "min <= v".
// This can be taken care of by the LowerOrEqual(min, v) constraint.
// 2/ min >= MIN(vars).
//
// And in turn, 2/ can be decomposed in:
// a) lb(min) >= lb(MIN(vars)) = MIN(lb(var));
// b) ub(min) >= ub(MIN(vars)) and we can't propagate anything here unless
// there is just one possible variable 'v' that can be the min:
// for all u != v, lb(u) > ub(min);
// In this case, ub(min) >= ub(v).
//
// This constraint take care of a) and b). That is:
// - If the min of the lower bound of the vars increase, then the lower bound of
// the min_var will be >= to it.
// - If there is only one candidate for the min, then if the ub(min) decrease,
// the ub of the only candidate will be <= to it.
//
// Complexity: This is a basic implementation in O(num_vars) on each call to
// Propagate(), which will happen each time one or more variables in vars_
// changed.
//
// TODO(user): Implement a more efficient algorithm when the need arise.
class MinPropagator : public PropagatorInterface {
public:
MinPropagator(const std::vector<IntegerVariable>& vars, IntegerVariable min_var,
IntegerTrail* integer_trail);
bool Propagate(Trail* trail) final;
void RegisterWith(GenericLiteralWatcher* watcher);
private:
const std::vector<IntegerVariable> vars_;
const IntegerVariable min_var_;
IntegerTrail* integer_trail_;
std::vector<Literal> literal_reason_;
std::vector<IntegerLiteral> integer_reason_;
DISALLOW_COPY_AND_ASSIGN(MinPropagator);
};
// Propagate the fact that a given integer variable is equal to exactly one
// element out of a given set of values. Each value is selected or not by a
// literal being true.
//
// Note that the fact that exactly one "selector" should be true is not enforced
// here. This class just propagate the directions:
// - selector is false => potentially restrict the [lb, ub] of var.
// - [lb, ub] change => more selector can be set to false.
class IsOneOfPropagator : public PropagatorInterface {
public:
IsOneOfPropagator(IntegerVariable var, const std::vector<Literal>& selectors,
const std::vector<IntegerValue>& values,
IntegerTrail* integer_trail);
bool Propagate(Trail* trail) final;
void RegisterWith(GenericLiteralWatcher* watcher);
private:
const IntegerVariable var_;
const std::vector<Literal> selectors_;
const std::vector<IntegerValue> values_;
IntegerTrail* integer_trail_;
std::vector<Literal> literal_reason_;
std::vector<IntegerLiteral> integer_reason_;
DISALLOW_COPY_AND_ASSIGN(IsOneOfPropagator);
};
// =============================================================================
// Model based functions.
// =============================================================================
// Model-based function to create an IntegerVariable that corresponds to the
// given weighted sum of other IntegerVariables.
inline std::function<IntegerVariable(Model*)> NewWeightedSum(
const std::vector<int>& coefficients, const std::vector<IntegerVariable>& vars) {
return [=](Model* model) {
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
// The trival bounds will be propagated correctly at level zero.
IntegerVariable sum = integer_trail->AddIntegerVariable();
IntegerSum* constraint =
new IntegerSum(vars, coefficients, sum, integer_trail);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
return sum;
};
}
// Expresses the fact that an existing integer variable is equal to the minimum
// of other integer variables.
inline std::function<void(Model*)> IsEqualToMinOf(
IntegerVariable min_var, const std::vector<IntegerVariable>& vars) {
return [=](Model* model) {
for (const IntegerVariable& var : vars) {
model->Add(LowerOrEqual(min_var, var));
}
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
MinPropagator* constraint = new MinPropagator(vars, min_var, integer_trail);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
};
}
// Expresses the fact that an existing integer variable is equal to the maximum
// of other integer variables.
inline std::function<void(Model*)> IsEqualToMaxOf(
IntegerVariable max_var, const std::vector<IntegerVariable>& vars) {
return [=](Model* model) {
std::vector<IntegerVariable> negated_vars;
for (const IntegerVariable& var : vars) {
negated_vars.push_back(NegationOf(var));
model->Add(GreaterOrEqual(max_var, var));
}
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
MinPropagator* constraint =
new MinPropagator(negated_vars, NegationOf(max_var), integer_trail);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
};
}
// Creates an integer variable equal to the minimum of other integer variables.
inline std::function<IntegerVariable(Model*)> NewMin(
const std::vector<IntegerVariable>& vars) {
return [=](Model* model) {
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
// The trival bounds will be propagated correctly at level zero.
IntegerVariable min_var = integer_trail->AddIntegerVariable();
model->Add(IsEqualToMinOf(min_var, vars));
return min_var;
};
}
// Creates an IntegerVariable equal to the maximum of a set of IntegerVariables.
inline std::function<IntegerVariable(Model*)> NewMax(
const std::vector<IntegerVariable>& vars) {
return [=](Model* model) {
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
// The trival bounds will be propagated correctly at level zero.
IntegerVariable max_var = integer_trail->AddIntegerVariable();
model->Add(IsEqualToMaxOf(max_var, vars));
return max_var;
};
}
// Expresses the fact that an existing integer variable is equal to one of
// the given values, each selected by a given literal.
inline std::function<void(Model*)> IsOneOf(IntegerVariable var,
const std::vector<Literal>& selectors,
const std::vector<IntegerValue>& values) {
return [=](Model* model) {
// TODO(user): Add the exactly one constaint here?
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
IsOneOfPropagator* constraint =
new IsOneOfPropagator(var, selectors, values, integer_trail);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
};
}
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_INTEGER_EXPR_H_

75
src/sat/integer_sum.cc
View File

@@ -1,75 +0,0 @@
// Copyright 2010-2014 Google
// 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 "sat/integer_sum.h"
namespace operations_research {
namespace sat {
IntegerSum::IntegerSum(const std::vector<IntegerVariable>& vars,
const std::vector<int>& coeffs, IntegerVariable sum,
IntegerTrail* integer_trail)
: vars_(vars), coeffs_(coeffs), sum_(sum), integer_trail_(integer_trail) {}
bool IntegerSum::Propagate(Trail* trail) {
if (vars_.empty()) return true;
int new_lb = integer_trail_->LowerBound(vars_[0]) * coeffs_[0];
for (int i = 1; i < vars_.size(); ++i) {
new_lb += integer_trail_->LowerBound(vars_[i]) * coeffs_[i];
}
// Update the sum lower-bound.
if (new_lb > integer_trail_->LowerBound(sum_)) {
integer_reason_.clear();
for (const IntegerVariable& var : vars_) {
integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(var));
}
integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(sum_, new_lb),
literal_reason_, integer_reason_);
if (integer_trail_->DomainIsEmpty(sum_, trail)) return false;
}
// Update the variables upper-bound.
const int sum_upper_bound = integer_trail_->UpperBound(sum_);
for (int i = 0; i < vars_.size(); ++i) {
const int new_term_ub = sum_upper_bound - new_lb +
integer_trail_->LowerBound(vars_[i]) * coeffs_[i];
const int new_ub = new_term_ub / coeffs_[i];
if (new_ub < integer_trail_->UpperBound(vars_[i])) {
integer_reason_.clear();
for (int j = 0; j < vars_.size(); ++j) {
if (i == j) continue;
integer_reason_.push_back(
integer_trail_->LowerBoundAsLiteral(vars_[j]));
}
integer_reason_.push_back(integer_trail_->UpperBoundAsLiteral(sum_));
integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(vars_[i], new_ub),
literal_reason_, integer_reason_);
if (integer_trail_->DomainIsEmpty(vars_[i], trail)) return false;
}
}
return true;
}
void IntegerSum::RegisterWith(GenericLiteralWatcher* watcher) {
const int id = watcher->Register(this);
for (const IntegerVariable& var : vars_) {
watcher->WatchIntegerVariable(var, id);
}
watcher->WatchIntegerVariable(sum_, id);
}
} // namespace sat
} // namespace operations_research

79
src/sat/integer_sum.h
View File

@@ -1,79 +0,0 @@
// Copyright 2010-2014 Google
// 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.
#ifndef OR_TOOLS_SAT_INTEGER_SUM_H_
#define OR_TOOLS_SAT_INTEGER_SUM_H_
#include "sat/integer.h"
#include "sat/model.h"
#include "sat/sat_base.h"
namespace operations_research {
namespace sat {
// A really basic implementation of a sum of integer variables.
// The complexity is in O(num_variables) at each propagation.
//
// TODO(user): handle negative coefficients.
// TODO(user): Propagate all the bounds.
// TODO(user): If one has many such constraint, it will be more efficient to
// propagate all of them at once rather than doing it one at the time.
class IntegerSum : public PropagatorInterface {
public:
IntegerSum(const std::vector<IntegerVariable>& vars,
const std::vector<int>& coefficients, IntegerVariable sum,
IntegerTrail* integer_trail);
// Currently we only propagates the directions:
// * vars lower-bound -> sum lower-bound.
// * for all vars i,
// vars lower-bound (excluding i) + sum upper_bound -> i upper-bound.
bool Propagate(Trail* trail) final;
void RegisterWith(GenericLiteralWatcher* watcher);
private:
std::vector<IntegerVariable> vars_;
std::vector<int> coeffs_;
IntegerVariable sum_;
IntegerTrail* integer_trail_;
std::vector<Literal> literal_reason_;
std::vector<IntegerLiteral> integer_reason_;
DISALLOW_COPY_AND_ASSIGN(IntegerSum);
};
// Model-based function to create an IntegerVariable that corresponds to the
// given weighted sum of other IntegerVariables.
inline std::function<IntegerVariable(Model*)> NewWeightedSum(
const std::vector<int>& coefficients, const std::vector<IntegerVariable>& vars) {
return [=](Model* model) {
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
// The trival bounds will be propagated correctly at level zero.
// TODO(user): pay attention to integer overflow. It currently work but
// it is not really robust.
IntegerVariable sum = integer_trail->AddIntegerVariable(
std::numeric_limits<int>::min(), std::numeric_limits<int>::max());
IntegerSum* constraint =
new IntegerSum(vars, coefficients, sum, integer_trail);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
return sum;
};
}
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_INTEGER_SUM_H_