![]() |
Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
|
#include <cstdint>
#include <cstdlib>
#include <functional>
#include <iostream>
#include <limits>
#include <memory>
#include <string>
#include <vector>
#include "absl/base/thread_annotations.h"
#include "absl/flags/flag.h"
#include "absl/flags/parse.h"
#include "absl/flags/usage.h"
#include "absl/log/check.h"
#include "absl/log/flags.h"
#include "absl/log/initialize.h"
#include "absl/log/log.h"
#include "absl/strings/match.h"
#include "absl/strings/str_format.h"
#include "absl/strings/str_split.h"
#include "absl/strings/string_view.h"
#include "absl/synchronization/mutex.h"
#include "absl/types/span.h"
#include "google/protobuf/arena.h"
#include "google/protobuf/text_format.h"
#include "ortools/base/helpers.h"
#include "ortools/base/options.h"
#include "ortools/base/path.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/sat/model.h"
#include "ortools/sat/opb_reader.h"
#include "ortools/sat/sat_cnf_reader.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/sat/synchronization.h"
#include "ortools/util/file_util.h"
#include "ortools/util/logging.h"
#include "ortools/util/sigint.h"
#include "ortools/util/sorted_interval_list.h"
Go to the source code of this file.
Namespaces | |
namespace | operations_research |
In SWIG mode, we don't want anything besides these top-level includes. | |
namespace | operations_research::sat |
Functions | |
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).") | |
ABSL_FLAG (std::string, hint_file, "", "Protobuf file containing a CpModelResponse. The solution will be used as a" " hint to bootstrap the search.") | |
ABSL_FLAG (std::string, domain_file, "", "Protobuf file containing a CpModelResponse. If present, the " "tightened models will be used to reduce the domain of variables.") | |
ABSL_FLAG (std::string, output, "", "If non-empty, write the response there. By default it uses the " "binary format except if the file extension is '.txt'.") | |
ABSL_FLAG (std::string, params, "", "Parameters for the sat solver in a text format of the " "SatParameters proto, example: --params=use_conflicts:true.") | |
ABSL_FLAG (bool, wcnf_use_strong_slack, true, "If true, when we add a slack variable to reify a soft clause, we " "enforce the fact that when it is true, the clause must be false.") | |
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.") | |
int | main (int argc, char **argv) |
Variables | |
static const char | kUsage [] |
ABSL_FLAG | ( | bool | , |
competition_mode | , | ||
false | , | ||
"If | true, | ||
output the log in a competition format." | ) |
ABSL_FLAG | ( | bool | , |
fingerprint_intermediate_solutions | , | ||
false | , | ||
"Attach the fingerprint of intermediate solutions to the output." | ) |
ABSL_FLAG | ( | bool | , |
force_interleave_search | , | ||
false | , | ||
"If | true, | ||
enable interleaved workers when num_workers is 1." | ) |
ABSL_FLAG | ( | bool | , |
wcnf_use_strong_slack | , | ||
true | , | ||
"If | true, | ||
when we add a slack variable to reify a soft | clause, | ||
we " "enforce the fact that when it is | true, | ||
the clause must be false." | ) |
ABSL_FLAG | ( | std::string | , |
domain_file | , | ||
"" | , | ||
"Protobuf file containing a CpModelResponse. If | present, | ||
the " "tightened models will be used to reduce the domain of variables." | ) |
ABSL_FLAG | ( | std::string | , |
hint_file | , | ||
"" | , | ||
"Protobuf file containing a CpModelResponse. The solution will be used as a" " hint to bootstrap the search." | ) |
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)." | ) |
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.
ABSL_FLAG | ( | std::string | , |
output | , | ||
"" | , | ||
"If non- | empty, | ||
write the response there. By default it uses the " "binary format except if the file extension is '.txt'." | ) |
ABSL_FLAG | ( | std::string | , |
params | , | ||
"" | , | ||
"Parameters for the sat solver in a text format of the " "SatParameters | proto ) |
int main | ( | int | argc, |
char ** | argv ) |
Definition at line 444 of file sat_runner.cc.
|
static |
Definition at line 440 of file sat_runner.cc.