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

change sat internal API; stop ignoring random seed in glop

Browse Source
This commit is contained in:
Laurent Perron
2018-05-16 13:43:29 +02:00
parent cb1fc93b94
commit 9402f58d1d
11 changed files with 131 additions and 86 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
examples/python/wedding_optimal_chart_sat.py
View File

@@ -71,7 +71,7 @@ class WeddingChartPrinter(cp_model.CpSolverSolutionCallback):
return self.__solution_count
def main():
def BuildData():
#
# Data
#
@@ -128,6 +128,11 @@ def main():
"DeAnn (G)",
"Lori (G)"
]
return num_tables, table_capacity, min_known_neighbors, C, names
def SolveWithDiscreteModel():
num_tables, table_capacity, min_known_neighbors, C, names = BuildData()
num_guests = len(C)
@@ -214,5 +219,9 @@ def main():
print(' - num solutions: %i' % solution_printer.NumSolutions())
def main():
SolveWithDiscreteModel()
if __name__ == '__main__':
main()

15
ortools/glop/lp_solver.cc
View File

@@ -179,6 +179,9 @@ ProblemStatus LPSolver::SolveWithTimeLimit(const LinearProgram& lp,
const bool postsolve_is_needed = preprocessor.Run(&current_linear_program_);
VLOG(1) << "Presolved problem: "
<< current_linear_program_.GetDimensionString();
// At this point, we need to initialize a ProblemSolution with the correct
// size and status.
ProblemSolution solution(current_linear_program_.num_constraints(),
@@ -193,7 +196,17 @@ ProblemStatus LPSolver::SolveWithTimeLimit(const LinearProgram& lp,
}
if (postsolve_is_needed) preprocessor.RecoverSolution(&solution);
return LoadAndVerifySolution(lp, solution);
const ProblemStatus status = LoadAndVerifySolution(lp, solution);
// LOG some statistics that can be parsed by our benchmark script.
VLOG(1) << "status: " << status;
VLOG(1) << "objective: " << GetObjectiveValue();
VLOG(1) << "iterations: " << GetNumberOfSimplexIterations();
VLOG(1) << "time: " << time_limit->GetElapsedTime();
VLOG(1) << "deterministic_time: "
<< time_limit->GetElapsedDeterministicTime();
return status;
}
void LPSolver::Clear() {

2
ortools/glop/revised_simplex.cc
View File

@@ -2830,7 +2830,7 @@ Fractional RevisedSimplex::ComputeInitialProblemObjectiveValue() const {
void RevisedSimplex::SetParameters(const GlopParameters& parameters) {
SCOPED_TIME_STAT(&function_stats_);
random_.seed(parameters_.random_seed());
random_.seed(parameters.random_seed());
initial_parameters_ = parameters;
parameters_ = parameters;
PropagateParameters();

22
ortools/glop/scip_to_glop.cpp
View File

@@ -7,12 +7,12 @@
// If SCIP is compiled with this .cpp, then it will use Glop as the underlying
// LP solver. This is done in the target scip:libscip_with_glop.
//
// TODO(fdid): currently a lot of functions are left unimplemented and result
// TODO(user): currently a lot of functions are left unimplemented and result
// in a LOG(FATAL) if they are called. It seems that SCIP never uses them when
// called through the MPSolver interface (on July 2013; based on solving a
// couple of MIP problems).
//
// TODO(fdid): The function comments come from the SCIP lpi.h file and are not
// TODO(user): The function comments come from the SCIP lpi.h file and are not
// compliant with the Google style guide. We could remove them since they are
// in the .h, but given the file size, they are quite helpful.
@@ -49,7 +49,7 @@ struct SCIP_LPi {
operations_research::glop::GlopParameters* parameters;
operations_research::StatsGroup* stats;
// TODO(fdid): Store the parameters not yet supported by this interface.
// TODO(user): Store the parameters not yet supported by this interface.
// In debug mode, SCIP check that set() and then get() work as expected, so
// we need to store them.
bool from_scratch;
@@ -173,7 +173,7 @@ SCIP_RETCODE SCIPlpiAddCols(
// NULL if nnonz == 0
) {
SCOPED_TIME_STAT(lpi->stats);
// TODO(fdid): propagate the names?
// TODO(user): propagate the names?
VLOG(1) << "calling SCIPlpiAddCols ncols=" << ncols << " nnonz=" << nnonz;
int nz = 0;
for (int i = 0; i < ncols; ++i) {
@@ -256,7 +256,7 @@ SCIP_RETCODE SCIPlpiAddRows(
// NULL if nnonz == 0
) {
SCOPED_TIME_STAT(lpi->stats);
// TODO(fdid): propagate the names?
// TODO(user): propagate the names?
VLOG(1) << "calling SCIPlpiAddRows nrows=" << nrows << " nnonz=" << nnonz;
int nz = 0;
for (int i = 0; i < nrows; ++i) {
@@ -700,7 +700,7 @@ SCIP_RETCODE SCIPlpiSolveBarrier(SCIP_LPI* lpi, // LP interface structure
SCIP_RETCODE SCIPlpiStartStrongbranch(SCIP_LPI* lpi) {
SCOPED_TIME_STAT(lpi->stats);
VLOG(1) << "calling SCIPlpiStartStrongbranch";
// TODO(fdid): Save state and do all the branching from there.
// TODO(user): Save state and do all the branching from there.
return SCIP_OKAY;
}
@@ -708,7 +708,7 @@ SCIP_RETCODE SCIPlpiStartStrongbranch(SCIP_LPI* lpi) {
SCIP_RETCODE SCIPlpiEndStrongbranch(SCIP_LPI* lpi) {
SCOPED_TIME_STAT(lpi->stats);
VLOG(1) << "calling SCIPlpiEndStrongbranch";
// TODO(fdid): Restore the saved state in SCIPlpiStartStrongbranch().
// TODO(user): Restore the saved state in SCIPlpiStartStrongbranch().
return SCIP_OKAY;
}
@@ -748,7 +748,7 @@ SCIP_RETCODE SCIPlpiStrongbranchFrac(
const Fractional ub = lpi->linear_program->variable_upper_bounds()[col];
// Configure solver.
// TODO(fdid): use the iteration limit once glop support incrementality.
// TODO(user): use the iteration limit once glop support incrementality.
int num_iterations = 0;
lpi->parameters->set_use_dual_simplex(true);
lpi->solver->SetParameters(*(lpi->parameters));
@@ -854,7 +854,7 @@ SCIP_RETCODE SCIPlpiStrongbranchesInt(
SCIP_Bool SCIPlpiWasSolved(SCIP_LPI* lpi) {
SCOPED_TIME_STAT(lpi->stats);
// TODO(fdid): track this to avoid uneeded resolving.
// TODO(user): track this to avoid uneeded resolving.
return !(lpi->lp_modified_since_last_solve);
}
@@ -934,7 +934,7 @@ SCIP_Bool SCIPlpiHasDualRay(SCIP_LPI* lpi) {
SCOPED_TIME_STAT(lpi->stats);
VLOG(1) << "calling SCIPlpiHasDualRay";
const ProblemStatus status = lpi->solver->GetProblemStatus();
// TODO(fdid): check the sign of SCIPlpiGetDualfarkas()
// TODO(user): check the sign of SCIPlpiGetDualfarkas()
return status == ProblemStatus::DUAL_UNBOUNDED;
}
@@ -1382,7 +1382,7 @@ SCIP_RETCODE SCIPlpiWriteState(SCIP_LPI* lpi, // LP interface structure
// SCIP_LPiNorms stores norm information so they are not recomputed from one
// state to the next.
//
// TODO(fdid): Implement this.
// TODO(user): Implement this.
struct SCIP_LPiNorms {};
// stores LPi pricing norms information

68
ortools/sat/cp_model_solver.cc
View File

@@ -1713,15 +1713,13 @@ void TryToLinearizeConstraint(
const CpModelProto& model_proto, const ConstraintProto& ct,
ModelWithMapping* m, int linearization_level,
std::vector<LinearConstraint>* linear_constraints) {
auto* encoder = m->GetOrCreate<IntegerEncoder>();
if (encoder == nullptr) return;
const double kInfinity = std::numeric_limits<double>::infinity();
if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr) {
if (linearization_level < 2) return;
if (HasEnforcementLiteral(ct)) return;
LinearConstraintBuilder lc(1.0, kInfinity);
LinearConstraintBuilder lc(m->model(), 1.0, kInfinity);
for (const int ref : ct.bool_or().literals()) {
CHECK(lc.AddLiteralTerm(m->Literal(ref), 1.0, *encoder));
CHECK(lc.AddLiteralTerm(m->Literal(ref), 1.0));
}
linear_constraints->push_back(lc.Build());
} else if (ct.constraint_case() ==
@@ -1731,9 +1729,9 @@ void TryToLinearizeConstraint(
const Literal e = m->Literal(ct.enforcement_literal(0));
for (const int ref : ct.bool_and().literals()) {
// We linearize (e implies literal) as (e - literals <= 0).
LinearConstraintBuilder lc(-kInfinity, 0.0);
CHECK(lc.AddLiteralTerm(e, 1.0, *encoder));
CHECK(lc.AddLiteralTerm(m->Literal(ref), -1.0, *encoder));
LinearConstraintBuilder lc(m->model(), -kInfinity, 0.0);
CHECK(lc.AddLiteralTerm(e, 1.0));
CHECK(lc.AddLiteralTerm(m->Literal(ref), -1.0));
linear_constraints->push_back(lc.Build());
}
} else if (ct.constraint_case() == ConstraintProto::ConstraintCase::kIntMax) {
@@ -1743,7 +1741,7 @@ void TryToLinearizeConstraint(
// This deal with the corner case X = max(X, Y, Z, ..) !
// Note that this can be presolved into X >= Y, X >= Z, ...
if (target == var) continue;
LinearConstraintBuilder lc(-kInfinity, 0.0);
LinearConstraintBuilder lc(m->model(), -kInfinity, 0.0);
lc.AddTerm(m->Integer(var), 1.0);
lc.AddTerm(m->Integer(target), -1.0);
linear_constraints->push_back(lc.Build());
@@ -1753,7 +1751,7 @@ void TryToLinearizeConstraint(
const int target = ct.int_min().target();
for (const int var : ct.int_min().vars()) {
if (target == var) continue;
LinearConstraintBuilder lc(-kInfinity, 0.0);
LinearConstraintBuilder lc(m->model(), -kInfinity, 0.0);
lc.AddTerm(m->Integer(target), 1.0);
lc.AddTerm(m->Integer(var), -1.0);
linear_constraints->push_back(lc.Build());
@@ -1769,7 +1767,8 @@ void TryToLinearizeConstraint(
if (min == kint64min && max == kint64max) return;
if (!HasEnforcementLiteral(ct)) {
LinearConstraintBuilder lc((min == kint64min) ? -kInfinity : min,
LinearConstraintBuilder lc(m->model(),
(min == kint64min) ? -kInfinity : min,
(max == kint64max) ? kInfinity : max);
for (int i = 0; i < ct.linear().vars_size(); i++) {
const int ref = ct.linear().vars(i);
@@ -1807,24 +1806,24 @@ void TryToLinearizeConstraint(
const int e = ct.enforcement_literal(0);
if (min != kint64min) {
// (e => terms >= min) <=> terms >= implied_lb + e * (min - implied_lb);
LinearConstraintBuilder lc(implied_lb, kInfinity);
LinearConstraintBuilder lc(m->model(), implied_lb, kInfinity);
for (int i = 0; i < ct.linear().vars_size(); i++) {
const int ref = ct.linear().vars(i);
const int64 coeff = ct.linear().coeffs(i);
lc.AddTerm(m->Integer(ref), coeff);
}
CHECK(lc.AddLiteralTerm(m->Literal(e), implied_lb - min, *encoder));
CHECK(lc.AddLiteralTerm(m->Literal(e), implied_lb - min));
linear_constraints->push_back(lc.Build());
}
if (max != kint64max) {
// (e => terms <= max) <=> terms <= implied_ub + e * (max - implied_ub)
LinearConstraintBuilder lc(-kInfinity, implied_ub);
LinearConstraintBuilder lc(m->model(), -kInfinity, implied_ub);
for (int i = 0; i < ct.linear().vars_size(); i++) {
const int ref = ct.linear().vars(i);
const int64 coeff = ct.linear().coeffs(i);
lc.AddTerm(m->Integer(ref), coeff);
}
CHECK(lc.AddLiteralTerm(m->Literal(e), implied_ub - max, *encoder));
CHECK(lc.AddLiteralTerm(m->Literal(e), implied_ub - max));
linear_constraints->push_back(lc.Build());
}
} else if (ct.constraint_case() ==
@@ -1841,10 +1840,11 @@ void TryToLinearizeConstraint(
std::map<int, std::unique_ptr<LinearConstraintBuilder>>
outgoing_arc_constraints;
auto get_constraint =
[](std::map<int, std::unique_ptr<LinearConstraintBuilder>>* node_map,
int node) {
[m](std::map<int, std::unique_ptr<LinearConstraintBuilder>>* node_map,
int node) {
if (!gtl::ContainsKey(*node_map, node)) {
(*node_map)[node].reset(new LinearConstraintBuilder(1, 1));
(*node_map)[node].reset(
new LinearConstraintBuilder(m->model(), 1, 1));
}
return (*node_map)[node].get();
};
@@ -1857,9 +1857,9 @@ void TryToLinearizeConstraint(
m->Add(NewIntegerVariableFromLiteral(arc));
CHECK(get_constraint(&outgoing_arc_constraints, tail)
->AddLiteralTerm(arc, 1.0, *encoder));
->AddLiteralTerm(arc, 1.0));
CHECK(get_constraint(&incoming_arc_constraints, head)
->AddLiteralTerm(arc, 1.0, *encoder));
->AddLiteralTerm(arc, 1.0));
}
for (const auto* node_map :
{&outgoing_arc_constraints, &incoming_arc_constraints}) {
@@ -1877,7 +1877,7 @@ void TryToLinearizeConstraint(
// We only relax the case where all the vars are constant.
// target = sum (index == i) * fixed_vars[i].
LinearConstraintBuilder constraint(0.0, 0.0);
LinearConstraintBuilder constraint(m->model(), 0.0, 0.0);
constraint.AddTerm(target, -1.0);
for (const auto literal_value : m->Add(FullyEncodeVariable((index)))) {
const IntegerVariable var = vars[literal_value.value.value()];
@@ -1885,8 +1885,8 @@ void TryToLinearizeConstraint(
// Make sure this literal has a view.
m->Add(NewIntegerVariableFromLiteral(literal_value.literal));
CHECK(constraint.AddLiteralTerm(literal_value.literal, m->Get(Value(var)),
*encoder));
CHECK(
constraint.AddLiteralTerm(literal_value.literal, m->Get(Value(var))));
}
linear_constraints->push_back(constraint.Build());
@@ -1896,7 +1896,6 @@ void TryToLinearizeConstraint(
void TryToAddCutGenerators(const CpModelProto& model_proto,
const ConstraintProto& ct, ModelWithMapping* m,
std::vector<CutGenerator>* cut_generators) {
auto* encoder = m->GetOrCreate<IntegerEncoder>();
if (ct.constraint_case() == ConstraintProto::ConstraintCase::kCircuit) {
std::vector<int> tails(ct.circuit().tails().begin(),
ct.circuit().tails().end());
@@ -1919,6 +1918,7 @@ void TryToAddCutGenerators(const CpModelProto& model_proto,
std::vector<int> heads;
std::vector<IntegerVariable> vars;
int num_nodes = 0;
auto* encoder = m->GetOrCreate<IntegerEncoder>();
for (int i = 0; i < ct.routes().tails_size(); ++i) {
const IntegerVariable var =
encoder->GetLiteralView(m->Literal(ct.routes().literals(i)));
@@ -2654,7 +2654,7 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto,
drat_proof_handler.reset(new DratProofHandler(
/*in_binary_format=*/false, output, FLAGS_drat_check));
} else {
drat_proof_handler.reset(nullptr);
drat_proof_handler.reset(new DratProofHandler());
}
solver->SetDratProofHandler(drat_proof_handler.get());
}
@@ -2844,24 +2844,34 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
// TODO(user): improve the normal presolver to do the same thing.
// TODO(user): Support solution hint, but then the first TODO will make it
// automatic.
const SatParameters& params = *model->GetOrCreate<SatParameters>();
if (!model_proto.has_objective() && !model_proto.has_solution_hint() &&
!model->GetOrCreate<SatParameters>()->enumerate_all_solutions()) {
!params.enumerate_all_solutions()) {
bool is_pure_sat = true;
for (const ConstraintProto& ct : model_proto.constraints()) {
if (ct.constraint_case() != ConstraintProto::ConstraintCase::kBoolOr &&
ct.constraint_case() != ConstraintProto::ConstraintCase::kBoolAnd) {
for (const IntegerVariableProto& var : model_proto.variables()) {
if (var.domain_size() != 2 || var.domain(0) < 0 || var.domain(1) > 1) {
is_pure_sat = false;
break;
}
}
if (is_pure_sat) {
for (const ConstraintProto& ct : model_proto.constraints()) {
if (ct.constraint_case() != ConstraintProto::ConstraintCase::kBoolOr &&
ct.constraint_case() != ConstraintProto::ConstraintCase::kBoolAnd) {
is_pure_sat = false;
break;
}
}
}
if (is_pure_sat) return SolvePureSatModel(model_proto, model);
}
// Starts by expanding some constraints if needed.
CpModelProto presolved_proto = ExpandCpModel(model_proto);
// Solve without presolving ?
const auto& observers = model->GetOrCreate<SolutionObservers>()->observers;
if (!model->GetOrCreate<SatParameters>()->cp_model_presolve()) {
if (!params.cp_model_presolve() || params.enumerate_all_solutions()) {
return SolveCpModelInternal(presolved_proto, true,
[&](const CpSolverResponse& response) {
for (const auto& observer : observers) {

7
ortools/sat/integer_search.cc
View File

@@ -280,8 +280,11 @@ SatSolver::Status SolveIntegerProblemWithLazyEncoding(
}
case SatParameters::FIXED_SEARCH: {
auto no_restart = []() { return false; };
return SolveProblemWithPortfolioSearch({next_decision}, {no_restart},
model);
// Not all Boolean might appear in next_decision(), so once there is no
// decision left, we fix all Booleans that are still undecided.
return SolveProblemWithPortfolioSearch(
{SequentialSearch({next_decision, SatSolverHeuristic(model)})},
{no_restart}, model);
}
case SatParameters::PORTFOLIO_SEARCH: {
auto incomplete_portfolio = AddModelHeuristics({next_decision}, model);

32
ortools/sat/linear_programming_constraint.h
View File

@@ -58,7 +58,11 @@ struct LinearConstraint {
// duplicates might be more efficient. Change if required.
class LinearConstraintBuilder {
public:
LinearConstraintBuilder(double lb, double ub) : lb_(lb), ub_(ub) {}
LinearConstraintBuilder(const Model* model, double lb, double ub)
: assignment_(model->Get<Trail>()->Assignment()),
encoder_(*model->Get<IntegerEncoder>()),
lb_(lb),
ub_(ub) {}
int size() const { return terms_.size(); }
bool IsEmpty() const { return terms_.empty(); }
@@ -79,18 +83,26 @@ class LinearConstraintBuilder {
// Add literal * coeff to the constaint. Returns false and do nothing if the
// given literal didn't have an integer view.
bool AddLiteralTerm(Literal lit, double coeff,
const IntegerEncoder& encoder) MUST_USE_RESULT {
bool has_direct_view = encoder.GetLiteralView(lit) != kNoIntegerVariable;
bool AddLiteralTerm(Literal lit, double coeff) MUST_USE_RESULT {
if (assignment_.LiteralIsTrue(lit)) {
lb_ -= coeff;
ub_ -= coeff;
return true;
}
if (assignment_.LiteralIsFalse(lit)) {
return true;
}
bool has_direct_view = encoder_.GetLiteralView(lit) != kNoIntegerVariable;
bool has_opposite_view =
encoder.GetLiteralView(lit.Negated()) != kNoIntegerVariable;
encoder_.GetLiteralView(lit.Negated()) != kNoIntegerVariable;
// If a literal has both views, we want to always keep the same
// representative: the smallest IntegerVariable. Note that AddTerm() will
// also make sure to use the associated positive variable.
if (has_direct_view && has_opposite_view) {
if (encoder.GetLiteralView(lit) <=
encoder.GetLiteralView(lit.Negated())) {
if (encoder_.GetLiteralView(lit) <=
encoder_.GetLiteralView(lit.Negated())) {
has_direct_view = true;
has_opposite_view = false;
} else {
@@ -99,11 +111,11 @@ class LinearConstraintBuilder {
}
}
if (has_direct_view) {
AddTerm(encoder.GetLiteralView(lit), coeff);
AddTerm(encoder_.GetLiteralView(lit), coeff);
return true;
}
if (has_opposite_view) {
AddTerm(encoder.GetLiteralView(lit.Negated()), -coeff);
AddTerm(encoder_.GetLiteralView(lit.Negated()), -coeff);
lb_ -= coeff;
ub_ -= coeff;
return true;
@@ -123,6 +135,8 @@ class LinearConstraintBuilder {
}
private:
const VariablesAssignment& assignment_;
const IntegerEncoder& encoder_;
double lb_;
double ub_;
double offset_;

45
ortools/sat/linear_relaxation.cc
View File

@@ -25,16 +25,16 @@ bool AppendFullEncodingRelaxation(IntegerVariable var, const Model& model,
if (encoder == nullptr) return false;
if (!encoder->VariableIsFullyEncoded(var)) return false;
LinearConstraintBuilder exactly_one_ct(1.0, 1.0);
LinearConstraintBuilder encoding_ct(0.0, 0.0);
LinearConstraintBuilder exactly_one_ct(&model, 1.0, 1.0);
LinearConstraintBuilder encoding_ct(&model, 0.0, 0.0);
encoding_ct.AddTerm(var, 1.0);
// Create the constraint if all literal have a view.
for (const auto value_literal : encoder->FullDomainEncoding(var)) {
const Literal lit = value_literal.literal;
const double coeff = static_cast<double>(value_literal.value.value());
if (!exactly_one_ct.AddLiteralTerm(lit, 1, *encoder)) return false;
if (!encoding_ct.AddLiteralTerm(lit, -coeff, *encoder)) return false;
if (!exactly_one_ct.AddLiteralTerm(lit, 1)) return false;
if (!encoding_ct.AddLiteralTerm(lit, -coeff)) return false;
}
// TODO(user): also skip if var is fixed and there is just one term. Or more
@@ -97,11 +97,11 @@ void AppendPartialEncodingRelaxation(
if (encoding.empty()) return;
const double kInfinity = std::numeric_limits<double>::infinity();
LinearConstraintBuilder at_most_one_ct(-kInfinity, 1.0);
LinearConstraintBuilder at_most_one_ct(&model, -kInfinity, 1.0);
std::unordered_set<IntegerValue> encoded_values;
for (const auto value_literal : encoding) {
// Note that we skip pairs that do not have an Integer view.
if (at_most_one_ct.AddLiteralTerm(value_literal.literal, 1, *encoder)) {
if (at_most_one_ct.AddLiteralTerm(value_literal.literal, 1)) {
encoded_values.insert(value_literal.value);
}
}
@@ -116,14 +116,14 @@ void AppendPartialEncodingRelaxation(
// TODO(user): try to remove the duplication with
// AppendFullEncodingRelaxation()? actually I am not sure we need the other
// function since this one is just more general.
LinearConstraintBuilder exactly_one_ct(1.0, 1.0);
LinearConstraintBuilder encoding_ct(0.0, 0.0);
LinearConstraintBuilder exactly_one_ct(&model, 1.0, 1.0);
LinearConstraintBuilder encoding_ct(&model, 0.0, 0.0);
encoding_ct.AddTerm(var, 1.0);
for (const auto value_literal : encoding) {
const Literal lit = value_literal.literal;
const double coeff = static_cast<double>(value_literal.value.value());
CHECK(exactly_one_ct.AddLiteralTerm(lit, 1, *encoder));
CHECK(encoding_ct.AddLiteralTerm(lit, -coeff, *encoder));
CHECK(exactly_one_ct.AddLiteralTerm(lit, 1));
CHECK(encoding_ct.AddLiteralTerm(lit, -coeff));
}
if (exactly_one_ct.size() > 1) {
constraints->push_back(exactly_one_ct.Build());
@@ -136,22 +136,20 @@ void AppendPartialEncodingRelaxation(
// min + sum li * (xi - min) <= var.
const double d_min = static_cast<double>(pair.first.value());
LinearConstraintBuilder lower_bound_ct(d_min, kInfinity);
LinearConstraintBuilder lower_bound_ct(&model, d_min, kInfinity);
lower_bound_ct.AddTerm(var, 1);
for (const auto value_literal : encoding) {
const double value = static_cast<double>(value_literal.value.value());
CHECK(lower_bound_ct.AddLiteralTerm(value_literal.literal, d_min - value,
*encoder));
CHECK(lower_bound_ct.AddLiteralTerm(value_literal.literal, d_min - value));
}
// var <= max + sum li * (xi - max).
const double d_max = static_cast<double>(pair.second.value());
LinearConstraintBuilder upper_bound_ct(-kInfinity, d_max);
LinearConstraintBuilder upper_bound_ct(&model, -kInfinity, d_max);
upper_bound_ct.AddTerm(var, 1);
for (const auto value_literal : encoding) {
const double value = static_cast<double>(value_literal.value.value());
CHECK(upper_bound_ct.AddLiteralTerm(value_literal.literal, d_max - value,
*encoder));
CHECK(upper_bound_ct.AddLiteralTerm(value_literal.literal, d_max - value));
}
if (at_most_one_ct.size() > 1 && encoded_values.size() > 1) {
@@ -178,7 +176,7 @@ void AppendPartialGreaterThanEncodingRelaxation(
{
IntegerValue prev_used_bound = integer_trail->LowerBound(var);
const double lb = static_cast<double>(prev_used_bound.value());
LinearConstraintBuilder lb_constraint(lb, kInfinity);
LinearConstraintBuilder lb_constraint(&model, lb, kInfinity);
lb_constraint.AddTerm(var, 1.0);
LiteralIndex prev_literal_index = kNoLiteralIndex;
for (const auto entry : greater_than_encoding) {
@@ -189,14 +187,13 @@ void AppendPartialGreaterThanEncodingRelaxation(
static_cast<double>((prev_used_bound - entry.first).value());
// Skip the entry if the literal doesn't have a view.
if (!lb_constraint.AddLiteralTerm(entry.second, diff, *encoder)) continue;
if (!lb_constraint.AddLiteralTerm(entry.second, diff)) continue;
if (prev_literal_index != kNoLiteralIndex) {
// Add var <= prev_var.
LinearConstraintBuilder lower_than(
-std::numeric_limits<double>::infinity(), 0);
CHECK(lower_than.AddLiteralTerm(Literal(literal_index), 1.0, *encoder));
CHECK(lower_than.AddLiteralTerm(Literal(prev_literal_index), -1.0,
*encoder));
&model, -std::numeric_limits<double>::infinity(), 0);
CHECK(lower_than.AddLiteralTerm(Literal(literal_index), 1.0));
CHECK(lower_than.AddLiteralTerm(Literal(prev_literal_index), -1.0));
if (!lower_than.IsEmpty()) constraints->push_back(lower_than.Build());
}
prev_used_bound = entry.first;
@@ -210,7 +207,7 @@ void AppendPartialGreaterThanEncodingRelaxation(
{
IntegerValue prev_used_bound = integer_trail->LowerBound(NegationOf(var));
const double lb = static_cast<double>(prev_used_bound.value());
LinearConstraintBuilder lb_constraint(lb, kInfinity);
LinearConstraintBuilder lb_constraint(&model, lb, kInfinity);
lb_constraint.AddTerm(var, -1.0);
for (const auto entry :
encoder->PartialGreaterThanEncoding(NegationOf(var))) {
@@ -219,7 +216,7 @@ void AppendPartialGreaterThanEncodingRelaxation(
static_cast<double>((prev_used_bound - entry.first).value());
// Skip the entry if the literal doesn't have a view.
if (!lb_constraint.AddLiteralTerm(entry.second, diff, *encoder)) continue;
if (!lb_constraint.AddLiteralTerm(entry.second, diff)) continue;
prev_used_bound = entry.first;
}
if (!lb_constraint.IsEmpty()) constraints->push_back(lb_constraint.Build());

3
ortools/sat/python/cp_model.py
View File

@@ -1118,15 +1118,12 @@ class CpSolver(object):
'satisfiability problems')
# Store old values.
enumerate_all = self.parameters.enumerate_all_solutions
presolve = self.parameters.cp_model_presolve
self.parameters.enumerate_all_solutions = True
self.parameters.cp_model_presolve = False
self.__solution = (
pywrapsat.SatHelper.SolveWithParametersAndSolutionObserver(
model.ModelProto(), self.parameters, callback))
# Restore parameters.
self.parameters.enumerate_all_solutions = enumerate_all
self.parameters.cp_model_presolve = presolve
return self.__solution.status
def Value(self, expression):

11
ortools/sat/sat_parameters.proto
View File

@@ -543,12 +543,13 @@ message SatParameters {
// Whether we also use the sat presolve when cp_model_presolve is true.
optional bool cp_model_use_sat_presolve = 93 [default = true];
// Whether we enumerate all solutions of a SAT problem.
//
// TODO(user): When used with cp_model_presolve, it is possible that not all
// solutions are enumerated. This is because our presolver currently do not
// look at this parameter and only guarantee the existence of one feasible
// Whether we enumerate all solutions of a problem without objective. Note
// that setting this to true automatically disable the presolve. This is
// because the presolve rules only guarantee the existence of one feasible
// solution to the presolved problem.
//
// TODO(user): Activate the presolve but with just the rules that do not
// change the set of feasible solutions.
optional bool enumerate_all_solutions = 87 [default = false];
// If true, then the precedences propagator try to detect for each variable if

1
ortools/util/stats.h
View File

@@ -61,6 +61,7 @@
// times your function calls!
//
// IMPORTANT: The SCOPED_TIME_STAT() macro only does something if OR_STATS is
// defined, so you need to build your code with blaze build --copt='-DOR_STATS'.
// The idea is that by default the instrumentation is off. You can also use the
// macro IF_STATS_ENABLED() that does nothing if OR_STATS is not defined or just
// translates to its argument otherwise.