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

reorganize SIGINT catching

Browse Source
This commit is contained in:
Laurent Perron
2019-06-27 17:28:56 +02:00
parent 00a87db3d6
commit 7115cf570f
14 changed files with 1724 additions and 1660 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
examples/cpp/sat_runner.cc
View File

@@ -11,7 +11,6 @@
// See the License for the specific language governing permissions and
// limitations under the License.
#include <atomic>
#include <cstdio>
#include <cstdlib>
#include <memory>
@@ -50,7 +49,6 @@
#include "ortools/sat/simplification.h"
#include "ortools/sat/symmetry.h"
#include "ortools/util/file_util.h"
#include "ortools/util/sigint.h"
#include "ortools/util/time_limit.h"
DEFINE_string(
@@ -196,9 +194,6 @@ int Run() {
LOG(FATAL) << "Please supply a data file with --input=";
}
// In the algorithms below, this seems like a good parameter.
parameters.set_count_assumption_levels_in_lbd(false);
// Parse the --params flag.
if (!FLAGS_params.empty()) {
CHECK(google::protobuf::TextFormat::MergeFromString(FLAGS_params,
@@ -216,7 +211,6 @@ int Run() {
if (!LoadBooleanProblem(FLAGS_input, &problem, &cp_model)) {
CpSolverResponse response;
response.set_status(CpSolverStatus::MODEL_INVALID);
LOG(INFO) << CpSolverResponseStats(response);
return EXIT_SUCCESS;
}
if (FLAGS_use_cp_model && cp_model.variables_size() == 0) {
@@ -228,15 +222,9 @@ int Run() {
// completely replaced by the more general CpModelProto.
if (!cp_model.variables().empty()) {
problem.Clear(); // We no longer need it, release memory.
std::atomic<bool> stopped(false);
Model model;
model.Add(NewSatParameters(parameters));
model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(&stopped);
model.GetOrCreate<SigintHandler>()->Register(
[&stopped]() { stopped = true; });
LOG(INFO) << CpModelStats(cp_model);
const CpSolverResponse response = SolveCpModel(cp_model, &model);
LOG(INFO) << CpSolverResponseStats(response);
if (!FLAGS_output.empty()) {
if (absl::EndsWith(FLAGS_output, ".txt")) {

8
makefiles/Makefile.gen.mk
View File

@@ -1438,10 +1438,10 @@ objs/sat/cp_model_solver.$O: ortools/sat/cp_model_solver.cc \
ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/model.h \
ortools/base/logging.h ortools/base/macros.h ortools/base/map_util.h \
ortools/base/typeid.h ortools/gen/ortools/sat/sat_parameters.pb.h \
ortools/base/file.h ortools/base/status.h ortools/base/cleanup.h \
ortools/base/commandlineflags.h ortools/base/int_type.h \
ortools/base/int_type_indexed_vector.h ortools/base/threadpool.h \
ortools/base/timer.h ortools/base/basictypes.h \
ortools/base/file.h ortools/base/status.h ortools/util/sigint.h \
ortools/base/cleanup.h ortools/base/commandlineflags.h \
ortools/base/int_type.h ortools/base/int_type_indexed_vector.h \
ortools/base/threadpool.h ortools/base/timer.h ortools/base/basictypes.h \
ortools/graph/connectivity.h ortools/port/proto_utils.h \
ortools/sat/circuit.h ortools/sat/integer.h ortools/base/hash.h \
ortools/graph/iterators.h ortools/sat/sat_base.h ortools/util/bitset.h \

1
ortools/flatzinc/BUILD
View File

@@ -148,7 +148,6 @@ cc_library(
"//ortools/sat:optimization",
"//ortools/sat:sat_solver",
"//ortools/sat:table",
"//ortools/util:sigint",
":checker",
":logging",
":model",

7
ortools/flatzinc/cp_model_fz_solver.cc
View File

@@ -43,8 +43,6 @@
#include "ortools/sat/optimization.h"
#include "ortools/sat/sat_solver.h"
#include "ortools/sat/table.h"
#include "ortools/util/sigint.h"
#include "ortools/util/time_limit.h"
DEFINE_bool(use_flatzinc_format, true, "Output uses the flatzinc format");
@@ -1002,10 +1000,6 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
<< sat_params;
m.parameters.MergeFrom(flag_parameters);
std::atomic<bool> stopped(false);
SigintHandler handler;
handler.Register([&stopped]() { stopped = true; });
// We only need an observer if 'p.all_solutions' is true.
std::function<void(const CpSolverResponse&)> solution_observer = nullptr;
if (p.display_all_solutions && FLAGS_use_flatzinc_format) {
@@ -1024,7 +1018,6 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
Model sat_model;
sat_model.Add(NewSatParameters(m.parameters));
sat_model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(&stopped);
if (solution_observer != nullptr) {
sat_model.Add(NewFeasibleSolutionObserver(solution_observer));
}

3
ortools/sat/BUILD
View File

@@ -191,6 +191,7 @@ cc_library(
"//ortools/base:threadpool",
"//ortools/graph:connectivity",
"//ortools/port:proto_utils",
"//ortools/util:sigint",
"//ortools/util:sorted_interval_list",
"//ortools/util:time_limit",
"@com_google_absl//absl/base:core_headers",
@@ -1134,7 +1135,5 @@ cc_library(
":model",
":sat_parameters_cc_proto",
"//ortools/base",
"//ortools/util:sigint",
"//ortools/util:time_limit",
],
)

263
ortools/sat/cp_model_loader.cc
View File

@@ -499,6 +499,269 @@ void CpModelMapping::DetectOptionalVariables(const CpModelProto& model_proto,
VLOG(2) << "Auto-detected " << num_optionals << " optional variables.";
}
// ============================================================================
// A class that detects when variables should be fully encoded by computing a
// fixed point. It also fully encodes such variables.
// ============================================================================
class FullEncodingFixedPointComputer {
public:
FullEncodingFixedPointComputer(const CpModelProto& model_proto, Model* model)
: model_proto_(model_proto),
parameters_(*(model->GetOrCreate<SatParameters>())),
model_(model),
mapping_(model->GetOrCreate<CpModelMapping>()),
integer_encoder_(model->GetOrCreate<IntegerEncoder>()),
integer_trail_(model->GetOrCreate<IntegerTrail>()) {}
void ComputeFixedPoint();
private:
DEFINE_INT_TYPE(ConstraintIndex, int32);
// Constraint ct is interested by (full-encoding) state of variable.
void Register(ConstraintIndex ct_index, int variable) {
variable = PositiveRef(variable);
constraint_is_registered_[ct_index] = true;
if (variable_watchers_.size() <= variable) {
variable_watchers_.resize(variable + 1);
variable_was_added_in_to_propagate_.resize(variable + 1);
}
variable_watchers_[variable].push_back(ct_index);
}
void AddVariableToPropagationQueue(int variable) {
variable = PositiveRef(variable);
if (variable_was_added_in_to_propagate_.size() <= variable) {
variable_watchers_.resize(variable + 1);
variable_was_added_in_to_propagate_.resize(variable + 1);
}
if (!variable_was_added_in_to_propagate_[variable]) {
variable_was_added_in_to_propagate_[variable] = true;
variables_to_propagate_.push_back(variable);
}
}
// Note that we always consider a fixed variable to be fully encoded here.
const bool IsFullyEncoded(int v) {
const IntegerVariable variable = mapping_->Integer(v);
if (v == kNoIntegerVariable) return false;
return model_->Get(IsFixed(variable)) ||
integer_encoder_->VariableIsFullyEncoded(variable);
}
void FullyEncode(int v) {
v = PositiveRef(v);
const IntegerVariable variable = mapping_->Integer(v);
if (v == kNoIntegerVariable) return;
if (!model_->Get(IsFixed(variable))) {
model_->Add(FullyEncodeVariable(variable));
}
AddVariableToPropagationQueue(v);
}
bool ProcessConstraint(ConstraintIndex ct_index);
bool ProcessElement(ConstraintIndex ct_index);
bool ProcessTable(ConstraintIndex ct_index);
bool ProcessAutomaton(ConstraintIndex ct_index);
bool ProcessInverse(ConstraintIndex ct_index);
bool ProcessLinear(ConstraintIndex ct_index);
const CpModelProto& model_proto_;
const SatParameters& parameters_;
Model* model_;
CpModelMapping* mapping_;
IntegerEncoder* integer_encoder_;
IntegerTrail* integer_trail_;
std::vector<bool> variable_was_added_in_to_propagate_;
std::vector<int> variables_to_propagate_;
std::vector<std::vector<ConstraintIndex>> variable_watchers_;
gtl::ITIVector<ConstraintIndex, bool> constraint_is_finished_;
gtl::ITIVector<ConstraintIndex, bool> constraint_is_registered_;
};
// We only add to the propagation queue variable that are fully encoded.
// Note that if a variable was already added once, we never add it again.
void FullEncodingFixedPointComputer::ComputeFixedPoint() {
const int num_constraints = model_proto_.constraints_size();
constraint_is_registered_.assign(num_constraints, false);
constraint_is_finished_.assign(num_constraints, false);
// Process all constraint once.
for (ConstraintIndex ct_index(0); ct_index < num_constraints; ++ct_index) {
ProcessConstraint(ct_index);
}
// Make sure all fully encoded variables of interest are in the queue.
for (int v = 0; v < variable_watchers_.size(); v++) {
if (!variable_watchers_[v].empty() && IsFullyEncoded(v)) {
AddVariableToPropagationQueue(v);
}
}
// Loop until no additional variable can be fully encoded.
while (!variables_to_propagate_.empty()) {
const int variable = variables_to_propagate_.back();
variables_to_propagate_.pop_back();
for (const ConstraintIndex ct_index : variable_watchers_[variable]) {
if (constraint_is_finished_[ct_index]) continue;
constraint_is_finished_[ct_index] = ProcessConstraint(ct_index);
}
}
}
// Returns true if the constraint has finished encoding what it wants.
bool FullEncodingFixedPointComputer::ProcessConstraint(
ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
switch (ct.constraint_case()) {
case ConstraintProto::ConstraintProto::kElement:
return ProcessElement(ct_index);
case ConstraintProto::ConstraintProto::kTable:
return ProcessTable(ct_index);
case ConstraintProto::ConstraintProto::kAutomaton:
return ProcessAutomaton(ct_index);
case ConstraintProto::ConstraintProto::kInverse:
return ProcessInverse(ct_index);
case ConstraintProto::ConstraintProto::kLinear:
return ProcessLinear(ct_index);
default:
return true;
}
}
bool FullEncodingFixedPointComputer::ProcessElement(ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
// Index must always be full encoded.
FullyEncode(ct.element().index());
// If target is a constant or fully encoded, variables must be fully encoded.
const int target = ct.element().target();
if (IsFullyEncoded(target)) {
for (const int v : ct.element().vars()) FullyEncode(v);
}
// If all non-target variables are fully encoded, target must be too.
bool all_variables_are_fully_encoded = true;
for (const int v : ct.element().vars()) {
if (v == target) continue;
if (!IsFullyEncoded(v)) {
all_variables_are_fully_encoded = false;
break;
}
}
if (all_variables_are_fully_encoded) {
if (!IsFullyEncoded(target)) FullyEncode(target);
return true;
}
// If some variables are not fully encoded, register on those.
if (constraint_is_registered_[ct_index]) {
for (const int v : ct.element().vars()) Register(ct_index, v);
Register(ct_index, target);
}
return false;
}
bool FullEncodingFixedPointComputer::ProcessTable(ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
// TODO(user): This constraint also fully encode variable sometimes. Find a
// way to be in sync.
if (ct.table().negated()) return true;
for (const int variable : ct.table().vars()) {
FullyEncode(variable);
}
return true;
}
bool FullEncodingFixedPointComputer::ProcessAutomaton(
ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
for (const int variable : ct.automaton().vars()) {
FullyEncode(variable);
}
return true;
}
bool FullEncodingFixedPointComputer::ProcessInverse(ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
for (const int variable : ct.inverse().f_direct()) {
FullyEncode(variable);
}
for (const int variable : ct.inverse().f_inverse()) {
FullyEncode(variable);
}
return true;
}
bool FullEncodingFixedPointComputer::ProcessLinear(ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
if (parameters_.boolean_encoding_level() == 0) return true;
// Only act when the constraint is an equality.
if (ct.linear().domain(0) != ct.linear().domain(1)) return true;
// If some domain is too large, abort;
if (!constraint_is_registered_[ct_index]) {
for (const int v : ct.linear().vars()) {
const IntegerVariable var = mapping_->Integer(v);
const IntegerValue lb = integer_trail_->LowerBound(var);
const IntegerValue ub = integer_trail_->UpperBound(var);
if (ub - lb > 1024) return true; // Arbitrary limit value.
}
}
const int num_vars = ct.linear().vars_size();
if (HasEnforcementLiteral(ct)) {
// Fully encode x in half-reified equality b => x == constant.
if (num_vars == 1) FullyEncode(ct.linear().vars(0));
// Skip any other form of half-reified linear constraint for now.
return true;
}
// If all variables but one are fully encoded,
// force the last one to be fully encoded.
int variable_not_fully_encoded;
int num_fully_encoded = 0;
for (const int var : ct.linear().vars()) {
if (IsFullyEncoded(var)) {
num_fully_encoded++;
} else {
variable_not_fully_encoded = var;
}
}
if (num_fully_encoded == num_vars - 1) {
FullyEncode(variable_not_fully_encoded);
return true;
}
if (num_fully_encoded == num_vars) return true;
// Register on remaining variables if not already done.
if (!constraint_is_registered_[ct_index]) {
for (const int var : ct.linear().vars()) {
if (!IsFullyEncoded(var)) Register(ct_index, var);
}
}
return false;
}
void MaybeFullyEncodeMoreVariables(const CpModelProto& model_proto, Model* m) {
FullEncodingFixedPointComputer fixpoint(model_proto, m);
fixpoint.ComputeFixedPoint();
}
// ============================================================================
// Constraint loading functions.
// ============================================================================
void LoadBoolOrConstraint(const ConstraintProto& ct, Model* m) {
auto* mapping = m->GetOrCreate<CpModelMapping>();
std::vector<Literal> literals = mapping->Literals(ct.bool_or().literals());

10
ortools/sat/cp_model_loader.h
View File

@@ -179,6 +179,16 @@ class CpModelMapping {
absl::flat_hash_set<const ConstraintProto*> is_half_encoding_ct_;
};
// Inspects the model and use some heuristic to decide which variable, if any,
// should be fully encoded. Note that some constraints like the element or table
// constraints require some of their variables to be fully encoded.
//
// TODO(user): This function exists so that we fully encode first all the
// variable that needs to be fully encoded so that at loading time we can adapt
// the algorithm used. Howeve it needs to duplicate the logic that decide what
// needs to be fully encoded. Try to come up with a more robust design.
void MaybeFullyEncodeMoreVariables(const CpModelProto& model_proto, Model* m);
// Calls one of the functions below.
// Returns false if we do not know how to load the given constraints.
bool LoadConstraint(const ConstraintProto& ct, Model* m);

2617
ortools/sat/cp_model_presolve.cc
View File

File diff suppressed because it is too large Load Diff

123
ortools/sat/cp_model_presolve.h
View File

@@ -187,6 +187,15 @@ struct PresolveContext {
std::vector<Domain> domains;
};
// Replaces all the instance of a variable i (and the literals referring to it)
// by mapping[i]. The definition of variables i is also moved to its new index.
// Variables with a negative mapping value are ignored and it is an error if
// such variable is referenced anywhere (this is CHECKed).
//
// The image of the mapping should be dense in [0, new_num_variables), this is
// also CHECKed.
void ApplyVariableMapping(const std::vector<int>& mapping, CpModelProto* proto);
// Presolves the initial content of presolved_model.
//
// This also creates a mapping model that encode the correspondence between the
@@ -208,24 +217,110 @@ struct PresolveContext {
// TODO(user): Identify disconnected components and returns a vector of
// presolved model? If we go this route, it may be nicer to store the indices
// inside the model. We can add a IntegerVariableProto::initial_index;
//
// Returns false if a non-recoverable error was encountered.
//
// TODO(user): Make sure this can never run into this case provided that the
// initial model is valid!
class CpModelPresolver {
public:
CpModelPresolver(const PresolveOptions& options,
CpModelProto* presolved_model, CpModelProto* mapping_model,
std::vector<int>* postsolve_mapping);
// Returns false if a non-recoverable error was encountered.
//
// TODO(user): Make sure this can never run into this case provided that the
// initial model is valid!
bool Presolve();
private:
void PresolveToFixPoint();
// Runs the probing.
void Probe();
// Presolve functions.
//
// They should return false only if the constraint <-> variable graph didn't
// change. This is just an optimization, returning true is always correct.
//
// Invariant about UNSAT: All these functions should abort right away if
// context_.IsUnsat() is true. And the only way to change the status to unsat
// is through ABSL_MUST_USE_RESULT function that should also abort right away
// the current code. This way we shouldn't keep doing computation on an
// inconsistent state.
// TODO(user,user): Make these public and unit test.
bool PresolveOneConstraint(int c);
bool PresolveAutomaton(ConstraintProto* ct);
bool PresolveCircuit(ConstraintProto* ct);
bool PresolveCumulative(ConstraintProto* ct);
bool PresolveNoOverlap(ConstraintProto* ct);
bool PresolveAllDiff(ConstraintProto* ct);
bool PresolveTable(ConstraintProto* ct);
bool PresolveElement(ConstraintProto* ct);
bool PresolveInterval(int c, ConstraintProto* ct);
bool PresolveLinear(ConstraintProto* ct);
bool PresolveLinearOnBooleans(ConstraintProto* ct);
bool CanonicalizeLinear(ConstraintProto* ct);
bool RemoveSingletonInLinear(ConstraintProto* ct);
bool PresolveIntDiv(ConstraintProto* ct);
bool PresolveIntProd(ConstraintProto* ct);
bool PresolveIntMin(ConstraintProto* ct);
bool PresolveIntMax(ConstraintProto* ct);
bool PresolveBoolXor(ConstraintProto* ct);
bool PresolveAtMostOne(ConstraintProto* ct);
bool PresolveBoolAnd(ConstraintProto* ct);
bool PresolveBoolOr(ConstraintProto* ct);
bool PresolveEnforcementLiteral(ConstraintProto* ct);
// SetPPC is short for set packing, partitioning and covering constraints.
// These are sum of booleans <=, = and >= 1 respectively.
bool ProcessSetPPC();
// Removes dominated constraints or fixes some variables for given pair of
// setppc constraints. This assumes that literals in constraint c1 is subset
// of literals in constraint c2.
bool ProcessSetPPCSubset(int c1, int c2, const std::vector<int>& c2_minus_c1,
const std::vector<int>& original_constraint_index,
std::vector<bool>* marked_for_removal);
void PresolvePureSatPart();
// Extracts AtMostOne constraint from Linear constraint.
void ExtractAtMostOneFromLinear(ConstraintProto* ct);
void DivideLinearByGcd(ConstraintProto* ct);
void ExtractEnforcementLiteralFromLinearConstraint(ConstraintProto* ct);
// Extracts cliques from bool_and and small at_most_one constraints and
// transforms them into maximal cliques.
void TransformIntoMaxCliques();
// Converts bool_or and at_most_one of size 2 to bool_and.
void ExtractBoolAnd();
void ExpandObjective();
void TryToSimplifyDomains();
void MergeNoOverlapConstraints();
void RemoveUnusedEquivalentVariables();
bool IntervalsCanIntersect(const IntervalConstraintProto& interval1,
const IntervalConstraintProto& interval2);
bool ExploitEquivalenceRelations(ConstraintProto* ct);
ABSL_MUST_USE_RESULT bool RemoveConstraint(ConstraintProto* ct);
ABSL_MUST_USE_RESULT bool MarkConstraintAsFalse(ConstraintProto* ct);
const PresolveOptions& options_;
std::vector<int>* postsolve_mapping_;
PresolveContext context_;
};
// Convenient wrapper to call the full presolve.
bool PresolveCpModel(const PresolveOptions& options,
CpModelProto* presolved_model, CpModelProto* mapping_model,
std::vector<int>* postsolve_mapping);
// Replaces all the instance of a variable i (and the literals referring to it)
// by mapping[i]. The definition of variables i is also moved to its new index.
// Variables with a negative mapping value are ignored and it is an error if
// such variable is referenced anywhere (this is CHECKed).
//
// The image of the mapping should be dense in [0, new_num_variables), this is
// also CHECKed.
void ApplyVariableMapping(const std::vector<int>& mapping, CpModelProto* proto);
} // namespace sat
} // namespace operations_research

274
ortools/sat/cp_model_solver.cc
View File

@@ -28,6 +28,7 @@
#include "absl/synchronization/notification.h"
#include "google/protobuf/text_format.h"
#include "ortools/base/file.h"
#include "ortools/util/sigint.h"
#endif // __PORTABLE_PLATFORM__
#include "absl/container/flat_hash_set.h"
@@ -114,260 +115,6 @@ namespace sat {
namespace {
// =============================================================================
// A class that detects when variables should be fully encoded by computing a
// fixed point.
// =============================================================================
// This class is will ask the underlying Model to fully encode IntegerVariables
// of the model using constraint processors PropagateConstraintXXX(), until no
// such processor wants to fully encode a variable. The workflow is to call
// PropagateFullEncoding() on a set of constraints, then ComputeFixedPoint() to
// launch the fixed point computation.
class FullEncodingFixedPointComputer {
public:
FullEncodingFixedPointComputer(const CpModelProto& model_proto, Model* model)
: model_proto_(model_proto),
parameters_(*(model->GetOrCreate<SatParameters>())),
model_(model),
mapping_(model->GetOrCreate<CpModelMapping>()),
integer_encoder_(model->GetOrCreate<IntegerEncoder>()) {}
void ComputeFixedPoint();
private:
DEFINE_INT_TYPE(ConstraintIndex, int32);
// Constraint ct is interested by (full-encoding) state of variable.
void Register(ConstraintIndex ct_index, int variable) {
variable = PositiveRef(variable);
constraint_is_registered_[ct_index] = true;
if (variable_watchers_.size() <= variable) {
variable_watchers_.resize(variable + 1);
variable_was_added_in_to_propagate_.resize(variable + 1);
}
variable_watchers_[variable].push_back(ct_index);
}
void AddVariableToPropagationQueue(int variable) {
variable = PositiveRef(variable);
if (variable_was_added_in_to_propagate_.size() <= variable) {
variable_watchers_.resize(variable + 1);
variable_was_added_in_to_propagate_.resize(variable + 1);
}
if (!variable_was_added_in_to_propagate_[variable]) {
variable_was_added_in_to_propagate_[variable] = true;
variables_to_propagate_.push_back(variable);
}
}
// Note that we always consider a fixed variable to be fully encoded here.
const bool IsFullyEncoded(int v) {
const IntegerVariable variable = mapping_->Integer(v);
return model_->Get(IsFixed(variable)) ||
integer_encoder_->VariableIsFullyEncoded(variable);
}
void FullyEncode(int v) {
v = PositiveRef(v);
const IntegerVariable variable = mapping_->Integer(v);
if (!model_->Get(IsFixed(variable))) {
model_->Add(FullyEncodeVariable(variable));
}
AddVariableToPropagationQueue(v);
}
bool PropagateFullEncoding(ConstraintIndex ct_index);
bool PropagateElement(ConstraintIndex ct_index);
bool PropagateTable(ConstraintIndex ct_index);
bool PropagateAutomaton(ConstraintIndex ct_index);
bool PropagateInverse(ConstraintIndex ct_index);
bool PropagateLinear(ConstraintIndex ct_index);
const CpModelProto& model_proto_;
const SatParameters& parameters_;
Model* model_;
CpModelMapping* mapping_;
IntegerEncoder* integer_encoder_;
std::vector<bool> variable_was_added_in_to_propagate_;
std::vector<int> variables_to_propagate_;
std::vector<std::vector<ConstraintIndex>> variable_watchers_;
gtl::ITIVector<ConstraintIndex, bool> constraint_is_finished_;
gtl::ITIVector<ConstraintIndex, bool> constraint_is_registered_;
};
// We only add to the propagation queue variable that are fully encoded.
// Note that if a variable was already added once, we never add it again.
void FullEncodingFixedPointComputer::ComputeFixedPoint() {
const int num_constraints = model_proto_.constraints_size();
constraint_is_registered_.assign(num_constraints, false);
constraint_is_finished_.assign(num_constraints, false);
for (ConstraintIndex ct_index(0); ct_index < num_constraints; ++ct_index) {
PropagateFullEncoding(ct_index);
}
// Make sure all fully encoded variables of interest are in the queue.
for (int v = 0; v < variable_watchers_.size(); v++) {
if (!variable_watchers_[v].empty() && IsFullyEncoded(v)) {
AddVariableToPropagationQueue(v);
}
}
// Propagate until no additional variable can be fully encoded.
while (!variables_to_propagate_.empty()) {
const int variable = variables_to_propagate_.back();
variables_to_propagate_.pop_back();
for (const ConstraintIndex ct_index : variable_watchers_[variable]) {
if (constraint_is_finished_[ct_index]) continue;
constraint_is_finished_[ct_index] = PropagateFullEncoding(ct_index);
}
}
}
// Returns true if the constraint has finished encoding what it wants.
bool FullEncodingFixedPointComputer::PropagateFullEncoding(
ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
switch (ct.constraint_case()) {
case ConstraintProto::ConstraintProto::kElement:
return PropagateElement(ct_index);
case ConstraintProto::ConstraintProto::kTable:
return PropagateTable(ct_index);
case ConstraintProto::ConstraintProto::kAutomaton:
return PropagateAutomaton(ct_index);
case ConstraintProto::ConstraintProto::kInverse:
return PropagateInverse(ct_index);
case ConstraintProto::ConstraintProto::kLinear:
return PropagateLinear(ct_index);
default:
return true;
}
}
bool FullEncodingFixedPointComputer::PropagateElement(
ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
// Index must always be full encoded.
FullyEncode(ct.element().index());
// If target is a constant or fully encoded, variables must be fully encoded.
const int target = ct.element().target();
if (IsFullyEncoded(target)) {
for (const int v : ct.element().vars()) FullyEncode(v);
}
// If all non-target variables are fully encoded, target must be too.
bool all_variables_are_fully_encoded = true;
for (const int v : ct.element().vars()) {
if (v == target) continue;
if (!IsFullyEncoded(v)) {
all_variables_are_fully_encoded = false;
break;
}
}
if (all_variables_are_fully_encoded) {
if (!IsFullyEncoded(target)) FullyEncode(target);
return true;
}
// If some variables are not fully encoded, register on those.
if (constraint_is_registered_[ct_index]) {
for (const int v : ct.element().vars()) Register(ct_index, v);
Register(ct_index, target);
}
return false;
}
// If a constraint uses its variables in a symbolic (vs. numeric) manner,
// always encode its variables.
bool FullEncodingFixedPointComputer::PropagateTable(ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
if (ct.table().negated()) return true;
for (const int variable : ct.table().vars()) {
FullyEncode(variable);
}
return true;
}
bool FullEncodingFixedPointComputer::PropagateAutomaton(
ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
for (const int variable : ct.automaton().vars()) {
FullyEncode(variable);
}
return true;
}
bool FullEncodingFixedPointComputer::PropagateInverse(
ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
for (const int variable : ct.inverse().f_direct()) {
FullyEncode(variable);
}
for (const int variable : ct.inverse().f_inverse()) {
FullyEncode(variable);
}
return true;
}
bool FullEncodingFixedPointComputer::PropagateLinear(ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
if (parameters_.boolean_encoding_level() == 0) return true;
// Only act when the constraint is an equality.
if (ct.linear().domain(0) != ct.linear().domain(1)) return true;
// If some domain is too large, abort;
if (!constraint_is_registered_[ct_index]) {
for (const int v : ct.linear().vars()) {
const IntegerVariable var = mapping_->Integer(v);
IntegerTrail* integer_trail = model_->GetOrCreate<IntegerTrail>();
const IntegerValue lb = integer_trail->LowerBound(var);
const IntegerValue ub = integer_trail->UpperBound(var);
if (ub - lb > 1024) return true; // Arbitrary limit value.
}
}
if (HasEnforcementLiteral(ct)) {
// Fully encode x in half-reified equality b => x == constant.
const auto& vars = ct.linear().vars();
if (vars.size() == 1) {
FullyEncode(vars.Get(0));
}
return true;
} else {
// If all variables but one are fully encoded,
// force the last one to be fully encoded.
int variable_not_fully_encoded;
int num_fully_encoded = 0;
for (const int var : ct.linear().vars()) {
if (IsFullyEncoded(var)) {
num_fully_encoded++;
} else {
variable_not_fully_encoded = var;
}
}
const int num_vars = ct.linear().vars_size();
if (num_fully_encoded == num_vars - 1) {
FullyEncode(variable_not_fully_encoded);
return true;
}
if (num_fully_encoded == num_vars) return true;
// Register on remaining variables if not already done.
if (!constraint_is_registered_[ct_index]) {
for (const int var : ct.linear().vars()) {
if (!IsFullyEncoded(var)) Register(ct_index, var);
}
}
return false;
}
}
// Makes the std::string fit in one line by cutting it in the middle if
// necessary.
std::string Summarize(const std::string& input) {
@@ -1338,11 +1085,7 @@ void LoadCpModel(const CpModelProto& model_proto,
mapping->ExtractEncoding(model_proto, model);
// Force some variables to be fully encoded.
// This takes some memory, so release it right away.
{
FullEncodingFixedPointComputer fixpoint(model_proto, model);
fixpoint.ComputeFixedPoint();
}
MaybeFullyEncodeMoreVariables(model_proto, model);
// Load the constraints.
std::set<std::string> unsupported_types;
@@ -2438,6 +2181,19 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
params.MergeFrom(flag_params);
model->Add(NewSatParameters(params));
}
// Register SIGINT handler if requested by the parameters.
std::atomic<bool> stopped_boolean(false);
SigintHandler handler;
if (model->GetOrCreate<SatParameters>()->catch_sigint_signal()) {
std::atomic<bool>* stopped =
model->GetOrCreate<TimeLimit>()->ExternalBooleanAsLimit();
if (stopped == nullptr) {
stopped = &stopped_boolean;
model->GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(stopped);
}
handler.Register([stopped]() { *stopped = true; });
}
#endif // __PORTABLE_PLATFORM__
const SatParameters& params = *model->GetOrCreate<SatParameters>();

1
ortools/sat/cp_model_solver.h
View File

@@ -39,7 +39,6 @@ std::string CpSolverResponseStats(const CpSolverResponse& response);
// easy to set custom parameters or interrupt the solver will calls like:
// - model->Add(NewSatParameters(parameters_as_string_or_proto));
// - model->GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(&stop);
// - model->GetOrCreate<SigintHandler>()->Register([&stop]() { stop = true; });
CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model);
// Solves the given cp_model and returns an instance of CpSolverResponse.

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

@@ -15,29 +15,30 @@
The following two sections describe the main
methods for building and solving CP-SAT models.
* [`CpModel`](#ortools.sat.python.cp_model.CpModel): Methods for creating
* [`CpModel`](#cp_model.CpModel): Methods for creating
models, including variables and constraints.
* [`CPSolver`](#ortools.sat.python.cp_model.CpSolver): Methods for solving
* [`CPSolver`](#cp_model.CpSolver): Methods for solving
a model and evaluating solutions.
The following methods implement callbacks that the
solver calls each time it finds a new solution.
* [`CpSolverSolutionCallback`](#cpsolversolutioncallback): A general method for
implementing callbacks.
* [`ObjectiveSolutionPrinter`](#objectivesolutionprinter): Print objective
values and elapsed time for intermediate solutions.
* [`VarArraySolutionPrinter`](#vararraysolutionprinter): Print intermediate
solutions (variable values, time).
* [`VarArrayAndObjectiveSolutionPrinter`](#vararrayandobjectivesolutionprinter):
* [`CpSolverSolutionCallback`](#cp_model.CpSolverSolutionCallback):
A general method for implementing callbacks.
* [`ObjectiveSolutionPrinter`](#cp_model.ObjectiveSolutionPrinter):
Print objective values and elapsed time for intermediate solutions.
* [`VarArraySolutionPrinter`](#cp_model.VarArraySolutionPrinter):
Print intermediate solutions (variable values, time).
* [`VarArrayAndObjectiveSolutionPrinter`]
(#cp_model.VarArrayAndObjectiveSolutionPrinter):
Print both intermediate solutions and objective values.
Additional methods for solving CP-SAT models:
* [`Constraint`](#constraint): A few utility methods for modifying
* [`Constraint`](#cp_model.Constraint): A few utility methods for modifying
contraints created by `CpModel`.
* [`LinearExpr`](#linearexpr): Methods for creating constraints and the
objective from large arrays.
* [`LinearExpr`](#lineacp_model.LinearExpr): Methods for creating constraints
and the objective from large arrays of coefficients.
Other methods and functions listed are primarily used for developing OR-Tools,
rather than for solving specific optimization problems.

7
ortools/sat/sat_parameters.proto
View File

@@ -21,7 +21,7 @@ option java_multiple_files = true;
// Contains the definitions for all the sat algorithm parameters and their
// default values.
//
// NEXT TAG: 135
// NEXT TAG: 136
message SatParameters {
// ==========================================================================
// Branching and polarity
@@ -765,4 +765,9 @@ message SatParameters {
// cannot, we will report MODEL_INVALID if the relative preicision is larger
// than this parameter.
optional double mip_check_precision = 128 [default = 1e-4];
// Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals
// when calling solve. If set, catching the SIGINT signal will terminate the
// search gracefully, as if a time limit was reached.
optional bool catch_sigint_signal = 135 [default = true];
}

33
ortools/sat/swig_helper.h
View File

@@ -21,7 +21,6 @@
#include "ortools/sat/cp_model_solver.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/util/sigint.h"
#include "ortools/util/time_limit.h"
namespace operations_research {
@@ -104,41 +103,23 @@ class SatHelper {
static operations_research::sat::CpSolverResponse Solve(
const operations_research::sat::CpModelProto& model_proto) {
FixFlagsAndEnvironmentForSwig();
Model model;
std::atomic<bool> stopped(false);
model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(&stopped);
model.GetOrCreate<SigintHandler>()->Register(
[&stopped]() { stopped = true; });
return operations_research::sat::SolveCpModel(model_proto, &model);
return operations_research::sat::Solve(model_proto);
}
static operations_research::sat::CpSolverResponse SolveWithParameters(
const operations_research::sat::CpModelProto& model_proto,
const operations_research::sat::SatParameters& parameters) {
FixFlagsAndEnvironmentForSwig();
Model model;
model.Add(NewSatParameters(parameters));
std::atomic<bool> stopped(false);
model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(&stopped);
model.GetOrCreate<SigintHandler>()->Register(
[&stopped]() { stopped = true; });
return SolveCpModel(model_proto, &model);
return operations_research::sat::SolveWithParameters(model_proto,
parameters);
}
static operations_research::sat::CpSolverResponse SolveWithStringParameters(
const operations_research::sat::CpModelProto& model_proto,
const std::string& parameters) {
FixFlagsAndEnvironmentForSwig();
Model model;
model.Add(NewSatParameters(parameters));
std::atomic<bool> stopped(false);
model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(&stopped);
model.GetOrCreate<SigintHandler>()->Register(
[&stopped]() { stopped = true; });
return SolveCpModel(model_proto, &model);
return operations_research::sat::SolveWithParameters(model_proto,
parameters);
}
static operations_research::sat::CpSolverResponse
@@ -153,8 +134,6 @@ class SatHelper {
[&callback](const CpSolverResponse& r) { return callback.Run(r); }));
model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
callback.stopped());
model.GetOrCreate<SigintHandler>()->Register(
[&callback]() { *callback.stopped() = true; });
return SolveCpModel(model_proto, &model);
}
@@ -170,8 +149,6 @@ class SatHelper {
[&callback](const CpSolverResponse& r) { return callback.Run(r); }));
model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
callback.stopped());
model.GetOrCreate<SigintHandler>()->Register(
[&callback]() { *callback.stopped() = true; });
return SolveCpModel(model_proto, &model);
}