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

minor improvements to sat solver; continue working on SAT cookbook

Browse Source
This commit is contained in:
Laurent Perron
2018-06-04 11:59:33 +02:00
parent 185b62c997
commit ea0d59e130
8 changed files with 145 additions and 126 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
ortools/sat/cp_model_checker.cc
View File

@@ -158,8 +158,8 @@ std::string ValidateLinearConstraint(const CpModelProto& model,
// Note that we use min/max with zero to disallow "alternative" terms and
// be sure that we cannot have an overflow if we do the computation in a
// different order.
sum_min = CapAdd(sum_min, std::min(0ll, std::min(prod1, prod2)));
sum_max = CapAdd(sum_max, std::max(0ll, std::max(prod1, prod2)));
sum_min = CapAdd(sum_min, std::min(int64{0}, std::min(prod1, prod2)));
sum_max = CapAdd(sum_max, std::max(int64{0}, std::max(prod1, prod2)));
for (const int64 v : {prod1, prod2, sum_min, sum_max}) {
if (v == kint64max || v == kint64min) {
return "Possible integer overflow in constraint: " +
@@ -221,8 +221,8 @@ std::string ValidateObjective(const CpModelProto& model,
// Note that we use min/max with zero to disallow "alternative" terms and
// be sure that we cannot have an overflow if we do the computation in a
// different order.
sum_min = CapAdd(sum_min, std::min(0ll, std::min(prod1, prod2)));
sum_max = CapAdd(sum_max, std::max(0ll, std::max(prod1, prod2)));
sum_min = CapAdd(sum_min, std::min(int64{0}, std::min(prod1, prod2)));
sum_max = CapAdd(sum_max, std::max(int64{0}, std::max(prod1, prod2)));
for (const int64 v : {prod1, prod2, sum_min, sum_max}) {
// When introducing the objective variable, we use a [...] domain so we
// need to be more defensive here to make sure no overflow can happen in

6
ortools/sat/cp_model_presolve.cc
View File

@@ -477,7 +477,7 @@ bool PresolveIntMax(ConstraintProto* ct, PresolveContext* context) {
if (gtl::ContainsKey(used_ref, ref)) continue;
if (gtl::ContainsKey(used_ref, NegatedRef(ref)) ||
ref == NegatedRef(target_ref)) {
target_min = std::max(target_min, 0ll);
target_min = std::max(target_min, int64{0});
}
used_ref.insert(ref);
ct->mutable_int_max()->set_vars(new_size++, ref);
@@ -1850,7 +1850,9 @@ void PresolveCpModel(CpModelProto* presolved_model, CpModelProto* mapping_model,
//
// TODO(user): expose the parameters here so we can use
// cp_model_use_sat_presolve().
PresolvePureSatPart(&context);
if (!context.is_unsat) {
PresolvePureSatPart(&context);
}
if (context.is_unsat) {
// Set presolved_model to the simplest UNSAT problem (empty clause).

145
ortools/sat/doc/boolean_logic.md
View File

@@ -18,7 +18,7 @@ negation of 'x'.
### Python code
```python
from google3.util.operations_research.sat.python import cp_model
from ortools.sat.python import cp_model
model = cp_model.CpModel()
@@ -30,24 +30,26 @@ not_x = x.Not()
### C++ code
```cpp
#include "util/operations_research/sat/cp_model.pb.h"
#include "util/operations_research/sat/cp_model_utils.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_utils.h"
namespace operations_research {
namespace sat {
CpModelProto cp_model;
void LiteralSample() {
CpModelProto cp_model;
auto new_boolean_variable = [&cp_model]() {
const int index = cp_model.variables_size();
IntegerVariableProto* const var = cp_model.add_variables();
var->add_domain(0);
var->add_domain(1);
return index;
};
auto new_boolean_variable = [&cp_model]() {
const int index = cp_model.variables_size();
IntegerVariableProto* const var = cp_model.add_variables();
var->add_domain(0);
var->add_domain(1);
return index;
};
const int x = new_boolean_variable();
const int not_x = NegatedRef(x);
const int x = new_boolean_variable();
const int not_x = NegatedRef(x);
}
} // namespace sat
} // namespace operations_research
@@ -89,7 +91,7 @@ constraints. For instance, we can add a constraint Or(x, not(y)).
### Python code
```python
from google3.util.operations_research.sat.python import cp_model
from ortools.sat.python import cp_model
model = cp_model.CpModel()
@@ -102,34 +104,35 @@ model.AddBoolOr([x, y.Not()])
### C++ code
```cpp
#include "util/operations_research/sat/cp_model.pb.h"
#include "util/operations_research/sat/cp_model_utils.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_utils.h"
namespace operations_research {
namespace sat {
CpModelProto cp_model;
void BoolOrSample() {
CpModelProto cp_model;
auto new_boolean_variable = [&cp_model]() {
const int index = cp_model.variables_size();
IntegerVariableProto* const var = cp_model.add_variables();
var->add_domain(0);
var->add_domain(1);
return index;
};
auto new_boolean_variable = [&cp_model]() {
const int index = cp_model.variables_size();
IntegerVariableProto* const var = cp_model.add_variables();
var->add_domain(0);
var->add_domain(1);
return index;
};
auto add_bool_or = [&cp_model](const std::vector<int>& literals) {
BooleanArgumentProto* const bool_or =
model.add_constraints()->mutable_bool_or();
for (const int lit : literals) {
mutable_bool_or->add_literals(lit);
}
};
const int x = new_boolean_variable();
const int y = new_boolean_variable();
add_bool_or({x, NegatedRef(y)});
auto add_bool_or = [&cp_model](const std::vector<int>& literals) {
BooleanArgumentProto* const bool_or =
model.add_constraints()->mutable_bool_or();
for (const int lit : literals) {
mutable_bool_or->add_literals(lit);
}
};
const int x = new_boolean_variable();
const int y = new_boolean_variable();
add_bool_or({x, NegatedRef(y)});
}
} // namespace sat
} // namespace operations_research
```
@@ -176,7 +179,7 @@ then is written as Or(not b, x) and Or(not b, not y).
### Python code
```python
from google3.util.operations_research.sat.python import cp_model
from ortools.sat.python import cp_model
model = cp_model.CpModel()
@@ -199,49 +202,51 @@ model.AddBoolOt([b.Not(), y.Not()])
### C++ code
```cpp
#include "util/operations_research/sat/cp_model.pb.h"
#include "util/operations_research/sat/cp_model_utils.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_utils.h"
namespace operations_research {
namespace sat {
CpModelProto cp_model;
void ReifiedSample() {
CpModelProto cp_model;
auto new_boolean_variable = [&cp_model]() {
const int index = cp_model.variables_size();
IntegerVariableProto* const var = cp_model.add_variables();
var->add_domain(0);
var->add_domain(1);
return index;
};
auto new_boolean_variable = [&cp_model]() {
const int index = cp_model.variables_size();
IntegerVariableProto* const var = cp_model.add_variables();
var->add_domain(0);
var->add_domain(1);
return index;
};
auto add_bool_or = [&cp_model](const std::vector<int>& literals) {
BooleanArgumentProto* const bool_or =
model.add_constraints()->mutable_bool_or();
for (const int lit : literals) {
mutable_bool_or->add_literals(lit);
}
};
auto add_bool_or = [&cp_model](const std::vector<int>& literals) {
BooleanArgumentProto* const bool_or =
model.add_constraints()->mutable_bool_or();
for (const int lit : literals) {
mutable_bool_or->add_literals(lit);
}
};
auto add_reified_bool_and = [&cp_model](const std::vector<int>& literals,
const int literal) {
Constraint* const ct = model.add_constraints();
ct->add_enforcement_literal(literal);
for (const int lit : literals) {
ct->mutable_bool_and()->add_literals(lit);
}
};
auto add_reified_bool_and = [&cp_model](const std::vector<int>& literals,
const int literal) {
Constraint* const ct = model.add_constraints();
ct->add_enforcement_literal(literal);
for (const int lit : literals) {
ct->mutable_bool_and()->add_literals(lit);
}
};
const int x = new_boolean_variable();
const int y = new_boolean_variable();
const int b = new_boolean_variable();
const int x = new_boolean_variable();
const int y = new_boolean_variable();
const int b = new_boolean_variable();
// First version using a half-reified bool and.
add_reified_bool_and({x, NegatedRef(y)}, b);
// First version using a half-reified bool and.
add_reified_bool_and({x, NegatedRef(y)}, b);
// Second version using implications.
add_bool_or({NegatedRef(b), x});
add_bool_or({NegatedRef(b), NegatedRef(y)});
// Second version using bool or.
add_bool_or({NegatedRef(b), x});
add_bool_or({NegatedRef(b), NegatedRef(y)});
}
} // namespace sat
} // namespace operations_research
@@ -279,4 +284,4 @@ public class CodeSamplesSat
ReifiedSample();
}
}
```
```

15
ortools/sat/doc/index.md
View File

@@ -20,8 +20,8 @@ The Python interface to the CP-SAT solver is implemented using two classes.
* The **CpModel** class proposes modeling methods that creates variables, or
add constraints. This class completely hides the underlying *CpModelProto*
used to store the model.
* The **CpSolver** class encapsulates the solve API. and offers
helpers to access the solution found by the solve.
* The **CpSolver** class encapsulates the solve API. and offers helpers to
access the solution found by the solve.
```python
from ortools.sat.python import cp_model
@@ -34,7 +34,8 @@ x = model.NewBoolVar('x')
## C++ code samples
The interface to the C++ CP-SAT solver is implemented through the
**CpModelProto** class described in *ortools/sat/cp_model.proto*.
**CpModelProto** class described in
*ortools/sat/cp_model.proto*.
To help creating variables and constraints, we propose some inline helpers to
improve readability.
@@ -64,7 +65,7 @@ void CodeSample() {
} // namespace operations_research
```
## C\# code
## C\# code samples
The C\# code implements the same interface as the python code, with a
**CpModel**, and a **CpSolver** class.
@@ -75,14 +76,16 @@ using Google.OrTools.Sat;
public class CodeSamplesSat
{
static void CodeSample() {
static void CodeSample()
{
// Creates the model.
CpModel model = new CpModel();
// Creates the Boolean variable.
IntVar x = model.NewBoolVar("x");
}
static void Main() {
static void Main()
{
CodeSample();
}
}

52
ortools/sat/doc/scheduling.md
View File

@@ -41,35 +41,37 @@ interval_var = model.NewIntervalVar(start_var, duration, end_var, 'interval')
namespace operations_research {
namespace sat {
CpModelProto cp_model;
void IntervalSample() {
CpModelProto cp_model;
auto new_variable = [&cp_model](int64 lb, int64 ub) {
CHECK_LE(lb, ub);
const int index = cp_model.variables_size();
IntegerVariableProto* const var = cp_model.add_variables();
var->add_domain(lb);
var->add_domain(ub);
return index;
};
auto new_variable = [&cp_model](int64 lb, int64 ub) {
CHECK_LE(lb, ub);
const int index = cp_model.variables_size();
IntegerVariableProto* const var = cp_model.add_variables();
var->add_domain(lb);
var->add_domain(ub);
return index;
};
auto new_constant = [&cp_model, &new_variable](int64 v) {
return new_variable(v, v);
};
auto new_constant = [&cp_model, &new_variable](int64 v) {
return new_variable(v, v);
};
auto new_interval = [&cp_model](int start, int duration, int end) {
const int index = cp_model.constraints_size();
IntervalConstraintProto* const interval =
cp_model.add_constraints()->mutable_interval();
interval_proto->set_start(start);
interval_proto->set_size(duration);
interval_proto->set_end(end);
return index;
};
auto new_interval = [&cp_model](int start, int duration, int end) {
const int index = cp_model.constraints_size();
IntervalConstraintProto* const interval =
cp_model.add_constraints()->mutable_interval();
interval_proto->set_start(start);
interval_proto->set_size(duration);
interval_proto->set_end(end);
return index;
};
const int start_var = new_variable(0, horizon);
const int duration_var = new_constant(10);
const int end_var = new_variable(0, horizon);
const int interval_var = new_interval(start_var, duration_var, end_var);
const int start_var = new_variable(0, horizon);
const int duration_var = new_constant(10);
const int end_var = new_variable(0, horizon);
const int interval_var = new_interval(start_var, duration_var, end_var);
}
} // namespace sat
} // namespace operations_research

40
ortools/sat/doc/solver.md
View File

@@ -1,12 +1,12 @@
# Solving a CP-SAT model
https://developers.google.com/optimization/
## Searching for one (optimal) solution
By default, search for one solution will return the first solution found if the
model has no objective, or the optimal solution if the model has an objective.
By default, searching for one solution will return the first solution found if
the model has no objective, or the optimal solution if the model has an
objective.
### Python solver code
@@ -22,8 +22,7 @@ x = model.NewBoolVar('x')
# Create a solver and solve.
solver = cp_model.CpSolver()
status = solver.Solve(model)
if status == cp_model.OPTIMAL:
print("Objective value: %i" % solver.ObjectiveValue()) # if defined.
if status == cp_model.MODEL_SAT:
print('x= %i' % solver.Value(x))
```
@@ -73,7 +72,10 @@ void SimpleSolve() {
} // namespace operations_research
```
### C\# solver code
### C\# code
As in python, the CpSolver class encapsulates searching for a solution of a
model.
```cs
using System;
@@ -115,8 +117,8 @@ public class CodeSamplesSat
## Changing the parameters of the solver
The SatParameters protobuf encapsulate a set of parameters of a CP-SAT solver.
The most useful one is the time limit.
The SatParameters protobuf encapsulates the set of parameters of a CP-SAT
solver. The most useful one is the time limit.
### Specifying the time limit in python
@@ -182,7 +184,6 @@ void SolveWithTimeLimit() {
if (response.status() == CpSolverStatus::MODEL_SAT) {
// Get the value of x in the solution.
const int64 value_x = response.solution(x);
LOG(INFO) << "x = " << value_x;
}
}
@@ -238,7 +239,7 @@ public class CodeSamplesSat
## Printing intermediate solutions
In an optimization model, you can print intermediate solution. You need to
In an optimization model, you can print intermediate solutions. You need to
register a callback on the solver that will be called at each solution.
The exact implementation depends on the target language.
@@ -277,11 +278,11 @@ def MinimalCpSatPrintIntermediateSolutions():
x = model.NewIntVar(0, num_vals - 1, "x")
y = model.NewIntVar(0, num_vals - 1, "y")
z = model.NewIntVar(0, num_vals - 1, "z")
# Create the constraints.
# Creates the constraints.
model.Add(x != y)
model.Maximize(x + 2 * y + 3 * z)
# Create a solver and solve.
# Creates a solver and solve.
solver = cp_model.CpSolver()
solution_printer = VarArraySolutionPrinter([x, y, z])
status = solver.SolveWithSolutionObserver(model, solution_printer)
@@ -402,7 +403,6 @@ public class VarArraySolutionPrinterWithObjective : CpSolverSolutionCallback
private IntVar[] variables_;
}
public class CodeSamplesSat
{
static void MinimalCpSatPrintIntermediateSolutions()
@@ -417,7 +417,7 @@ public class CodeSamplesSat
IntVar z = model.NewIntVar(0, num_vals - 1, "z");
// Creates the constraints.
model.Add(x != y);
// Create the objective.
// Creates the objective.
model.Maximize(x + 2 * y + 3 * z);
// Creates a solver and solves the model.
@@ -445,6 +445,8 @@ The exact implementation depends on the target language.
### Python code
To search for all solutions, the SearchForAllSolutions method must be used.
```python
from ortools.sat.python import cp_model
@@ -476,10 +478,10 @@ def MinimalSatSearchForAllSolutions():
x = model.NewIntVar(0, num_vals - 1, "x")
y = model.NewIntVar(0, num_vals - 1, "y")
z = model.NewIntVar(0, num_vals - 1, "z")
# Create the constraints.
# Creates the constraint.
model.Add(x != y)
# Create a solver and solve.
# Creates a solver and solve.
solver = cp_model.CpSolver()
solution_printer = VarArraySolutionPrinter([x, y, z])
status = solver.SearchForAllSolutions(model, solution_printer)
@@ -489,6 +491,8 @@ def MinimalSatSearchForAllSolutions():
### C++ code
To search for all solution, a parameter of the sat solver must be changed.
```cpp
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
@@ -555,6 +559,8 @@ void MinimalSatSearchForAllSolutions() {
### C\# code
As in python, CpSolver.SearchAllSolutions() must be called.
```cs
using System;
using Google.OrTools.Sat;
@@ -619,4 +625,4 @@ public class CodeSamplesSat
MinimalCpSatAllSolutions();
}
}
```
```

4
ortools/sat/drat_checker.cc
View File

@@ -98,8 +98,8 @@ ClauseIndex DratChecker::AddClause(absl::Span<Literal> clause) {
for (int i = first_literal_index + 1; i < literals_.size(); ++i) {
CHECK(literals_[i] != literals_[i - 1].Negated());
}
clauses_.push_back(Clause(first_literal_index,
literals_.size() - first_literal_index));
clauses_.emplace_back(first_literal_index,
literals_.size() - first_literal_index);
if (!clause.empty()) {
num_variables_ =
std::max(num_variables_, literals_.back().Variable().value() + 1);

1
ortools/sat/linear_programming_constraint.cc
View File

@@ -271,6 +271,7 @@ bool LinearProgrammingConstraint::Propagate() {
lp_data_.SetConstraintBounds(row, cut.lb, cut.ub);
for (int i = 0; i < cut.vars.size(); ++i) {
const glop::ColIndex col = GetOrCreateMirrorVariable(cut.vars[i]);
// The returned coefficients correspond to variables at the CP scale,
// so we need to divide them by CpToLpScalingFactor() which is the
// same as multiplying by LpToCpScalingFactor().