Google OR-Tools: ortools/sat/sat_runner.cc Source File

14#include <cstdint>

15#include <cstdlib>

16#include <functional>

17#include <iostream>

18#include <limits>

19#include <memory>

20#include <string>

21#include <vector>

23#include "absl/base/thread_annotations.h"

24#include "absl/flags/flag.h"

25#include "absl/flags/parse.h"

26#include "absl/flags/usage.h"

27#include "absl/log/check.h"

28#include "absl/log/flags.h"

29#include "absl/log/initialize.h"

30#include "absl/log/log.h"

31#include "absl/strings/match.h"

32#include "absl/strings/str_format.h"

33#include "absl/strings/str_split.h"

34#include "absl/strings/string_view.h"

35#include "absl/synchronization/mutex.h"

36#include "absl/types/span.h"

37#include "google/protobuf/arena.h"

38#include "google/protobuf/text_format.h"

56 std::string, input, "",

57 "Required: input file of the problem to solve. Many format are supported:"

58 ".cnf (sat, max-sat, weighted max-sat), .opb (pseudo-boolean sat/optim) "

59 "and by default the CpModelProto proto (binary or text).");

62 std::string, hint_file, "",

63 "Protobuf file containing a CpModelResponse. The solution will be used as a"

64 " hint to bootstrap the search.");

67 "Protobuf file containing a CpModelResponse. If present, the "

68 "tightened models will be used to reduce the domain of variables.");

71 "If non-empty, write the response there. By default it uses the "

72 "binary format except if the file extension is '.txt'.");

75 "Parameters for the sat solver in a text format of the "

76 "SatParameters proto, example: --params=use_conflicts:true.");

78ABSL_FLAG(bool, wcnf_use_strong_slack, true,

79 "If true, when we add a slack variable to reify a soft clause, we "

80 "enforce the fact that when it is true, the clause must be false.");

81ABSL_FLAG(bool, fingerprint_intermediate_solutions, false,

82 "Attach the fingerprint of intermediate solutions to the output.");

84 "If true, output the log in a competition format.");

85ABSL_FLAG(bool, force_interleave_search, false,

86 "If true, enable interleaved workers when num_workers is 1.");

89namespace sat {

90namespace {

92void TryToRemoveSuffix(absl::string_view suffix, std::string* str) {

94}

96std::string ExtractName(absl::string_view full_filename) {

97 std::string filename = std::string(file::Basename(full_filename));

99 TryToRemoveSuffix("gz", &filename);

100 TryToRemoveSuffix("txt", &filename);

101 TryToRemoveSuffix("pb", &filename);

102 TryToRemoveSuffix("pbtxt", &filename);

103 TryToRemoveSuffix("proto", &filename);

104 TryToRemoveSuffix("prototxt", &filename);

105 TryToRemoveSuffix("textproto", &filename);

106 TryToRemoveSuffix("bin", &filename);

107 return filename;

108}

109

110class LastSolutionPrinter {

111 public:

112

113 void MaybePrintLastSolution() {

114 absl::MutexLock lock(mutex_);

115 if (last_solution_printed_) return;

116 last_solution_printed_ = true;

117

118 if (last_solution_.empty()) {

119 std::cout << "s UNKNOWN" << std::endl;

120 } else {

121 std::cout << "s SATISFIABLE" << std::endl;

122 std::string line;

123 for (int i = 0; i < num_variables_; ++i) {

124 if (last_solution_[i]) {

125 absl::StrAppend(&line, "x", i + 1, " ");

126 } else {

127 absl::StrAppend(&line, "-x", i + 1, " ");

128 }

129 if (line.size() >= 75) {

130 std::cout << "v " << line << std::endl;

131 line.clear();

132 }

133 }

134 if (!line.empty()) {

135 std::cout << "v " << line << std::endl;

136 }

137 }

138 }

139

140 void set_num_variables(int num_variables) { num_variables_ = num_variables; }

141

142 void set_last_solution(absl::Span<const int64_t> solution) {

143 absl::MutexLock lock(mutex_);

144 if (last_solution_printed_) return;

146 }

147

148

149

150 bool mark_last_solution_printed() {

151 const absl::MutexLock lock(mutex_);

152 if (last_solution_printed_) {

153 return false;

154 }

155 last_solution_printed_ = true;

156 return true;

157 }

158

159 private:

160 int num_variables_ = 0;

161 std::vector<int64_t> last_solution_ ABSL_GUARDED_BY(mutex_);

162 bool last_solution_printed_ ABSL_GUARDED_BY(mutex_) = false;

163 absl::Mutex mutex_;

164};

165

166void LogInPbCompetitionFormat(

167 int num_variables, bool has_objective, Model* model,

169 std::shared_ptr<LastSolutionPrinter> last_solution_printer) {

170 CHECK(last_solution_printer != nullptr);

171 last_solution_printer->set_num_variables(num_variables);

172

173 const auto log_callback = [](const std::string& multi_line_input) {

174 if (multi_line_input.empty()) {

175 std::cout << "c" << std::endl;

176 return;

177 }

178 const std::vector<absl::string_view> lines =

179 absl::StrSplit(multi_line_input, '\n');

180 for (const absl::string_view& line : lines) {

181 std::cout << "c " << line << std::endl;

182 }

183 };

184 model->GetOrCreate<SolverLogger>()->AddInfoLoggingCallback(log_callback);

185 parameters->set_log_to_stdout(false);

186

187 const auto response_callback = [last_solution_printer](

189 std::cout << "o " << static_cast<int64_t>(r.objective_value()) << std::endl;

190 last_solution_printer->set_last_solution(r.solution());

191 };

193

194 const auto final_response_callback =

195 [num_variables, has_objective,

197 if (!last_solution_printer->mark_last_solution_printed()) return;

198

199 switch (r->status()) {

201 if (has_objective) {

202 std::cout << "s OPTIMUM FOUND " << std::endl;

203 } else {

204 std::cout << "s SATISFIABLE" << std::endl;

205 }

206 break;

208 std::cout << "s SATISFIABLE" << std::endl;

209 break;

211 std::cout << "s UNSATISFIABLE" << std::endl;

212 break;

214 std::cout << "s UNSUPPORTED" << std::endl;

215 break;

217 std::cout << "s UNKNOWN" << std::endl;

218 break;

219 default:

220 break;

221 }

224 std::string line;

225 for (int i = 0; i < num_variables; ++i) {

226 if (r->solution(i)) {

227 absl::StrAppend(&line, "x", i + 1, " ");

228 } else {

229 absl::StrAppend(&line, "-x", i + 1, " ");

230 }

231 if (line.size() >= 75) {

232 std::cout << "v " << line << std::endl;

233 line.clear();

234 }

235 }

236 if (!line.empty()) {

237 std::cout << "v " << line << std::endl;

238 }

239 }

240 };

242 final_response_callback);

243}

