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

polish probing code

Browse Source
This commit is contained in:
Laurent Perron
2020-11-19 18:12:18 +01:00
parent f14694250b
commit ad194e85fb
7 changed files with 139 additions and 121 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
ortools/sat/cp_model_search.cc
View File

@@ -342,6 +342,7 @@ std::vector<SatParameters> GetDiverseSetOfParameters(
SatParameters new_params = base_params;
new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
new_params.set_use_probing_search(true);
new_params.set_linearization_level(0);
strategies["probing"] = new_params;
}

8
ortools/sat/cp_model_solver.cc
View File

@@ -1554,11 +1554,13 @@ void SolveLoadedCpModel(const CpModelProto& model_proto,
std::vector<BooleanVariable> bool_vars;
std::vector<IntegerVariable> int_vars;
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
absl::flat_hash_set<BooleanVariable> visited;
for (int v = 0; v < model_proto.variables_size(); ++v) {
if (mapping.IsBoolean(v)) {
const Literal literal = mapping.Literal(v);
if (literal.IsPositive()) {
bool_vars.push_back(literal.Variable());
const BooleanVariable bool_var = mapping.Literal(v).Variable();
if (!visited.contains(bool_var)) {
visited.insert(bool_var);
bool_vars.push_back(bool_var);
}
} else {
IntegerVariable var = mapping.Integer(v);

68
ortools/sat/integer_search.cc
View File

@@ -783,10 +783,9 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
++num_decisions_without_probing >=
sat_parameters.probing_period_at_root()) {
num_decisions_without_probing = 0;
// TODO(user): Be smarter about what variables we probe, we can also
// do more than one.
if (!prober->ClearStatisticsAndResetSearch() ||
!prober->ProbeOneVariable(Literal(decision).Variable())) {
// TODO(user,user): Be smarter about what variables we probe, we can
// also do more than one.
if (!prober->ProbeOneVariable(Literal(decision).Variable())) {
return SatSolver::INFEASIBLE;
}
DCHECK_EQ(sat_solver->CurrentDecisionLevel(), 0);
@@ -936,7 +935,7 @@ SatSolver::Status ContinuousProbing(
int loop = 0;
while (!time_limit->LimitReached()) {
VLOG(1) << "Loop " << loop++;
VLOG(1) << "Probing loop " << loop++;
// Sync the bounds first.
auto SyncBounds = [solver, &level_zero_callbacks]() {
@@ -956,28 +955,39 @@ SatSolver::Status ContinuousProbing(
return SatSolver::INFEASIBLE;
}
// TODO(user): Explore fast probing methods.
// Probe each Boolean variable at most once per loop.
absl::flat_hash_set<BooleanVariable> probed;
// Probe variable bounds.
// TODO(user,user): Probe optional variables.
for (const IntegerVariable int_var : int_vars) {
if (integer_trail->IsFixed(int_var) ||
integer_trail->IsOptional(int_var)) {
continue;
}
IntegerLiteral fix_to_lb = IntegerLiteral::LowerOrEqual(
int_var, integer_trail->LowerBound(int_var));
const Literal shave_lb = encoder->GetOrCreateAssociatedLiteral(fix_to_lb);
if (shave_lb.IsPositive()) {
if (!prober->ClearStatisticsAndResetSearch() ||
!prober->ProbeOneVariable(shave_lb.Variable())) {
const BooleanVariable shave_lb =
encoder
->GetOrCreateAssociatedLiteral(IntegerLiteral::LowerOrEqual(
int_var, integer_trail->LowerBound(int_var)))
.Variable();
if (!probed.contains(shave_lb)) {
probed.insert(shave_lb);
if (!prober->ProbeOneVariable(shave_lb)) {
return SatSolver::INFEASIBLE;
}
}
IntegerLiteral fix_to_ub = IntegerLiteral::GreaterOrEqual(
int_var, integer_trail->UpperBound(int_var));
const Literal shave_ub = encoder->GetOrCreateAssociatedLiteral(fix_to_ub);
if (shave_ub.IsPositive()) {
if (!prober->ClearStatisticsAndResetSearch() ||
!prober->ProbeOneVariable(shave_ub.Variable())) {
const BooleanVariable shave_ub =
encoder
->GetOrCreateAssociatedLiteral(IntegerLiteral::GreaterOrEqual(
int_var, integer_trail->UpperBound(int_var)))
.Variable();
if (!probed.contains(shave_ub)) {
probed.insert(shave_ub);
if (!prober->ProbeOneVariable(shave_ub)) {
return SatSolver::INFEASIBLE;
}
}
@@ -985,25 +995,25 @@ SatSolver::Status ContinuousProbing(
if (!SyncBounds()) {
return SatSolver::INFEASIBLE;
}
if (time_limit->LimitReached()) {
return SatSolver::LIMIT_REACHED;
}
}
// Probe Boolean variables from the model.
int count = 0;
for (const BooleanVariable& bool_var : bool_vars) {
if (!solver->Assignment().LiteralIsAssigned(Literal(bool_var, true))) {
if (!prober->ClearStatisticsAndResetSearch() ||
!prober->ProbeOneVariable(bool_var)) {
return SatSolver::INFEASIBLE;
}
if (solver->Assignment().VariableIsAssigned(bool_var)) continue;
if (time_limit->LimitReached()) {
return SatSolver::LIMIT_REACHED;
}
if (++count > 10) {
count = 0;
if (!SyncBounds()) {
if (!SyncBounds()) {
return SatSolver::INFEASIBLE;
}
if (!probed.contains(bool_var)) {
probed.insert(bool_var);
if (!prober->ProbeOneVariable(bool_var)) {
return SatSolver::INFEASIBLE;
}
if (time_limit->LimitReached()) {
return SatSolver::LIMIT_REACHED;
}
}
}
}

88
ortools/sat/probing.cc
View File

@@ -29,17 +29,13 @@ namespace operations_research {
namespace sat {
Prober::Prober(Model* model)
: model_(model),
trail_(model->GetOrCreate<Trail>()),
: trail_(*model->GetOrCreate<Trail>()),
assignment_(model->GetOrCreate<SatSolver>()->Assignment()),
integer_trail_(model->GetOrCreate<IntegerTrail>()),
implied_bounds_(model->GetOrCreate<ImpliedBounds>()),
sat_solver_(model->GetOrCreate<SatSolver>()),
implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
time_limit_(model->GetOrCreate<TimeLimit>()),
num_new_holes_(0),
num_new_binary_(0),
num_new_integer_bounds_(0),
id_(implication_graph_->PropagatorId()) {}
implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()) {}
bool Prober::ProbeBooleanVariables(const double deterministic_time_limit,
bool log_info) {
@@ -55,26 +51,24 @@ bool Prober::ProbeBooleanVariables(const double deterministic_time_limit,
return ProbeBooleanVariables(deterministic_time_limit, bool_vars, log_info);
}
bool Prober::ProbeOneVariable(BooleanVariable b) {
bool Prober::ProbeOneVariableInternal(BooleanVariable b) {
new_integer_bounds_.clear();
propagated_.SparseClearAll();
for (const Literal decision : {Literal(b, true), Literal(b, false)}) {
if (sat_solver_->Assignment().LiteralIsAssigned(decision)) continue;
if (assignment_.LiteralIsAssigned(decision)) continue;
CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
const int saved_index = trail_->Index();
const int saved_index = trail_.Index();
sat_solver_->EnqueueDecisionAndBackjumpOnConflict(decision);
sat_solver_->AdvanceDeterministicTime(time_limit_);
if (sat_solver_->IsModelUnsat()) return false;
if (sat_solver_->CurrentDecisionLevel() == 0) continue;
if (integer_trail_ != nullptr) {
implied_bounds_->ProcessIntegerTrail(decision);
integer_trail_->AppendNewBounds(&new_integer_bounds_);
}
for (int i = saved_index + 1; i < trail_->Index(); ++i) {
const Literal l = (*trail_)[i];
implied_bounds_->ProcessIntegerTrail(decision);
integer_trail_->AppendNewBounds(&new_integer_bounds_);
for (int i = saved_index + 1; i < trail_.Index(); ++i) {
const Literal l = trail_[i];
// We mark on the first run (b.IsPositive()) and check on the second.
if (decision.IsPositive()) {
@@ -88,7 +82,8 @@ bool Prober::ProbeOneVariable(BooleanVariable b) {
// Anything not propagated by the BinaryImplicationGraph is a "new"
// binary clause. This is becaue the BinaryImplicationGraph has the
// highest priority of all propagators.
if (trail_->AssignmentType(l.Variable()) != id_) {
if (trail_.AssignmentType(l.Variable()) !=
implication_graph_->PropagatorId()) {
new_binary_clauses_.push_back({decision.Negated(), l});
}
}
@@ -176,9 +171,25 @@ bool Prober::ProbeOneVariable(BooleanVariable b) {
}
}
// We might have updates some integer domain, lets propagate.
if (!sat_solver_->FinishPropagation()) return false;
return true;
// We might have updated some integer domain, let's propagate.
return sat_solver_->FinishPropagation();
}
bool Prober::ProbeOneVariable(BooleanVariable b) {
// Reset statistics.
num_new_binary_ = 0;
num_new_holes_ = 0;
num_new_integer_bounds_ = 0;
// Resize the propagated sparse bitset.
const int num_variables = sat_solver_->NumVariables();
propagated_.ClearAndResize(LiteralIndex(2 * num_variables));
// Reset the solver in case it was already used.
sat_solver_->SetAssumptionLevel(0);
if (!sat_solver_->RestoreSolverToAssumptionLevel()) return false;
return ProbeOneVariableInternal(b);
}
bool Prober::ProbeBooleanVariables(const double deterministic_time_limit,
@@ -188,10 +199,18 @@ bool Prober::ProbeBooleanVariables(const double deterministic_time_limit,
WallTimer wall_timer;
wall_timer.Start();
// Reset statistics.
num_new_binary_ = 0;
num_new_holes_ = 0;
num_new_integer_bounds_ = 0;
// Resize the propagated sparse bitset.
const int num_variables = sat_solver_->NumVariables();
propagated_.ClearAndResize(LiteralIndex(2 * num_variables));
// Reset the solver in case it was already used.
if (!ClearStatisticsAndResetSearch()) {
return SatSolver::INFEASIBLE;
}
sat_solver_->SetAssumptionLevel(0);
if (!sat_solver_->RestoreSolverToAssumptionLevel()) return false;
const int initial_num_fixed = sat_solver_->LiteralTrail().Index();
const double initial_deterministic_time =
@@ -217,7 +236,7 @@ bool Prober::ProbeBooleanVariables(const double deterministic_time_limit,
// Propagate b=1 and then b=0.
++num_probed;
if (!ProbeOneVariable(b)) {
if (!ProbeOneVariableInternal(b)) {
return false;
}
}
@@ -247,27 +266,6 @@ bool Prober::ProbeBooleanVariables(const double deterministic_time_limit,
return true;
}
bool Prober::ClearStatisticsAndResetSearch() {
// For the new direct implication detected.
num_new_binary_ = 0;
// This is used to tighten the integer variable bounds.
num_new_holes_ = 0;
num_new_integer_bounds_ = 0;
new_integer_bounds_.clear();
// To detect literal x that must be true because b => x and not(b) => x.
// When probing b, we add all propagated literal to propagated, and when
// probing not(b) we check if any are already there.
const int num_variables = sat_solver_->NumVariables();
propagated_.ClearAndResize(LiteralIndex(2 * num_variables));
sat_solver_->SetAssumptionLevel(0);
if (!sat_solver_->RestoreSolverToAssumptionLevel()) return false;
return true;
}
bool LookForTrivialSatSolution(double deterministic_time_limit, Model* model,
bool log_info) {
log_info |= VLOG_IS_ON(1);

83
ortools/sat/probing.h
View File

@@ -73,30 +73,38 @@ class Prober {
bool ProbeOneVariable(BooleanVariable b);
bool ClearStatisticsAndResetSearch();
private:
Model* model_;
SparseBitset<LiteralIndex> propagated_;
std::vector<IntegerLiteral> new_integer_bounds_;
Trail* trail_;
bool ProbeOneVariableInternal(BooleanVariable b);
// Model owned classes.
const Trail& trail_;
const VariablesAssignment& assignment_;
IntegerTrail* integer_trail_;
ImpliedBounds* implied_bounds_;
SatSolver* sat_solver_;
BinaryImplicationGraph* implication_graph_;
TimeLimit* time_limit_;
BinaryImplicationGraph* implication_graph_;
// To detect literal x that must be true because b => x and not(b) => x.
// When probing b, we add all propagated literal to propagated, and when
// probing not(b) we check if any are already there.
SparseBitset<LiteralIndex> propagated_;
// Modifications found during probing.
std::vector<Literal> to_fix_at_true_;
int num_new_holes_;
int num_new_binary_;
int num_new_integer_bounds_;
std::vector<IntegerLiteral> new_integer_bounds_;
std::vector<std::pair<Literal, Literal>> new_binary_clauses_;
int id_;
// Probing statistics.
int num_new_holes_ = 0;
int num_new_binary_ = 0;
int num_new_integer_bounds_ = 0;
};
// Try to randomly tweak the search and stop at the first conflict each time.
// This can sometimes find feasible solution, but more importantly, it is a
// form of probing that can sometimes find small and interesting conflicts or
// fix variables. This seems to work well on the SAT14/app/rook-* problems and
// This can sometimes find feasible solution, but more importantly, it is a form
// of probing that can sometimes find small and interesting conflicts or fix
// variables. This seems to work well on the SAT14/app/rook-* problems and
// do fix more variables if run before probing.
//
// If a feasible SAT solution is found (i.e. all Boolean assigned), then this
@@ -116,20 +124,19 @@ struct ProbingOptions {
// else can be deduced and everything has been probed until fix-point. The
// fix point depend on the extract_binay_clauses option:
// - If false, we will just stop when no more failed literal can be found.
// - If true, we will do more work and stop when all failed literal have
// been
// - If true, we will do more work and stop when all failed literal have been
// found and all hyper binary resolution have been performed.
//
// TODO(user): We can also provide a middle ground and probe all failed
// literal but do not extract all binary clauses.
//
// Note that the fix-point is unique, modulo the equivalent literal
// detection we do. And if we add binary clauses, modulo the transitive
// reduction of the binary implication graph.
// Note that the fix-point is unique, modulo the equivalent literal detection
// we do. And if we add binary clauses, modulo the transitive reduction of the
// binary implication graph.
//
// To be fast, we only use the binary clauses in the binary implication
// graph for the equivalence detection. So the power of the equivalence
// detection changes if the extract_binay_clauses option is true or not.
// To be fast, we only use the binary clauses in the binary implication graph
// for the equivalence detection. So the power of the equivalence detection
// changes if the extract_binay_clauses option is true or not.
//
// TODO(user): The fix point is not yet reached since we don't currently
// simplify non-binary clauses with these equivalence, but we will.
@@ -144,24 +151,22 @@ struct ProbingOptions {
// With these extra clause the power of the equivalence literal detection
// using only the binary implication graph with increase. Note that it is
// possible to do exactly the same thing without adding these binary clause
// first. This is what is done by yet another probing algorithm (currently
// in simplification.cc).
// first. This is what is done by yet another probing algorithm (currently in
// simplification.cc).
//
// TODO(user): Note that adding binary clause before/during the SAT presolve
// is currently not always a good idea. This is because we don't simplify
// the other clause as much as we could. Also, there can be up to a
// quadratic number of clauses added this way, which might slow down things
// a lot. But then because of the deterministic limit, we usually cannot add
// too much clauses, even for huge problems, since we will reach the limit
// before that.
// is currently not always a good idea. This is because we don't simplify the
// other clause as much as we could. Also, there can be up to a quadratic
// number of clauses added this way, which might slow down things a lot. But
// then because of the deterministic limit, we usually cannot add too much
// clauses, even for huge problems, since we will reach the limit before that.
bool extract_binary_clauses = false;
// Use a version of the "Tree look" algorithm as explained in the paper
// above. This is usually faster and more efficient. Note that when
// extracting binary clauses it might currently produce more "redundant" one
// in the sense that a transitive reduction of the binary implication graph
// after all hyper binary resolution have been performed may need to do more
// work.
// Use a version of the "Tree look" algorithm as explained in the paper above.
// This is usually faster and more efficient. Note that when extracting binary
// clauses it might currently produce more "redundant" one in the sense that a
// transitive reduction of the binary implication graph after all hyper binary
// resolution have been performed may need to do more work.
bool use_tree_look = true;
// There is two sligthly different implementation of the tree-look algo.
@@ -171,9 +176,9 @@ struct ProbingOptions {
bool use_queue = true;
// If we detect as we probe that a new binary clause subsumes one of the
// non-binary clause, we will replace the long clause by the binary one.
// This is orthogonal to the extract_binary_clauses parameters which will
// add all binary clauses but not neceassirly check for subsumption.
// non-binary clause, we will replace the long clause by the binary one. This
// is orthogonal to the extract_binary_clauses parameters which will add all
// binary clauses but not neceassirly check for subsumption.
bool subsume_with_binary_clause = true;
// We assume this is also true if --v 1 is activated.

2
ortools/sat/sat_parameters.proto
View File

@@ -756,7 +756,7 @@ message SatParameters {
// every root node.
optional int64 probing_period_at_root = 142 [default = 0];
// If true, this worker will continuously probe Boolean variables, and integer
// If true, search will continuously probe Boolean variables, and integer
// variable bounds.
optional bool use_probing_search = 176 [default = false];

10
ortools/sat/synchronization.cc
View File

@@ -593,10 +593,12 @@ void SharedBoundsManager::ReportPotentialNewBounds(
changed_variables_since_last_synchronize_.Set(var);
num_improvements++;
}
// TODO(user): remove LOG_IF and display number of bound improvements
// propagated per workers.
VLOG_IF(2, num_improvements > 0)
<< worker_name << " exports " << num_improvements << " modifications";
// TODO(user): Display number of bound improvements cumulatively per
// workers at the end of the search.
if (num_improvements > 0) {
VLOG(2) << worker_name << " exports " << num_improvements
<< " modifications";
}
}
void SharedBoundsManager::Synchronize() {