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

more work // flatzinc-sat; merge random utils in SAT/BOP

Browse Source
This commit is contained in:
Laurent Perron
2018-06-21 13:54:27 +02:00
parent 8bc9b15959
commit 9aaf972989
18 changed files with 279 additions and 241 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
makefiles/Makefile.gen.mk
View File

@@ -1829,8 +1829,10 @@ $(SRC_DIR)/ortools/sat/integer.h: \
$(SRC_DIR)/ortools/util/sorted_interval_list.h
$(SRC_DIR)/ortools/sat/integer_search.h: \
$(SRC_DIR)/ortools/base/random.h \
$(SRC_DIR)/ortools/sat/integer.h \
$(SRC_DIR)/ortools/sat/sat_solver.h
$(SRC_DIR)/ortools/sat/sat_solver.h \
$(SRC_DIR)/ortools/util/random_engine.h
$(SRC_DIR)/ortools/sat/intervals.h: \
$(SRC_DIR)/ortools/base/integral_types.h \
@@ -2133,8 +2135,7 @@ $(OBJ_DIR)/sat/cp_model_presolve.$O: \
$(OBJ_DIR)/sat/cp_model_search.$O: \
$(SRC_DIR)/ortools/sat/cp_model_search.cc \
$(SRC_DIR)/ortools/sat/cp_model_search.h \
$(SRC_DIR)/ortools/sat/cp_model_utils.h \
$(SRC_DIR)/ortools/util/random_engine.h
$(SRC_DIR)/ortools/sat/cp_model_utils.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Scp_model_search.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Scp_model_search.$O
$(OBJ_DIR)/sat/cp_model_solver.$O: \
@@ -2267,7 +2268,8 @@ $(OBJ_DIR)/sat/integer_search.$O: \
$(SRC_DIR)/ortools/sat/integer_search.cc \
$(SRC_DIR)/ortools/sat/integer_search.h \
$(SRC_DIR)/ortools/sat/linear_programming_constraint.h \
$(SRC_DIR)/ortools/sat/sat_decision.h
$(SRC_DIR)/ortools/sat/sat_decision.h \
$(SRC_DIR)/ortools/sat/util.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Sinteger_search.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sinteger_search.$O
$(OBJ_DIR)/sat/intervals.$O: \

5
ortools/bop/bop_fs.cc
View File

