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

update sat runner for pbo competition

Browse Source
This commit is contained in:
Laurent Perron
2025-04-17 16:23:03 +02:00
parent 6381d8d949
commit 89b85436fd
2 changed files with 32 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
ortools/sat/cp_model_solver.cc
View File

@@ -2140,6 +2140,13 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
--num_thread_available;
}
num_thread_available = std::max(num_thread_available, 0);
// If we are in interleaved mode with one worker, num_thread_available is
// always negative. We force it to 1 so that we at least have a
// feasibility_jump subsolver.
if (params.interleave_search() && params.num_workers() == 1) {
// TODO(user): the 1 should be a parameter.
num_thread_available = 1;
}
const std::vector<SatParameters> all_params =
RepeatParameters(name_filter.Filter(GetFirstSolutionBaseParams(params)),

25
ortools/sat/sat_runner.cc
View File

@@ -77,6 +77,8 @@ ABSL_FLAG(bool, fingerprint_intermediate_solutions, false,
"Attach the fingerprint of intermediate solutions to the output.");
ABSL_FLAG(bool, competition_mode, false,
"If true, output the log in a competition format.");
ABSL_FLAG(bool, force_interleave_search, false,
"If true, enable interleaved workers when num_workers is 1.");
namespace operations_research {
namespace sat {
@@ -169,6 +171,26 @@ void LogInPbCompetitionFormat(int num_variables, bool has_objective,
final_response_callback);
}
void SetInterleavedWorkers(bool has_objective, SatParameters* parameters) {
// Enable interleaved workers when num_workers is 1.
if (parameters->num_workers() == 1) {
parameters->set_interleave_search(true);
parameters->set_use_rins_lns(false);
if (has_objective) {
parameters->add_subsolvers("default_lp");
parameters->add_subsolvers("quick_restart");
parameters->add_subsolvers("core_or_no_lp");
parameters->add_subsolvers("max_lp");
parameters->set_num_violation_ls(1);
} else {
parameters->add_subsolvers("default_lp");
parameters->add_subsolvers("no_lp");
parameters->add_subsolvers("max_lp");
parameters->add_subsolvers("quick_restart");
}
}
}
bool LoadProblem(const std::string& filename, absl::string_view hint_file,
absl::string_view domain_file, CpModelProto* cp_model,
Model* model, SatParameters* parameters) {
@@ -204,6 +226,9 @@ bool LoadProblem(const std::string& filename, absl::string_view hint_file,
LogInPbCompetitionFormat(num_variables, cp_model->has_objective(), model,
parameters);
}
if (absl::GetFlag(FLAGS_force_interleave_search)) {
SetInterleavedWorkers(cp_model->has_objective(), parameters);
}
} else if (absl::EndsWith(filename, ".cnf") ||
absl::EndsWith(filename, ".cnf.xz") ||
absl::EndsWith(filename, ".cnf.gz") ||