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
	OR-Tools root namespace.
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)."	)

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.