sync with internal code; mostly reindent; implemented very naive circuit constraint. It is actually slower than the expanded version in minizinc; hook up the circuit constraint everywhere (io, flatzinc...)

This commit is contained in:
lperron@google.com
2013-07-24 00:28:11 +00:00
parent 37096cf41e
commit bc302f16c4
11 changed files with 382 additions and 481 deletions

View File

@@ -786,7 +786,7 @@ Constraint* Solver::MakeAllDifferentExcept(const std::vector<IntVar*>& vars,
escape_candidates += (vars[i]->Contains(escape_value));
}
if (escape_candidates <= 1) {
return MakeAllDifferent(vars, true);
return MakeAllDifferent(vars);
} else {
return RevAlloc(new AllDifferentExcept(this, vars, escape_value));
}

View File

@@ -2660,6 +2660,7 @@ const char ModelVisitor::kAbsEqual[] = "AbsEqual";
const char ModelVisitor::kAllDifferent[] = "AllDifferent";
const char ModelVisitor::kAllowedAssignments[] = "AllowedAssignments";
const char ModelVisitor::kBetween[] = "Between";
const char ModelVisitor::kCircuit[] = "Circuit";
const char ModelVisitor::kConvexPiecewise[] = "ConvexPiecewise";
const char ModelVisitor::kCountEqual[] = "CountEqual";
const char ModelVisitor::kCover[] = "Cover";

View File