244

245void SetInterleavedWorkers(SatParameters* parameters) {

246

247 if (parameters->num_workers() == 1) {

248 parameters->set_interleave_search(true);

249 parameters->set_use_rins_lns(false);

250 parameters->add_subsolvers("default_lp");

251 parameters->add_subsolvers("max_lp");

252 parameters->add_subsolvers("quick_restart");

253 parameters->add_subsolvers("core_or_no_lp");

254 parameters->set_num_violation_ls(1);

255 }

256}

257

258bool LoadProblem(const std::string& filename, absl::string_view hint_file,

259 absl::string_view domain_file, CpModelProto* cp_model,

261 std::shared_ptr<LastSolutionPrinter> last_solution_printer) {

262 if (absl::EndsWith(filename, ".opb") ||

263 absl::EndsWith(filename, ".opb.bz2") ||

264 absl::EndsWith(filename, ".opb.gz") || absl::EndsWith(filename, ".wbo") ||

265 absl::EndsWith(filename, ".wbo.bz2") ||

266 absl::EndsWith(filename, ".wbo.gz")) {

268 if (!reader.LoadAndValidate(filename, cp_model)) {

269 if (!reader.model_is_supported()) {

270 if (absl::GetFlag(FLAGS_competition_mode)) {

271

272 std::cout << "s UNSUPPORTED" << std::endl;

273 return false;

274 } else {

275

276

277

279 var->add_domain(std::numeric_limits<int64_t>::min());

280 var->add_domain(std::numeric_limits<int64_t>::max());

281 return true;

282 }

283 } else {

284 return false;

285 }

286 }

287

288 if (absl::GetFlag(FLAGS_competition_mode)) {

289 const int num_variables =

290 reader.model_is_supported() ? reader.num_variables() : 1;

291 LogInPbCompetitionFormat(num_variables, cp_model->has_objective(), model,

292 parameters, last_solution_printer);

293 }

294 if (absl::GetFlag(FLAGS_force_interleave_search)) {

295 SetInterleavedWorkers(parameters);

296 }

297 if (parameters->num_workers() >= 2 && parameters->num_workers() <= 15) {

298

299

300 parameters->add_ignore_subsolvers("max_lp_sym");

301 parameters->add_extra_subsolvers("max_lp");

302 }

303 } else if (absl::EndsWith(filename, ".cnf") ||

304 absl::EndsWith(filename, ".cnf.xz") ||

305 absl::EndsWith(filename, ".cnf.gz") ||

306 absl::EndsWith(filename, ".wcnf") ||

307 absl::EndsWith(filename, ".wcnf.xz") ||

308 absl::EndsWith(filename, ".wcnf.gz")) {

309 SatCnfReader reader(absl::GetFlag(FLAGS_wcnf_use_strong_slack));

310 if (!reader.Load(filename, cp_model)) {

311 LOG(FATAL) << "Cannot load file '" << filename << "'.";

312 }

313 } else {

315 }

316

317

318 if (!hint_file.empty()) {

321 if (!response.solution().empty()) {

322 CHECK_EQ(response.solution_size(), cp_model->variables_size())

323 << "The hint from the response proto is not compatible with the "

324 "model proto";

325

326 cp_model->clear_solution_hint();

327 for (int i = 0; i < cp_model->variables_size(); ++i) {

328 cp_model->mutable_solution_hint()->add_vars(i);

329 cp_model->mutable_solution_hint()->add_values(response.solution(i));

330 }

331 } else {

332 LOG(INFO) << "The response proto has no solutions, ignoring.";

333 }

334 }

335

336

337 if (!domain_file.empty()) {

340 if (!response.tightened_variables().empty()) {

341 CHECK_EQ(response.tightened_variables_size(), cp_model->variables_size())

342 << "The tighened variables from the response proto is not "

343 "compatible with the model proto";

344

345 for (int i = 0; i < cp_model->variables_size(); ++i) {

347 const Domain tightened_domain =

349 const Domain new_domain =

352 }

353 } else {

354 LOG(INFO) << "The response proto has no tightened variable domains, "

355 "ignoring.";

356 }

357 }

358

359

360 if (cp_model->name().empty()) {

361 cp_model->set_name(ExtractName(filename));

362 }

363 return true;

364}

