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

improve fz to sat encoding

Browse Source
This commit is contained in:
Laurent Perron
2019-09-11 12:49:59 +02:00
parent 9fba0771cc
commit e5d010490e
1 changed files with 36 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

41
ortools/flatzinc/cp_model_fz_solver.cc
View File

@@ -24,11 +24,13 @@
#include "absl/strings/str_split.h"
#include "absl/synchronization/mutex.h"
#include "google/protobuf/text_format.h"
#include "ortools/base/iterator_adaptors.h"
#include "ortools/base/map_util.h"
#include "ortools/base/threadpool.h"
#include "ortools/base/timer.h"
#include "ortools/flatzinc/checker.h"
#include "ortools/flatzinc/logging.h"
#include "ortools/flatzinc/model.h"
#include "ortools/sat/cp_constraints.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_search.h"
@@ -193,11 +195,40 @@ void CpModelProtoWithMapping::FillAMinusBInDomain(
const std::vector<int64>& domain, const fz::Constraint& fz_ct,
ConstraintProto* ct) {
auto* arg = ct->mutable_linear();
for (const int64 domain_bound : domain) arg->add_domain(domain_bound);
arg->add_vars(LookupVar(fz_ct.arguments[0]));
arg->add_coeffs(1);
arg->add_vars(LookupVar(fz_ct.arguments[1]));
arg->add_coeffs(-1);
if (fz_ct.arguments[1].type == fz::Argument::INT_VALUE) {
const int64 value = fz_ct.arguments[1].Value();
const int var_a = LookupVar(fz_ct.arguments[0]);
for (const int64 domain_bound : domain) {
if (domain_bound == kint64min || domain_bound == kint64max) {
arg->add_domain(domain_bound);
} else {
arg->add_domain(domain_bound + value);
}
}
arg->add_vars(var_a);
arg->add_coeffs(1);
} else if (fz_ct.arguments[0].type == fz::Argument::INT_VALUE) {
const int64 value = fz_ct.arguments[0].Value();
const int var_b = LookupVar(fz_ct.arguments[1]);
for (int64 domain_bound : gtl::reversed_view(domain)) {
if (domain_bound == kint64min) {
arg->add_domain(kint64max);
} else if (domain_bound == kint64max) {
arg->add_domain(kint64min);
} else {
arg->add_domain(value - domain_bound);
}
}
arg->add_vars(var_b);
arg->add_coeffs(1);
} else {
for (const int64 domain_bound : domain) arg->add_domain(domain_bound);
arg->add_vars(LookupVar(fz_ct.arguments[0]));
arg->add_coeffs(1);
arg->add_vars(LookupVar(fz_ct.arguments[1]));
arg->add_coeffs(-1);
}
}
void CpModelProtoWithMapping::FillLinearConstraintWithGivenDomain(