diff --git a/examples/cpp/BUILD b/examples/cpp/BUILD index c83a4f8a980..2f461bcd51e 100644 --- a/examples/cpp/BUILD +++ b/examples/cpp/BUILD @@ -12,9 +12,9 @@ cc_binary( name = "cryptarithm", srcs = ["cryptarithm.cc"], deps = [ - "@com_google_protobuf_cc//:protobuf", "//ortools/base", "//ortools/constraint_solver:cp", + "@com_google_protobuf_cc//:protobuf", ], ) @@ -230,7 +230,7 @@ cc_binary( srcs = ["integer_programming.cc"], deps = [ "//ortools/base", - "//ortools/linear_solver:linear_solver", + "//ortools/linear_solver", ], ) @@ -309,7 +309,7 @@ cc_binary( copts = ["-DUSE_GLOP"], deps = [ "//ortools/base", - "//ortools/linear_solver:linear_solver", + "//ortools/linear_solver", "//ortools/linear_solver:linear_solver_cc_proto", ], ) @@ -319,7 +319,7 @@ cc_binary( srcs = ["linear_solver_protocol_buffers.cc"], deps = [ "//ortools/base", - "//ortools/linear_solver:linear_solver", + "//ortools/linear_solver", "//ortools/linear_solver:linear_solver_cc_proto", ], ) @@ -415,28 +415,28 @@ cc_binary( "sat_runner.cc", ], deps = [ - "@com_google_protobuf_cc//:protobuf", + "//ortools/algorithms:sparse_permutation", + "//ortools/base", + "//ortools/base:file", + "//ortools/base:random", + "//ortools/base:status", + "//ortools/base:strings", + "//ortools/base:threadpool", + "//ortools/lp_data:mps_reader", + "//ortools/lp_data:proto_utils", "//ortools/sat:boolean_problem", "//ortools/sat:boolean_problem_cc_proto", - # "//ortools/sat:cp_model_proto", - # "//ortools/sat:cp_model_solver", + "//ortools/sat:cp_model_cc_proto", + "//ortools/sat:cp_model_solver", "//ortools/sat:drat", "//ortools/sat:lp_utils", "//ortools/sat:optimization", "//ortools/sat:sat_solver", "//ortools/sat:simplification", "//ortools/sat:symmetry", - "//ortools/base", - "//ortools/base:file", - "//ortools/base:strings", - "//ortools/base:status", - "//ortools/base:random", - "//ortools/base:threadpool", - "//ortools/algorithms:sparse_permutation", - "//ortools/lp_data:mps_reader", - "//ortools/lp_data:proto_utils", "//ortools/util:filelineiter", "//ortools/util:time_limit", + "@com_google_protobuf_cc//:protobuf", ], ) @@ -470,7 +470,7 @@ cc_binary( ], deps = [ "//ortools/base", - "//ortools/linear_solver:linear_solver", + "//ortools/linear_solver", "//ortools/linear_solver:linear_solver_cc_proto", "//ortools/lp_data:mps_reader", ], @@ -491,7 +491,7 @@ cc_binary( copts = ["-DUSE_GLOP"], deps = [ "//ortools/base", - "//ortools/linear_solver:linear_solver", + "//ortools/linear_solver", ], ) @@ -499,11 +499,11 @@ cc_binary( name = "tsp", srcs = ["tsp.cc"], deps = [ - "@com_google_protobuf_cc//:protobuf", "//ortools/base", "//ortools/constraint_solver:cp", "//ortools/constraint_solver:routing", "//ortools/constraint_solver:routing_flags", + "@com_google_protobuf_cc//:protobuf", ], ) @@ -513,7 +513,6 @@ cc_binary( "weighted_tardiness_sat.cc", ], deps = [ - "@com_google_protobuf_cc//:protobuf", "//ortools/base", "//ortools/base:file", "//ortools/base:strings", @@ -526,5 +525,6 @@ cc_binary( "//ortools/sat:precedences", "//ortools/sat:sat_solver", "//ortools/util:filelineiter", + "@com_google_protobuf_cc//:protobuf", ], ) diff --git a/examples/cpp/sat_cnf_reader.h b/examples/cpp/sat_cnf_reader.h index efed6901670..2e22dd5756b 100644 --- a/examples/cpp/sat_cnf_reader.h +++ b/examples/cpp/sat_cnf_reader.h @@ -103,11 +103,11 @@ class SatCnfReader { return problem_name; } - int64 StringViewAtoi(const string_view& input) { + int64 StringPieceAtoi(string_view input) { // Hack: data() is not null terminated, but we do know that it points // inside a std::string where numbers are separated by " " and since atoi64 will // stop at the first invalid char, this works. - return atoi64(input.data()); + return atoi64(input.data()); // NOLINT } void ProcessNewLine(const std::string& line, LinearBooleanProblem* problem) { @@ -123,11 +123,11 @@ class SatCnfReader { if (words_[0] == "p") { if (words_[1] == "cnf" || words_[1] == "wcnf") { - num_variables_ = StringViewAtoi(words_[2]); - num_clauses_ = StringViewAtoi(words_[3]); + num_variables_ = StringPieceAtoi(words_[2]); + num_clauses_ = StringPieceAtoi(words_[3]); if (words_[1] == "wcnf") { is_wcnf_ = true; - hard_weight_ = (words_.size() > 4) ? StringViewAtoi(words_[4]) : 0; + hard_weight_ = (words_.size() > 4) ? StringPieceAtoi(words_[4]) : 0; } } else { // TODO(user): The ToString() is only required for the open source. Fix. @@ -148,7 +148,7 @@ class SatCnfReader { int64 weight = (!is_wcnf_ && interpret_cnf_as_max_sat_) ? 1 : hard_weight_; for (int i = 0; i < size; ++i) { - const int64 signed_value = StringViewAtoi(words_[i]); + const int64 signed_value = StringPieceAtoi(words_[i]); if (i == 0 && is_wcnf_) { // Mathematically, a soft clause of weight 0 can be removed. if (signed_value == 0) { diff --git a/examples/cpp/sat_runner.cc b/examples/cpp/sat_runner.cc index d81cf82e71a..9681c02dc72 100644 --- a/examples/cpp/sat_runner.cc +++ b/examples/cpp/sat_runner.cc @@ -30,6 +30,8 @@ #include "ortools/base/threadpool.h" #include "ortools/algorithms/sparse_permutation.h" #include "ortools/sat/boolean_problem.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/drat.h" #include "examples/cpp/opb_reader.h" #include "ortools/sat/optimization.h" @@ -38,6 +40,7 @@ #include "ortools/sat/sat_solver.h" #include "ortools/sat/simplification.h" #include "ortools/sat/symmetry.h" +#include "ortools/util/file_util.h" #include "ortools/util/time_limit.h" #include "ortools/base/random.h" #include "ortools/base/status.h" @@ -106,11 +109,19 @@ DEFINE_bool(presolve, true, DEFINE_bool(probing, false, "If true, presolve the problem using probing."); +DEFINE_bool(use_cp_model, true, + "Whether to interpret a linear program input as a CpModelProto or " + "to read by default a CpModelProto."); + DEFINE_bool(reduce_memory_usage, false, "If true, do not keep a copy of the original problem in memory." "This reduce the memory usage, but disable the solution cheking at " "the end."); +DEFINE_string( + drat_output, "", + "If non-empty, a proof in DRAT format will be written to this file."); + namespace operations_research { namespace sat { namespace { @@ -126,7 +137,8 @@ double GetScaledTrivialBestBound(const LinearBooleanProblem& problem) { return AddOffsetAndScaleObjectiveValue(problem, best_bound); } -void LoadBooleanProblem(std::string filename, LinearBooleanProblem* problem) { +void LoadBooleanProblem(const std::string& filename, LinearBooleanProblem* problem, + CpModelProto* cp_model) { if (strings::EndsWith(filename, ".opb") || strings::EndsWith(filename, ".opb.bz2")) { OpbReader reader; @@ -145,8 +157,12 @@ void LoadBooleanProblem(std::string filename, LinearBooleanProblem* problem) { if (!reader.Load(filename, problem)) { LOG(FATAL) << "Cannot load file '" << filename << "'."; } + } else if (FLAGS_use_cp_model) { + LOG(INFO) << "Reading a CpModelProto."; + *cp_model = ReadFileToProtoOrDie(filename); } else { - file::ReadFileToProtoOrDie(filename, problem); + LOG(INFO) << "Reading a LinearBooleanProblem."; + *problem = ReadFileToProtoOrDie(filename); } } @@ -178,14 +194,20 @@ int Run() { << FLAGS_params; } - Model model; - DratWriter* drat_writer = model.GetOrCreate(); // Initialize the solver. std::unique_ptr solver(new SatSolver()); - solver->SetDratWriter(drat_writer); solver->SetParameters(parameters); + // Create a DratWriter? + std::unique_ptr drat_writer; + if (!FLAGS_drat_output.empty()) { + File* output; + CHECK_OK(file::Open(FLAGS_drat_output, "w", &output, file::Defaults())); + drat_writer.reset(new DratWriter(/*in_binary_format=*/false, output)); + solver->SetDratWriter(drat_writer.get()); + } + // The global time limit. std::unique_ptr time_limit(TimeLimit::FromParameters(parameters)); @@ -195,7 +217,21 @@ int Run() { // Read the problem. LinearBooleanProblem problem; - LoadBooleanProblem(FLAGS_input, &problem); + CpModelProto cp_model; + LoadBooleanProblem(FLAGS_input, &problem, &cp_model); + + // TODO(user): clean this hack. Ideally LinearBooleanProblem should be + // completely replaced by the more general CpModelProto. + if (cp_model.variables_size() != 0) { + Model model; + model.GetOrCreate()->SetParameters(parameters); + model.SetSingleton(std::move(time_limit)); + LOG(INFO) << CpModelStats(cp_model); + const CpSolverResponse response = SolveCpModel(cp_model, &model); + LOG(INFO) << CpSolverResponseStats(response); + exit(EXIT_SUCCESS); + } + if (FLAGS_strict_validity) { const util::Status status = ValidateBooleanProblem(problem); if (!status.ok()) { @@ -255,7 +291,8 @@ int Run() { for (int i = 0; i < generators.size(); ++i) { propagator->AddSymmetry(std::move(generators[i])); } - solver->AddPropagator(std::move(propagator)); + solver->AddPropagator(propagator.get()); + solver->TakePropagatorOwnership(std::move(propagator)); } // Optimize? @@ -292,7 +329,7 @@ int Run() { parameters.set_log_search_progress(true); solver->SetParameters(parameters); if (FLAGS_presolve) { - result = SolveWithPresolve(&solver, &solution, drat_writer); + result = SolveWithPresolve(&solver, &solution, drat_writer.get()); if (result == SatSolver::MODEL_SAT) { CHECK(IsAssignmentValid(problem, solution)); } diff --git a/examples/cpp/solve.cc b/examples/cpp/solve.cc index 91fa3864ff3..d7c4a37d156 100644 --- a/examples/cpp/solve.cc +++ b/examples/cpp/solve.cc @@ -45,8 +45,8 @@ DEFINE_string(params_file, "", "If this flag is set, the --params flag is ignored."); DEFINE_string(params, "", "Solver specific parameters"); DEFINE_int64(time_limit_ms, 0, - "If stricitly positive, specifies a limit in ms on the solving" - " time."); + "If strictly positive, specifies a limit in ms on the solving " + "time. Otherwise, no time limit will be imposed."); DEFINE_string(forced_mps_format, "", "Set to force the mps format to use: free, fixed");