365

366int Run() {

369 if (absl::GetFlag(FLAGS_input).empty()) {

370 LOG(FATAL) << "Please supply a data file with --input=";

371 }

372

373

375 if (!absl::GetFlag(FLAGS_params).empty()) {

376 CHECK(google::protobuf::TextFormat::MergeFromString(

377 absl::GetFlag(FLAGS_params), &parameters))

378 << absl::GetFlag(FLAGS_params);

379 }

380

381

382 google::protobuf::Arena arena;

384 google::protobuf::Arena::Create<CpModelProto>(&arena);

385 std::shared_ptr<LastSolutionPrinter> last_solution_printer;

386 if (absl::GetFlag(FLAGS_competition_mode)) {

387 last_solution_printer = std::make_shared<LastSolutionPrinter>();

388 }

389 if (!LoadProblem(absl::GetFlag(FLAGS_input), absl::GetFlag(FLAGS_hint_file),

390 absl::GetFlag(FLAGS_domain_file), cp_model, &model,

391 &parameters, last_solution_printer)) {

392 if (!absl::GetFlag(FLAGS_competition_mode)) {

393 LOG(FATAL) << "Cannot load file '" << absl::GetFlag(FLAGS_input) << "'.";

394 }

395 return EXIT_SUCCESS;

396 }

397

399 if (absl::GetFlag(FLAGS_fingerprint_intermediate_solutions)) {

400

401

403 return absl::StrFormat(

404 "fingerprint: %#x",

406 }));

407 }

408

409 if (absl::GetFlag(FLAGS_competition_mode)) {

410 model.GetOrCreate<SigtermHandler>()->Register([last_solution_printer]() {

411 last_solution_printer->MaybePrintLastSolution();

412 exit(EXIT_SUCCESS);

413 });

414 }

415

417

418 if (!absl::GetFlag(FLAGS_output).empty()) {

419 if (absl::EndsWith(absl::GetFlag(FLAGS_output), "txt")) {

422 } else {

425 }

426 }

427

428

429

433 return EXIT_SUCCESS;

434}

435

436}

437}

438}

439

441 "Usage: see flags.\n"

442 "This program solves a given problem with the CP-SAT solver.";

443

444int main(int argc, char** argv) {

445 absl::InitializeLog();

446 absl::SetProgramUsageMessage(kUsage);

447 absl::ParseCommandLine(argc, argv);

448 return operations_research::sat::Run();

449}

Domain IntersectionWith(const Domain &domain) const

void add_domain(::int64_t value)

void set_log_search_progress(bool value)

absl::Status SetBinaryProto(absl::string_view file_name, const google::protobuf::Message &proto, Options options)

absl::string_view Extension(absl::string_view path)

absl::Status SetTextProto(absl::string_view file_name, const google::protobuf::Message &proto, Options options)

absl::string_view Stem(absl::string_view path)

absl::string_view Basename(absl::string_view path)

constexpr uint64_t kDefaultFingerprintSeed

uint64_t FingerprintRepeatedField(const google::protobuf::RepeatedField< T > &sequence, uint64_t seed)

std::function< SatParameters(Model *)> NewSatParameters(absl::string_view params)

void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)

CpSolverResponse SolveCpModel(const CpModelProto &model_proto, Model *model)

std::function< void(Model *)> NewFeasibleSolutionLogCallback(const std::function< std::string(const CpSolverResponse &response)> &callback)

Domain ReadDomainFromProto(const ProtoWithDomain &proto)

std::function< void(Model *)> NewFeasibleSolutionObserver(const std::function< void(const CpSolverResponse &response)> &callback)

Select next search node to expand Select next item_i to add this new search node to the search Generate a new search node where item_i is not in the knapsack Check validity of this new partial solution(using propagators) - If valid

absl::Status ReadFileToProto(absl::string_view filename, google::protobuf::Message *proto, bool allow_partial)

static int input(yyscan_t yyscanner)

int main(int argc, char **argv)

Definition sat_runner.cc:444

ABSL_FLAG(std::string, input, "", "Required: input file of the problem to solve. Many format are supported:" ".cnf (sat, max-sat, weighted max-sat), .opb (pseudo-boolean sat/optim) " "and by default the CpModelProto proto (binary or text).")

static const char kUsage[]

Definition sat_runner.cc:440