sat_runner.cc File Reference

#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 []

Function Documentation

ABSL_FLAG() [1/9]

ABSL_FLAG	(	bool	,
		competition_mode	,
		false	,
		"If	true,
		output the log in a competition format."	)

ABSL_FLAG() [2/9]

ABSL_FLAG	(	bool	,
		fingerprint_intermediate_solutions	,
		false	,
		"Attach the fingerprint of intermediate solutions to the output."	)

ABSL_FLAG() [3/9]

ABSL_FLAG	(	bool	,
		force_interleave_search	,
		false	,
		"If	true,
		enable interleaved workers when num_workers is 1."	)

ABSL_FLAG() [4/9]

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() [5/9]

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() [6/9]

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() [7/9]

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

http://www.apache.org/licenses/LICENSE-2.0

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() [8/9]

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() [9/9]

ABSL_FLAG	(	std::string	,
		params	,
		""	,
		"Parameters for the sat solver in a text format of the " "SatParameters	proto )

main()

int main	(	int	argc,
		char **	argv )

Definition at line 444 of file sat_runner.cc.

Variable Documentation

kUsage

const char kUsage[]

static

Initial value:

=
    "Usage: see flags.\n"
    "This program solves a given problem with the CP-SAT solver."

Definition at line 440 of file sat_runner.cc.