boolean_problem.cc File Reference

Go to the source code of this file.

Namespaces
namespace	operations_research
	The vehicle routing library lets one model and solve generic vehicle routing problems ranging from the Traveling Salesman Problem to more complex problems such as the Capacitated Vehicle Routing Problem with Time Windows.
namespace	operations_research::sat

Functions
	ABSL_FLAG (std::string, debug_dump_symmetry_graph_to_file, "", "If this flag is non-empty, an undirected graph whose" " automorphism group is in one-to-one correspondence with the" " symmetries of the SAT problem will be dumped to a file every" " time FindLinearBooleanProblemSymmetries() is called.")
void	ExtractAssignment (const LinearBooleanProblem &problem, const SatSolver &solver, std::vector< bool > *assignment)
absl::Status	ValidateBooleanProblem (const LinearBooleanProblem &problem)
CpModelProto	BooleanProblemToCpModelproto (const LinearBooleanProblem &problem)
void	ChangeOptimizationDirection (LinearBooleanProblem *problem)
bool	LoadBooleanProblem (const LinearBooleanProblem &problem, SatSolver *solver)
bool	LoadAndConsumeBooleanProblem (LinearBooleanProblem *problem, SatSolver *solver)
void	UseObjectiveForSatAssignmentPreference (const LinearBooleanProblem &problem, SatSolver *solver)
bool	AddObjectiveUpperBound (const LinearBooleanProblem &problem, Coefficient upper_bound, SatSolver *solver)
bool	AddObjectiveConstraint (const LinearBooleanProblem &problem, bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, SatSolver *solver)
Coefficient	ComputeObjectiveValue (const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
bool	IsAssignmentValid (const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
std::string	LinearBooleanProblemToCnfString (const LinearBooleanProblem &problem)
void	StoreAssignment (const VariablesAssignment &assignment, BooleanAssignment *output)
void	ExtractSubproblem (const LinearBooleanProblem &problem, const std::vector< int > &constraint_indices, LinearBooleanProblem *subproblem)
template<typename Graph >
Graph *	GenerateGraphForSymmetryDetection (const LinearBooleanProblem &problem, std::vector< int > *initial_equivalence_classes)
void	MakeAllLiteralsPositive (LinearBooleanProblem *problem)
void	FindLinearBooleanProblemSymmetries (const LinearBooleanProblem &problem, std::vector< std::unique_ptr< SparsePermutation > > *generators)
void	ApplyLiteralMappingToBooleanProblem (const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping, LinearBooleanProblem *problem)
void	ProbeAndSimplifyProblem (SatPostsolver *postsolver, LinearBooleanProblem *problem)

Function Documentation

ABSL_FLAG()

ABSL_FLAG	(	std::string	,
		debug_dump_symmetry_graph_to_file	,
		""	,
		"If this flag is non-	empty,
		an undirected graph whose" " automorphism group is in one-to-one correspondence with the" " symmetries of the SAT problem will be dumped to a file every" " time FindLinearBooleanProblemSymmetries() is called."
	)