@@ -212,8 +212,7 @@ BopRandomFirstSolutionGenerator::BopRandomFirstSolutionGenerator(
sat::SatSolver* sat_propagator, MTRandom* random)
: BopOptimizerBase(name),
random_(random),
sat_propagator_(sat_propagator),
sat_seed_(parameters.random_seed()) {}
sat_propagator_(sat_propagator) {}
BopRandomFirstSolutionGenerator::~BopRandomFirstSolutionGenerator() {}
@@ -249,14 +248,12 @@ BopOptimizerBase::Status BopRandomFirstSolutionGenerator::Optimize(
bool solution_found = false;
while (remaining_num_conflicts > 0 && !time_limit->LimitReached()) {
++sat_seed_;
sat_propagator_->Backtrack(0);
old_num_failures = sat_propagator_->num_failures();
sat::SatParameters sat_params = saved_params;
sat::RandomizeDecisionHeuristic(random_, &sat_params);
sat_params.set_max_number_of_conflicts(kMaxNumConflicts);
sat_params.set_random_seed(sat_seed_);
sat_propagator_->SetParameters(sat_params);
sat_propagator_->ResetDecisionHeuristic();

1
ortools/bop/bop_fs.h
View File

@@ -100,7 +100,6 @@ class BopRandomFirstSolutionGenerator : public BopOptimizerBase {
int random_seed_;
MTRandom* random_;
sat::SatSolver* sat_propagator_;
uint32 sat_seed_;
};
// This class computes the linear relaxation of the state problem.

6
ortools/bop/bop_parameters.proto
View File

@@ -108,7 +108,11 @@ message BopParameters {
optional bool use_random_lns = 6 [default = true];
// The seed used to initialize the random generator.
optional int32 random_seed = 7 [default = 0];
//
// TODO(user): Some of our client test fail depending on this value! we need
// to fix them and ideally randomize our behavior from on test to the next so
// that this doesn't happen in the future.
optional int32 random_seed = 7 [default = 8];
// Number of variables to relax in the exhaustive Large Neighborhood Search.
optional int32 num_relaxed_vars = 8 [default = 10];

284
ortools/flatzinc/cp_model_fz_solver.cc
View File

@@ -26,6 +26,7 @@
#include "ortools/base/timer.h"
#include "ortools/flatzinc/checker.h"
#include "ortools/flatzinc/logging.h"
#include "ortools/port/proto_utils.h"
#include "ortools/sat/cp_constraints.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
@@ -926,6 +927,74 @@ CpSolverResponse WorkerSearch(
return response;
}
bool MergeOptimizationSolution(const CpSolverResponse& response, bool maximize,
CpSolverResponse* best) {
switch (response.status()) {
case CpSolverStatus::MODEL_SAT: {
const bool is_improving =
maximize ? response.objective_value() > best->objective_value()
: response.objective_value() < best->objective_value();
const double current_best_bound = response.best_objective_bound();
const double previous_best_bound = best->best_objective_bound();
const double new_best_objective_bound =
maximize ? std::min(previous_best_bound, current_best_bound)
: std::max(previous_best_bound, current_best_bound);
// TODO(user): return OPTIMAL if objective is tight.
if (is_improving) {
// Overwrite solution and fix best_objective_bound.
*best = response;
best->set_best_objective_bound(new_best_objective_bound);
return true;
}
// Maybe we can always improve best_objective_bound.
best->set_best_objective_bound(new_best_objective_bound);
return false;
}
case CpSolverStatus::MODEL_UNSAT: {
if (best->status() == CpSolverStatus::UNKNOWN ||
best->status() == CpSolverStatus::MODEL_UNSAT) {
// Stores the unsat solution.
*best = response;
return true;
} else {
// It can happen that the LNS finds the best solution, but does
// not prove it. Then another worker pulls in the best solution,
// does not improve upon it, returns UNSAT if it has not found a
// previous solution, or OPTIMAL with a bad objective value, and
// stops all other workers. In that case, if the last solution
// found has a MODEL_SAT status, it is indeed optimal, and
// should be marked as thus.
FZVLOG << "Fixing best known solution to optimal." << FZENDL;
best->set_status(CpSolverStatus::OPTIMAL);
best->set_best_objective_bound(best->objective_value());
return false;
}
break;
}
case CpSolverStatus::OPTIMAL: {
const double previous = best->objective_value();
const double current = response.objective_value();
if ((maximize && current >= previous) ||
(!maximize && current <= previous)) {
// We always overwrite the best solution with an at-least as good
// optimal solution.
*best = response;
return true;
} else {
// We are in the same case as the MODEL_UNSAT above. Solution
// synchronization has forced the solver to exit with a sub-optimal
// solution, believing it was optimal.
FZVLOG << "Fixing best known solution to optimal." << FZENDL;
best->set_status(CpSolverStatus::OPTIMAL);
best->set_best_objective_bound(best->objective_value());
return false;
}
break;
}
default: { return false; }
}
}
} // namespace
void SolveFzWithCpModelProto(const fz::Model& fz_model,
@@ -1035,8 +1104,18 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
const int num_search_workers = std::max(1, p.threads);
bool stopped = false;
std::vector<CpSolverResponse> responses(num_search_workers);
int last_worker_id = -1;
CpSolverResponse best_response;
if (fz_model.objective() != nullptr) {
const double kInfinity = std::numeric_limits<double>::infinity();
if (fz_model.maximize()) {
best_response.set_objective_value(-kInfinity);
best_response.set_best_objective_bound(kInfinity);
} else {
best_response.set_objective_value(kInfinity);
best_response.set_best_objective_bound(-kInfinity);
}
}
int solution_count = 1; // Start at 1 as in the sat solver output.
// Solve the problem.
@@ -1052,18 +1131,17 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
const SatParameters local_params =
DiversifySearchParameters(worker_id, m.parameters, m.proto, 0);
pool.Schedule([&fz_model, &m, &p, &stopped, local_params, worker_id,
&responses, &last_worker_id, &mutex]() {
responses[worker_id] =
&best_response, &mutex]() {
const CpSolverResponse local_response =
WorkerSearch(m.proto, local_params, p, nullptr, nullptr, nullptr,
worker_id, &stopped);
absl::MutexLock lock(&mutex);
if (responses[worker_id].status() == CpSolverStatus::MODEL_SAT ||
responses[worker_id].status() == CpSolverStatus::MODEL_UNSAT) {
last_worker_id = worker_id;
if (best_response.status() == CpSolverStatus::UNKNOWN) {
best_response = local_response;
}
if (local_response.status() != CpSolverStatus::UNKNOWN) {
CHECK_EQ(local_response.status(), best_response.status());
stopped = true;
} else if (last_worker_id == -1) {
// Puts a default value.
last_worker_id = worker_id;
}
});
}
@@ -1083,24 +1161,11 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
FZLOG << "Starting parallel search with " << num_search_workers
<< " workers" << FZENDL;
}
CpSolverResponse best_response;
bool suspicious_termination = false;
{
ThreadPool pool("Parallel_FlatZinc_sat", num_active_threads);
pool.StartWorkers();
for (int worker_id = 0; worker_id < num_active_threads; ++worker_id) {
const auto is_improving = [&best_response,
maximize](const CpSolverResponse& r) {
return (best_response.status() == CpSolverStatus::MODEL_SAT ||
best_response.status() == CpSolverStatus::OPTIMAL)
? (maximize ? r.objective_value() >
best_response.objective_value()
: r.objective_value() <
best_response.objective_value())
: true;
};
const auto solution_synchronization = [&mutex, &best_response]() {
absl::MutexLock lock(&mutex);
return best_response;
@@ -1116,25 +1181,28 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
};
const auto solution_observer = [maximize, &solution_count, worker_id,
&mutex, &p, &fz_model, &last_worker_id,
&m, &best_response, is_improving,
&mutex, &p, &fz_model, &m,
&best_response,
&timer](const CpSolverResponse& r) {
absl::MutexLock lock(&mutex);
// Check is the new solution is actually improving upon the best
// solution found so far.
if (is_improving(r)) {
best_response = r;
last_worker_id = worker_id;
FZLOG << "worker #" << worker_id << ", solution #"
<< solution_count++ << ", objective = " << r.objective_value()
<< ", time = " << timer.Get() << "s" << FZENDL;
if (FLAGS_use_flatzinc_format && p.all_solutions) {
const std::string solution_string =
SolutionString(fz_model, [&m, &r](fz::IntegerVariable* v) {
return r.solution(gtl::FindOrDie(m.fz_var_to_index, v));
});
std::cout << solution_string << std::endl;
if (MergeOptimizationSolution(r, maximize, &best_response)) {
if (p.all_solutions) {
FZLOG << "worker #" << worker_id << ", solution #"
<< solution_count++
<< ", objective = " << best_response.objective_value()
<< ", objective " << (maximize ? "upper" : "lower")
<< " bound = " << best_response.best_objective_bound()
<< ", time = " << timer.Get() << "s" << FZENDL;
if (FLAGS_use_flatzinc_format) {
const std::string solution_string =
SolutionString(fz_model, [&m, &r](fz::IntegerVariable* v) {
return r.solution(gtl::FindOrDie(m.fz_var_to_index, v));
});
std::cout << solution_string << std::endl;
}
}
}
};
@@ -1145,10 +1213,9 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
pool.Schedule([&fz_model, &m, &p, solution_observer,
solution_synchronization, objective_synchronization,
&stopped, local_params, worker_id, &mutex, &responses,
&last_worker_id, is_improving, &best_response, maximize,
&suspicious_termination]() {
responses[worker_id] =
&stopped, local_params, worker_id, &mutex,
&best_response, maximize]() {
const CpSolverResponse local_response =
WorkerSearch(m.proto, local_params, p, solution_observer,
solution_synchronization, objective_synchronization,
worker_id, &stopped);
@@ -1156,88 +1223,36 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
// Process final solution. Decide which worker has the 'best'
// solution. Note that the solution observer may or may not have been
// called.
//
// TODO(user): If the solution is SAT, we can pull the best lower
// bound.
absl::MutexLock lock(&mutex);
FZVLOG << "Worker " << worker_id << " terminates with status "
<< responses[worker_id].status()
<< ProtoEnumToString<CpSolverStatus>(local_response.status())
<< " and an objective value of "
<< responses[worker_id].objective_value() << FZENDL;
switch (responses[worker_id].status()) {
case CpSolverStatus::MODEL_SAT: {
if (is_improving(responses[worker_id])) {
last_worker_id = worker_id;
best_response = responses[worker_id];
}
break;
}
case CpSolverStatus::MODEL_UNSAT: {
if (best_response.status() != CpSolverStatus::MODEL_SAT &&
best_response.status() != CpSolverStatus::OPTIMAL) {
// Overwrite any previous worker.
last_worker_id = worker_id;
// Stores the unsat solution.
best_response = responses[worker_id];
} else {
suspicious_termination = true;
}
// Stops all other workers.
stopped = true;
break;
}
case CpSolverStatus::OPTIMAL: {
const double previous =
(best_response.status() == CpSolverStatus::MODEL_SAT ||
best_response.status() == CpSolverStatus::OPTIMAL)
? best_response.objective_value()
: (maximize ? kint64min : kint64max);
const double current = responses[worker_id].objective_value();
if ((maximize && current >= previous) ||
(!maximize && current <= previous)) {
// Overwrite any previous worker.
last_worker_id = worker_id;
// Stops all other workers.
stopped = true;
// Stores the best solution.
best_response = responses[worker_id];
} else {
suspicious_termination = true;
// Stops all other workers.
stopped = true;
}
break;
}
default: {
if (last_worker_id == -1) {
last_worker_id = worker_id;
}
}
<< local_response.objective_value() << FZENDL;
MergeOptimizationSolution(local_response, maximize, &best_response);
if (best_response.status() == CpSolverStatus::OPTIMAL ||
best_response.status() == CpSolverStatus::MODEL_UNSAT) {
stopped = true;
}
});
}
}
// It can happen that the LNS finds the best solution, but does not prove
// it. Then another worker pulls in the best solution, does not improve
// upon it, returns UNSAT if it has not found a previous solution, or
// OPTIMAL with a bad objective value, and stops all other workers. In that
// case, if the last solution found has a MODEL_SAT status, it is indeed
// optimal, and should be marked as thus.
if (last_worker_id != -1 &&
responses[last_worker_id].status() == CpSolverStatus::MODEL_SAT &&
suspicious_termination) {
FZVLOG << "Fixing best known solution to optimal." << FZENDL;
responses[last_worker_id].set_status(CpSolverStatus::OPTIMAL);
responses[last_worker_id].set_best_objective_bound(
responses[last_worker_id].objective_value());
}
// TODO(user): If the solution is SAT, we can pull the best lower bound.
// Fix wall time.
best_response.set_wall_time(timer.Get());
} else if (p.all_solutions) { // Sequential case with observer.
auto solution_observer = [&fz_model, &solution_count, &m,
const bool maximize = fz_model.maximize();
auto solution_observer = [&fz_model, &solution_count, &m, maximize,
&timer](const CpSolverResponse& r) {
if (fz_model.objective() == nullptr) {
FZLOG << "solution #" << solution_count++ << ", time = " << timer.Get()
<< " s" << FZENDL;
} else {
FZLOG << "solution #" << solution_count++
<< ", objective = " << r.objective_value()
<< ", objective = " << r.objective_value() << ", objective "
<< (maximize ? "upper" : "lower")
<< " bound = " << r.best_objective_bound()
<< ", time = " << timer.Get() << " s" << FZENDL;
}
if (FLAGS_use_flatzinc_format) {
@@ -1248,60 +1263,47 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
std::cout << solution_string << std::endl;
}
};
responses[0] = WorkerSearch(m.proto, m.parameters, p, solution_observer,
nullptr, nullptr, 0, &stopped);
last_worker_id = 0;
best_response = WorkerSearch(m.proto, m.parameters, p, solution_observer,
nullptr, nullptr, 0, &stopped);
} else { // Sequential case, no observer.
responses[0] = WorkerSearch(m.proto, m.parameters, p, nullptr, nullptr,
nullptr, 0, &stopped);
last_worker_id = 0;
}
for (int i = 0; i < num_search_workers; ++i) {
if (responses[i].status() != CpSolverStatus::UNKNOWN) {
FZLOG << "Worker " << i << ": " << responses[i].status() << FZENDL;
}
}
CHECK_NE(last_worker_id, -1);
if (num_search_workers > 1) {
FZLOG << "Final solution found by worker " << last_worker_id << FZENDL;
best_response = WorkerSearch(m.proto, m.parameters, p, nullptr, nullptr,
nullptr, 0, &stopped);
}
// Check the returned solution with the fz model checker.
const CpSolverResponse& response = responses[last_worker_id];
if (response.status() == CpSolverStatus::MODEL_SAT ||
response.status() == CpSolverStatus::OPTIMAL) {
CHECK(CheckSolution(fz_model, [&response, &m](fz::IntegerVariable* v) {
return response.solution(gtl::FindOrDie(m.fz_var_to_index, v));
if (best_response.status() == CpSolverStatus::MODEL_SAT ||
best_response.status() == CpSolverStatus::OPTIMAL) {
CHECK(CheckSolution(fz_model, [&best_response, &m](fz::IntegerVariable* v) {
return best_response.solution(gtl::FindOrDie(m.fz_var_to_index, v));
}));
}
// Output the solution if the flatzinc official format.
if (FLAGS_use_flatzinc_format) {
if (response.status() == CpSolverStatus::MODEL_SAT ||
response.status() == CpSolverStatus::OPTIMAL) {
if (best_response.status() == CpSolverStatus::MODEL_SAT ||
best_response.status() == CpSolverStatus::OPTIMAL) {
if (!p.all_solutions) { // Already printed otherwise.
const std::string solution_string =
SolutionString(fz_model, [&response, &m](fz::IntegerVariable* v) {
return response.solution(gtl::FindOrDie(m.fz_var_to_index, v));
const std::string solution_string = SolutionString(
fz_model, [&best_response, &m](fz::IntegerVariable* v) {
return best_response.solution(
gtl::FindOrDie(m.fz_var_to_index, v));
});
std::cout << solution_string << std::endl;
}
if (response.status() == CpSolverStatus::OPTIMAL ||
response.all_solutions_were_found()) {
if (best_response.status() == CpSolverStatus::OPTIMAL ||
best_response.all_solutions_were_found()) {
std::cout << "==========" << std::endl;
}
} else if (response.status() == CpSolverStatus::MODEL_UNSAT) {
} else if (best_response.status() == CpSolverStatus::MODEL_UNSAT) {
std::cout << "=====UNSATISFIABLE=====" << std::endl;
} else {
std::cout << "%% TIMEOUT" << std::endl;
}
if (p.statistics) {
LogInFlatzincFormat(CpSolverResponseStats(response));
LogInFlatzincFormat(CpSolverResponseStats(best_response));
}
} else {
LOG(INFO) << CpSolverResponseStats(response);
LOG(INFO) << CpSolverResponseStats(best_response);
}
}

21
ortools/sat/cp_model_search.cc
View File

@@ -17,7 +17,7 @@
#include <unordered_map>
#include "ortools/sat/cp_model_utils.h"
#include "ortools/util/random_engine.h"
#include "ortools/sat/util.h"
namespace operations_research {
namespace sat {
@@ -38,12 +38,6 @@ struct VarValue {
IntegerValue value;
};
// Thin wrapper around a random_engine. This helps store a random engine
// inside a Model as template programming messes up compilation.
struct SearchStrategyRandomGenerator {
random_engine_t rand;
};
const std::function<LiteralIndex()> ConstructSearchStrategyInternal(
const std::unordered_map<int, std::pair<int64, int64>>&
var_to_coeff_offset_pair,
@@ -134,16 +128,9 @@ const std::function<LiteralIndex()> ConstructSearchStrategyInternal(
active_vars.erase(std::remove_if(active_vars.begin(), active_vars.end(),
is_above_tolerance),
active_vars.end());
// TODO(user): Move this to its own method.
const bool seeded =
model->Get<SearchStrategyRandomGenerator>() != nullptr;
SearchStrategyRandomGenerator* const rw =
model->GetOrCreate<SearchStrategyRandomGenerator>();
if (!seeded) {
rw->rand.seed(parameters->random_seed());
}
const int winner = std::uniform_int_distribution<int>(
0, active_vars.size() - 1)(rw->rand);
const int winner =
std::uniform_int_distribution<int>(0, active_vars.size() - 1)(
*model->GetOrCreate<ModelRandomGenerator>());
candidate = active_vars[winner].var;
candidate_lb = integer_trail->LowerBound(candidate);
candidate_ub = integer_trail->UpperBound(candidate);

7
ortools/sat/cp_model_solver.cc
View File

@@ -2243,6 +2243,10 @@ std::function<SatParameters(Model*)> NewSatParameters(
std::function<SatParameters(Model*)> NewSatParameters(
const sat::SatParameters& parameters) {
return [=](Model* model) {
// Tricky: It is important to initialize the model parameters before any
// of the solver object are created, so that by default they use the given
// parameters.
*model->GetOrCreate<SatParameters>() = parameters;
model->GetOrCreate<SatSolver>()->SetParameters(parameters);
return parameters;
};
@@ -2536,6 +2540,9 @@ CpSolverResponse SolveCpModelInternal(
m.Integer(model_proto.objective().vars(i))));
}
response.set_objective_value(ScaleObjectiveValue(obj, objective_value));
const IntegerTrail* integer_trail = sat_model.Get<IntegerTrail>();
response.set_best_objective_bound(ScaleObjectiveValue(
obj, integer_trail->LevelZeroBound(objective_var).value()));
external_solution_observer(response);
VLOG(1) << "Solution #" << num_solutions
<< " obj:" << response.objective_value()

4
ortools/sat/cp_model_solver.h
View File

@@ -62,8 +62,8 @@ std::function<void(Model*)> NewFeasibleSolutionObserver(
void SetSynchronizationFunction(std::function<CpSolverResponse()> f,
Model* model);
// wait until this function returns with the current "best" information about
// the objective value of the current best solution.
// Wait until this function returns with the objective value of the current
// best solution.
void SetObjectiveSynchronizationFunction(std::function<double()> f,
Model* model);

14
ortools/sat/integer.h
View File

@@ -609,6 +609,13 @@ class IntegerTrail : public SatPropagator {
return false;
}
// Returns a lower bound on the given var that will always be valid.
IntegerValue LevelZeroBound(IntegerVariable var) const {
// The level zero bounds are stored at the beginning of the trail and they
// also serves as sentinels. Their index match the variables index.
return integer_trail_[var.value()].bound;
}
// Returns true if the variable lower bound is still the one from level zero.
bool VariableLowerBoundIsFromLevelZero(IntegerVariable var) const {
return vars_[var].current_trail_index < vars_.size();
@@ -638,13 +645,6 @@ class IntegerTrail : public SatPropagator {
absl::Span<IntegerLiteral> integer_reason,
BooleanVariable* variable_with_same_reason);
// Returns a lower bound on the given var that will always be valid.
IntegerValue LevelZeroBound(IntegerVariable var) const {
// The level zero bounds are stored at the beginning of the trail and they
// also serves as sentinels. Their index match the variables index.
return integer_trail_[var.value()].bound;
}
// Returns the lowest trail index of a TrailEntry that can be used to explain
// the given IntegerLiteral. The literal must be currently true (CHECKed).
// Returns -1 if the explanation is trivial.

46
ortools/sat/integer_search.cc
View File

@@ -17,6 +17,7 @@
#include "ortools/sat/linear_programming_constraint.h"
#include "ortools/sat/sat_decision.h"
#include "ortools/sat/util.h"
namespace operations_research {
namespace sat {
@@ -91,6 +92,23 @@ std::function<LiteralIndex()> SatSolverHeuristic(Model* model) {
};
}
std::function<LiteralIndex()> RandomizeOnRestartSatSolverHeuristic(
Model* model) {
SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
Trail* trail = model->GetOrCreate<Trail>();
SatDecisionPolicy* decision_policy = model->GetOrCreate<SatDecisionPolicy>();
return [sat_solver, trail, decision_policy, model] {
if (sat_solver->CurrentDecisionLevel() == 0) {
RandomizeDecisionHeuristic(model->GetOrCreate<ModelRandomGenerator>(),
model->GetOrCreate<SatParameters>());
decision_policy->ResetDecisionHeuristic();
}
const bool all_assigned = trail->Index() == sat_solver->NumVariables();
return all_assigned ? kNoLiteralIndex
: decision_policy->NextBranch().Index();
};
}
std::function<LiteralIndex()> FollowHint(
const std::vector<BooleanOrIntegerVariable>& vars,
const std::vector<IntegerValue>& values, Model* model) {
@@ -270,16 +288,18 @@ SatSolver::Status SolveIntegerProblemWithLazyEncoding(
const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
switch (parameters.search_branching()) {
case SatParameters::AUTOMATIC_SEARCH: {
std::function<LiteralIndex()> search;
if (parameters.randomize_search()) {
search = SequentialSearch(
{RandomizeOnRestartSatSolverHeuristic(model), next_decision});
} else {
search = SequentialSearch({SatSolverHeuristic(model), next_decision});
}
if (parameters.exploit_integer_lp_solution()) {
return SolveProblemWithPortfolioSearch(
{ExploitIntegerLpSolution(
SequentialSearch({SatSolverHeuristic(model), next_decision}),
model)},
{SatSolverRestartPolicy(model)}, model);
search = ExploitIntegerLpSolution(search, model);
}
return SolveProblemWithPortfolioSearch(
{SequentialSearch({SatSolverHeuristic(model), next_decision})},
{SatSolverRestartPolicy(model)}, model);
{search}, {SatSolverRestartPolicy(model)}, model);
}
case SatParameters::FIXED_SEARCH: {
// Not all Boolean might appear in next_decision(), so once there is no
@@ -361,6 +381,13 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
if (num_policies == 0) return SatSolver::MODEL_SAT;
CHECK_EQ(num_policies, restart_policies.size());
SatSolver* const solver = model->GetOrCreate<SatSolver>();
const SatParameters* const params = model->Get<SatParameters>();
const bool use_core = params != nullptr && params->optimize_with_core();
const ObjectiveSynchronizationHelper* helper =
model->Get<ObjectiveSynchronizationHelper>();
const bool synchronize_objective =
!use_core && helper != nullptr && helper->get_external_bound != nullptr &&
helper->objective_var != kNoIntegerVariable;
// Note that it is important to do the level-zero propagation if it wasn't
// already done because EnqueueDecisionAndBackjumpOnConflict() assumes that
@@ -385,10 +412,7 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
// Check external objective, and restart if a better one is supplied.
// TODO(user): Maybe do not check this at each decision.
const ObjectiveSynchronizationHelper* helper =
model->Get<ObjectiveSynchronizationHelper>();
if (helper != nullptr && helper->get_external_bound != nullptr &&
helper->objective_var != kNoIntegerVariable) {
if (synchronize_objective) {
const double external_bound = helper->get_external_bound();
if (std::isfinite(external_bound)) {
IntegerValue best_bound(helper->UnscaledObjective(external_bound));

19
ortools/sat/sat_decision.cc
View File

@@ -13,14 +13,15 @@
#include "ortools/sat/sat_decision.h"
#include "ortools/sat/util.h"
namespace operations_research {
namespace sat {
SatDecisionPolicy::SatDecisionPolicy(Model* model)
: parameters_(*(model->GetOrCreate<SatParameters>())),
trail_(model->GetOrCreate<Trail>()) {
random_.seed(parameters_.random_seed());
}
trail_(model->GetOrCreate<Trail>()),
random_(model->GetOrCreate<ModelRandomGenerator>()) {}
void SatDecisionPolicy::IncreaseNumVariables(int num_variables) {
const int old_num_variables = activities_.size();
@@ -47,8 +48,6 @@ void SatDecisionPolicy::IncreaseNumVariables(int num_variables) {
}
void SatDecisionPolicy::ResetDecisionHeuristic() {
random_.seed(parameters_.random_seed());
const int num_variables = activities_.size();
variable_activity_increment_ = 1.0;
activities_.assign(num_variables, parameters_.initial_variables_activity());
@@ -83,7 +82,7 @@ void SatDecisionPolicy::ResetInitialPolarity(int from) {
var_polarity_[var] = false;
break;
case SatParameters::POLARITY_RANDOM:
var_polarity_[var] = std::uniform_int_distribution<int>(0, 1)(random_);
var_polarity_[var] = std::uniform_int_distribution<int>(0, 1)(*random_);
break;
case SatParameters::POLARITY_WEIGHTED_SIGN:
var_polarity_[var] = weighted_sign_[var] > 0;
@@ -130,7 +129,7 @@ void SatDecisionPolicy::InitializeVariableOrdering() {
std::reverse(variables.begin(), variables.end());
break;
case SatParameters::IN_RANDOM_ORDER:
std::shuffle(variables.begin(), variables.end(), random_);
std::shuffle(variables.begin(), variables.end(), *random_);
break;
}
@@ -243,7 +242,7 @@ Literal SatDecisionPolicy::NextBranch() {
BooleanVariable var;
const double ratio = parameters_.random_branches_ratio();
auto zero_to_one = [this]() {
return std::uniform_real_distribution<double>()(random_);
return std::uniform_real_distribution<double>()(*random_);
};
if (ratio != 0.0 && zero_to_one() < ratio) {
while (true) {
@@ -251,7 +250,7 @@ Literal SatDecisionPolicy::NextBranch() {
// variables are assigned.
std::uniform_int_distribution<int> index_dist(0,
var_ordering_.Size() - 1);
var = var_ordering_.QueueElement(index_dist(random_)).var;
var = var_ordering_.QueueElement(index_dist(*random_)).var;
if (!trail_->Assignment().VariableIsAssigned(var)) break;
pq_need_update_for_var_at_trail_index_.Set(trail_->Info(var).trail_index);
var_ordering_.Remove(var.value());
@@ -271,7 +270,7 @@ Literal SatDecisionPolicy::NextBranch() {
// Choose its polarity (i.e. True of False).
const double random_ratio = parameters_.random_polarity_ratio();
if (random_ratio != 0.0 && zero_to_one() < random_ratio) {
return Literal(var, std::uniform_int_distribution<int>(0, 1)(random_));
return Literal(var, std::uniform_int_distribution<int>(0, 1)(*random_));
}
return Literal(var, var_use_phase_saving_[var]
? trail_->Info(var).last_polarity

4
ortools/sat/sat_decision.h
View File

@@ -109,9 +109,7 @@ class SatDecisionPolicy {
// Singleton model objects.
const SatParameters& parameters_;
Trail* trail_;
// TODO(user): make this part of the Model so it can be shared?
random_engine_t random_;
random_engine_t* random_;
// Variable ordering (priority will be adjusted dynamically). queue_elements_
// holds the elements used by var_ordering_ (it uses pointers).

11
ortools/sat/sat_parameters.proto
View File

@@ -18,7 +18,7 @@ package operations_research.sat;
// Contains the definitions for all the sat algorithm parameters and their
// default values.
//
// NEXT TAG: 105
// NEXT TAG: 106
message SatParameters {
// ==========================================================================
// Branching and polarity
@@ -568,13 +568,14 @@ message SatParameters {
// Specify the number of parallel workers to use during search.
// A number <= 1 means no parallelism.
optional int32 num_search_workers = 100 [default = 0];
optional bool deterministic_search = 101 [default = true];
// LNS parameters.
optional bool use_lns = 101 [default = false];
optional int32 lns_num_threads = 102 [default = 1];
optional bool use_lns = 102 [default = false];
optional int32 lns_num_threads = 103 [default = 1];
// Randomize fixed search.
optional bool randomize_search = 103 [default = false];
optional bool randomize_search = 104 [default = false];
// Search randomization will collect equivalent 'max valued' variables, and
// pick one randomly. For instance, if the variable strategy is CHOOSE_FIRST,
@@ -583,5 +584,5 @@ message SatParameters {
// variables, then the set of max valued variables will be all unassigned
// variables where
// lm <= variable min <= lm + search_randomization_tolerance
optional int64 search_randomization_tolerance = 104 [default = 0];
optional int64 search_randomization_tolerance = 105 [default = 0];
}

6
ortools/sat/sat_solver.cc
View File

@@ -123,9 +123,6 @@ void SatSolver::SetParameters(const SatParameters& parameters) {
*parameters_ = parameters;
pb_constraints_.SetParameters(parameters);
random_.seed(parameters.random_seed());
restart_->Reset();
time_limit_->ResetLimitFromParameters(parameters);
}
@@ -681,7 +678,8 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
SatParameters::
BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION) {
binary_implication_graph_.MinimizeConflictFirstWithTransitiveReduction(
*trail_, &learned_conflict_, &is_marked_, &random_);
*trail_, &learned_conflict_, &is_marked_,
model_->GetOrCreate<ModelRandomGenerator>());
}
DCHECK(IsConflictValid(learned_conflict_));
}

4
ortools/sat/sat_solver.h
View File

@@ -43,7 +43,6 @@
#include "ortools/sat/sat_base.h"
#include "ortools/sat/sat_decision.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/util/random_engine.h"
#include "ortools/util/stats.h"
#include "ortools/util/time_limit.h"
@@ -796,9 +795,6 @@ class SatSolver {
// analysis.
VariableWithSameReasonIdentifier same_reason_identifier_;
// A random number generator.
mutable random_engine_t random_;
// Temporary vector used by AddProblemClause().
std::vector<LiteralWithCoeff> tmp_pb_constraint_;

25
ortools/sat/util.cc
View File

@@ -13,34 +13,9 @@
#include "ortools/sat/util.h"
#if !defined(__PORTABLE_PLATFORM__)
#include "google/protobuf/descriptor.h"
#endif // __PORTABLE_PLATFORM__
namespace operations_research {
namespace sat {
void RandomizeDecisionHeuristic(MTRandom* random, SatParameters* parameters) {
#if !defined(__PORTABLE_PLATFORM__)
// Random preferred variable order.
const google::protobuf::EnumDescriptor* order_d =
SatParameters::VariableOrder_descriptor();
parameters->set_preferred_variable_order(
static_cast<SatParameters::VariableOrder>(
order_d->value(random->Uniform(order_d->value_count()))->number()));
// Random polarity initial value.
const google::protobuf::EnumDescriptor* polarity_d =
SatParameters::Polarity_descriptor();
parameters->set_initial_polarity(static_cast<SatParameters::Polarity>(
polarity_d->value(random->Uniform(polarity_d->value_count()))->number()));
#endif // __PORTABLE_PLATFORM__
// Other random parameters.
parameters->set_use_phase_saving(random->OneIn(2));
parameters->set_random_polarity_ratio(random->OneIn(2) ? 0.01 : 0.0);
parameters->set_random_branches_ratio(random->OneIn(2) ? 0.01 : 0.0);
}
int MoveOneUnprocessedLiteralLast(const std::set<LiteralIndex>& processed,
int relevant_prefix_size,
std::vector<Literal>* literals) {

51
ortools/sat/util.h
View File

@@ -15,14 +15,32 @@
#define OR_TOOLS_SAT_UTIL_H_
#include "ortools/base/random.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_base.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/util/random_engine.h"
#if !defined(__PORTABLE_PLATFORM__)
#include "google/protobuf/descriptor.h"
#endif // __PORTABLE_PLATFORM__
namespace operations_research {
namespace sat {
// The model "singleton" random engine used in the solver.
struct ModelRandomGenerator : public random_engine_t {
// We seed the strategy at creation only. This should be enough for our use
// case since the SatParameters is set first before the solver is created. We
// also never really need to change the seed afterwards, it is just used to
// diversify solves with identical parameters on different Model objects.
explicit ModelRandomGenerator(Model* model) : random_engine_t() {
seed(model->GetOrCreate<SatParameters>()->random_seed());
}
};
// Randomizes the decision heuristic of the given SatParameters.
void RandomizeDecisionHeuristic(MTRandom* random, SatParameters* parameters);
template <typename URBG>
void RandomizeDecisionHeuristic(URBG* random, SatParameters* parameters);
// Context: this function is not really generic, but required to be unit-tested.
// It is used in a clause minimization algorithm when we try to detect if any of
@@ -48,6 +66,37 @@ int MoveOneUnprocessedLiteralLast(const std::set<LiteralIndex>& processed,
int relevant_prefix_size,
std::vector<Literal>* literals);
// ============================================================================
// Implementation.
// ============================================================================
template <typename URBG>
inline void RandomizeDecisionHeuristic(URBG* random,
SatParameters* parameters) {
#if !defined(__PORTABLE_PLATFORM__)
// Random preferred variable order.
const google::protobuf::EnumDescriptor* order_d =
SatParameters::VariableOrder_descriptor();
parameters->set_preferred_variable_order(
static_cast<SatParameters::VariableOrder>(
order_d->value(absl::Uniform(*random, 0, order_d->value_count()))
->number()));
// Random polarity initial value.
const google::protobuf::EnumDescriptor* polarity_d =
SatParameters::Polarity_descriptor();
parameters->set_initial_polarity(static_cast<SatParameters::Polarity>(
polarity_d->value(absl::Uniform(*random, 0, polarity_d->value_count()))
->number()));
#endif // __PORTABLE_PLATFORM__
// Other random parameters.
parameters->set_use_phase_saving(absl::Bernoulli(*random, 0.5));
parameters->set_random_polarity_ratio(absl::Bernoulli(*random, 0.5) ? 0.01
: 0.0);
parameters->set_random_branches_ratio(absl::Bernoulli(*random, 0.5) ? 0.01
: 0.0);
}
} // namespace sat
} // namespace operations_research

2
ortools/util/time_limit.h
View File

@@ -244,7 +244,7 @@ class TimeLimit {
external_boolean_as_limit_ = external_boolean_as_limit;
}
// Returns the external boolean limit set by the previous call.
// Returns the current external Boolean limit.
bool* ExternalBooleanAsLimit() const { return external_boolean_as_limit_; }
// Sets new time limits. Note that this do not reset the running max nor