@@ -1668,6 +1668,9 @@ class Solver {
ResultCallback1<bool, int64>* sink_handler,
bool assume_paths);
// Force the nexts() variable to create an complete hamiltonian path.
Constraint* MakeCircuit(const std::vector<IntVar*>& nexts);
// Creates a constraint which accumulates values along a path such that:
// cumuls[next[i]] = cumuls[i] + transits[i].
// Active variables indicate if the corresponding next variable is active;
@@ -3332,6 +3335,7 @@ class ModelVisitor : public BaseObject {
static const char kAllowedAssignments[];
static const char kIndexOf[];
static const char kBetween[];
static const char kCircuit[];
static const char kConvexPiecewise[];
static const char kCountEqual[];
static const char kCover[];

View File

@@ -22,6 +22,7 @@
#include "base/scoped_ptr.h"
#include "constraint_solver/constraint_solver.h"
#include "constraint_solver/constraint_solveri.h"
#include "util/string_array.h"
namespace operations_research {
@@ -531,6 +532,80 @@ string NoCycle::DebugString() const {
return out;
}
// ----- Circuit constraint -----
class Circuit : public Constraint {
public:
Circuit(Solver* const s, const std::vector<IntVar*>& nexts)
: Constraint(s), nexts_(nexts), size_(nexts_.size()), processed_(0) {}
virtual ~Circuit() {}
virtual void Post() {
for (int i = 0; i < size_; ++i) {
Demon* const d = MakeDelayedConstraintDemon0(
solver(), this, &Circuit::CheckSupports, "CheckSupports");
nexts_[i]->WhenDomain(d);
}
solver()->AddConstraint(solver()->MakeAllDifferent(nexts_));
}
virtual void InitialPropagate() {
for (int i = 0; i < size_; ++i) {
nexts_[i]->SetRange(0, size_ - 1);
nexts_[i]->RemoveValue(i);
}
CheckSupports();
}
virtual string DebugString() const {
return StringPrintf("Circuit(%s)", DebugStringVector(nexts_, " ").c_str());
}
void Accept(ModelVisitor* const visitor) const {
visitor->BeginVisitConstraint(ModelVisitor::kCircuit, this);
visitor->VisitIntegerVariableArrayArgument(
ModelVisitor::kNextsArgument, nexts_);
visitor->EndVisitConstraint(ModelVisitor::kCircuit, this);
}
private:
// Can we build a spanning tree routed on 0. If no, we have cycles.
void CheckSupports() {
insertion_queue_.clear();
insertion_queue_.push_back(0);
processed_ = 0;
to_visit_.clear();
for (int i = 1; i < size_; ++i) {
to_visit_.push_back(i);
}
while (processed_ < insertion_queue_.size() &&
insertion_queue_.size() < size_) {
const int inserted = insertion_queue_[processed_++];
std::vector<int> rejected;
for (int index = 0; index < to_visit_.size(); ++index) {
const int candidate = to_visit_[index];
if (nexts_[candidate]->Contains(inserted)) {
insertion_queue_.push_back(candidate);
} else {
rejected.push_back(candidate);
}
}
to_visit_.clear();
to_visit_.swap(rejected);
}
if (insertion_queue_.size() < size_) {
solver()->Fail();
}
}
std::vector<IntVar*> nexts_;
const int size_;
std::vector<int> insertion_queue_;
std::vector<int> to_visit_;
int processed_;
};
bool GreaterThan(int64 x, int64 y) {
return y >= x;
}
@@ -560,6 +635,10 @@ Constraint* Solver::MakeNoCycle(const std::vector<IntVar*>& nexts,
return MakeNoCycle(nexts, active, sink_handler, true);
}
Constraint* Solver::MakeCircuit(const std::vector<IntVar*>& nexts) {
return RevAlloc(new Circuit(this, nexts));
}
// ----- Path cumul constraints -----
namespace {

File diff suppressed because it is too large Load Diff

View File

@@ -588,7 +588,10 @@ class IsGreaterEqualCstCt : public CastConstraint {
expr_->SetMin(cst_);
}
}
if (inhibit && expr_->IsVar()) {
if (inhibit && ((target_var_->Max() == 0 && expr_->Max() < cst_) ||
(target_var_->Min() == 1 && expr_->Min() >= cst_))) {
// Can we safely inhibit? Sometimes an expression is not
// persistent, just monotonic.
demon_->inhibit(solver());
}
}
@@ -691,7 +694,10 @@ class IsLessEqualCstCt : public CastConstraint {
expr_->SetMax(cst_);
}
}
if (inhibit && expr_->IsVar()) {
if (inhibit && ((target_var_->Max() == 0 && expr_->Min() > cst_) ||
(target_var_->Min() == 1 && expr_->Max() <= cst_))) {
// Can we safely inhibit? Sometimes an expression is not
// persistent, just monotonic.
demon_->inhibit(solver());
}
}
@@ -1028,8 +1034,9 @@ class IsMemberCt : public Constraint {
if (var_->Bound()) {
demon_->inhibit(solver());
boolvar_->SetValue(1);
return;
}
//We have found a positive support. Let's check the
// We have found a positive support. Let's check the
// negative support.
if (var_->Contains(neg_support_)) {
return;

View File

@@ -1072,6 +1072,15 @@ Constraint* BuildBetween(CPModelLoader* const builder,
return builder->solver()->MakeBetweenCt(expr->Var(), value_min, value_max);
}
// ----- kCircuit -----
Constraint* BuildCircuit(CPModelLoader* const builder,
const CPConstraintProto& proto) {
std::vector<IntVar*> vars;
VERIFY(builder->ScanArguments(ModelVisitor::kNextsArgument, proto, &vars));
return builder->solver()->MakeCircuit(vars);
}
// ----- kConvexPiecewise -----
IntExpr* BuildConvexPiecewise(CPModelLoader* const builder,
const CPIntegerExpressionProto& proto) {
@@ -2647,6 +2656,7 @@ void Solver::InitBuilders() {
REGISTER(kAllDifferent, BuildAllDifferent);
REGISTER(kAllowedAssignments, BuildAllowedAssignments);
REGISTER(kBetween, BuildBetween);
REGISTER(kCircuit, BuildCircuit);
REGISTER(kConvexPiecewise, BuildConvexPiecewise);
REGISTER(kCountEqual, BuildCountEqual);
REGISTER(kCover, BuildCover);

View File

@@ -1719,7 +1719,6 @@ class CumulativeTimeTable : public Constraint {
DCHECK_EQ(0, usage);
profile_unique_time_.push_back(ProfileDelta(kint64max, 0));
}
// Update the start min for all tasks. Runs in O(n^2) and Omega(n).
void PushTasks() {
Sort(&by_start_min_, TaskStartMinLessThan);

View File

@@ -210,7 +210,6 @@ FlatZincModel::~FlatZincModel(void) {
void FlatZincModel::InitOutput(AstArray* const output) { output_ = output; }
void FlatZincModel::CollectOutputVariables(AstNode* const node) {
int k;
if (node->isArray()) {
AstArray* element = node->getArray();
int size = element->a.size();

View File

@@ -0,0 +1,12 @@
%-----------------------------------------------------------------------------%
% Constrains the elements of 'x' to define a circuit where 'x[i] = j' means
% that 'j' is the successor of 'i'.
%-----------------------------------------------------------------------------%
predicate circuit(array[int] of var int: x);
predicate circuit_reif(array[int] of var int: x, var bool: b) =
abort("Reified circuit/1 is not supported.");
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

View File

@@ -2207,7 +2207,6 @@ void p_alldifferent_except_0(FlatZincModel* const model, CtSpec* const spec) {
AstArray* const array_variables = spec->Arg(0)->getArray();
const int size = array_variables->a.size();
std::vector<IntVar*> variables;
int non_zero = 0;
for (int i = 0; i < size; ++i) {
IntVar* const var = model->GetIntExpr(array_variables->a[i])->Var();
if (!var->Bound() || var->Min() != 0) {
@@ -2905,6 +2904,20 @@ void p_nvalue(FlatZincModel* const model, CtSpec* const spec) {
}
}
void p_circuit(FlatZincModel* const model, CtSpec* const spec) {
Solver* const solver = model->solver();
AstArray* const array_variables = spec->Arg(0)->getArray();
const int size = array_variables->a.size();
std::vector<IntVar*> variables(size);
for (int i = 0; i < size; ++i) {
variables[i] =
solver->MakeSum(model->GetIntExpr(array_variables->a[i]), -1)->Var();
}
Constraint* const ct = solver->MakeCircuit(variables);
VLOG(2) << " - posted " << ct->DebugString();
model->AddConstraint(spec, ct);
}
class IntBuilder {
public:
IntBuilder(void) {
@@ -3007,6 +3020,7 @@ class IntBuilder {
global_model_builder.Register("lex_lesseq_bool", &p_lex_less_int);
global_model_builder.Register("inverse", &p_inverse);
global_model_builder.Register("nvalue", &p_nvalue);
global_model_builder.Register("circuit", &p_circuit);
}
};
IntBuilder __int_Builder;