sat_runner.cc File Reference

Go to the source code of this file.

Namespaces
	operations_research
	Collection of objects used to extend the Constraint Solver library.
	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 LinearBooleanProblem proto (binary or text).")
	ABSL_FLAG (std::string, output, "", "If non-empty, write the input problem as a LinearBooleanProblem proto to " "this file. By default it uses the binary format except if the file " "extension is '.txt'. If the problem is SAT, a satisfiable assignment is " "also written to the file.")
	ABSL_FLAG (bool, output_cnf_solution, false, "If true and the problem was solved to optimality, this output " "the solution to stdout in cnf form.\n")
	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, strict_validity, false, "If true, stop if the given input is invalid (duplicate literals, " "out of range, zero cofficients, etc.)")
	ABSL_FLAG (std::string, lower_bound, "", "If not empty, look for a solution with an objective value >= this bound.")
	ABSL_FLAG (std::string, upper_bound, "", "If not empty, look for a solution with an objective value <= this bound.")
	ABSL_FLAG (bool, fu_malik, false, "If true, search the optimal solution with the Fu & Malik algo.")
	ABSL_FLAG (bool, wpm1, false, "If true, search the optimal solution with the WPM1 algo.")
	ABSL_FLAG (bool, qmaxsat, false, "If true, search the optimal solution with a linear scan and " " the cardinality encoding used in qmaxsat.")
	ABSL_FLAG (bool, core_enc, false, "If true, search the optimal solution with the core-based " "cardinality encoding algo.")
	ABSL_FLAG (bool, linear_scan, false, "If true, search the optimal solution with the linear scan algo.")
	ABSL_FLAG (int, randomize, 500, "If positive, solve that many times the problem with a random " "decision heuristic before trying to optimize it.")
	ABSL_FLAG (bool, use_symmetry, false, "If true, find and exploit the eventual symmetries " "of the problem.")
	ABSL_FLAG (bool, presolve, true, "Only work on pure SAT problem. If true, presolve the problem.")
	ABSL_FLAG (bool, probing, false, "If true, presolve the problem using probing.")
	ABSL_FLAG (bool, use_cp_model, true, "Whether to interpret everything as a CpModelProto or " "to read by default a CpModelProto.")
	ABSL_FLAG (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.")
int	main (int argc, char **argv)

Variables
static const char	kUsage []

Function Documentation

ABSL_FLAG() [1/18]

ABSL_FLAG	(	bool	,
		core_enc	,
		false	,
		"If	true,
		search the optimal solution with the core-based " "cardinality encoding algo."
	)

ABSL_FLAG() [2/18]

ABSL_FLAG	(	bool	,
		fu_malik	,
		false	,
		"If	true,
		search the optimal solution with the Fu &Malik algo."
	)

ABSL_FLAG() [3/18]

ABSL_FLAG	(	bool	,
		linear_scan	,
		false	,
		"If	true,
		search the optimal solution with the linear scan algo."
	)

ABSL_FLAG() [4/18]

ABSL_FLAG	(	bool	,
		output_cnf_solution	,
		false	,
		"If true and the problem was solved to	optimality,
		this output " "the solution to stdout in cnf form.\n"
	)

ABSL_FLAG() [5/18]

ABSL_FLAG	(	bool	,
		presolve	,
		true	,
		"Only work on pure SAT problem. If	true,
		presolve the problem."
	)

ABSL_FLAG() [6/18]

ABSL_FLAG	(	bool	,
		probing	,
		false	,
		"If	true,
		presolve the problem using probing."
	)

ABSL_FLAG() [7/18]

ABSL_FLAG	(	bool	,
		qmaxsat	,
		false	,
		"If	true,
		search the optimal solution with a linear scan and " " the cardinality encoding used in qmaxsat."
	)

ABSL_FLAG() [8/18]

ABSL_FLAG	(	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."
	)

ABSL_FLAG() [9/18]

ABSL_FLAG	(	bool	,
		strict_validity	,
		false	,
		"If	true,
		stop if the given input is invalid(duplicate literals, " "out of range, zero cofficients, etc.)"
	)

ABSL_FLAG() [10/18]

ABSL_FLAG	(	bool	,
		use_cp_model	,
		true	,
		"Whether to interpret everything as a CpModelProto or " "to read by default a CpModelProto."
	)

ABSL_FLAG() [11/18]

ABSL_FLAG	(	bool	,
		use_symmetry	,
		false	,
		"If	true,
		find and exploit the eventual symmetries " "of the problem."
	)

ABSL_FLAG() [12/18]

ABSL_FLAG	(	bool	,
		wpm1	,
		false	,
		"If	true,
		search the optimal solution with the WPM1 algo."
	)

ABSL_FLAG() [13/18]

ABSL_FLAG	(	int	,
		randomize	,
		500	,
		"If	positive,
		solve that many times the problem with a random " "decision heuristic before trying to optimize it."
	)

ABSL_FLAG() [14/18]

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 LinearBooleanProblem proto(binary or text)."
	)

ABSL_FLAG() [15/18]

ABSL_FLAG	(	std::string	,
		lower_bound	,
		""	,
		"If not	empty,
		look for a solution with an objective value >=this bound."
	)

ABSL_FLAG() [16/18]

ABSL_FLAG	(	std::string	,
		output	,
		""	,
		"If non-	empty,
		write the input problem as a LinearBooleanProblem proto to " "this file. By default it uses the binary format except if the file " "extension is '.txt'. If the problem is	SAT,
		a satisfiable assignment is " "also written to the file."
	)

ABSL_FLAG() [17/18]

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

ABSL_FLAG() [18/18]

ABSL_FLAG	(	std::string	,
		upper_bound	,
		""	,
		"If not	empty,
		look for a solution with an objective value<=this bound."
	)

main()

int main	(	int	argc,
		char **	argv
	)

Definition at line 451 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 447 of file sat_runner.cc.