boolean_problem.cc File Reference

#include "ortools/sat/boolean_problem.h"
#include <algorithm>
#include <cstdint>
#include <cstdlib>
#include <limits>
#include <memory>
#include <numeric>
#include <string>
#include <utility>
#include <vector>
#include "absl/container/flat_hash_map.h"
#include "absl/flags/flag.h"
#include "absl/log/check.h"
#include "absl/status/status.h"
#include "absl/strings/str_format.h"
#include "absl/strings/string_view.h"
#include "absl/types/span.h"
#include "ortools/base/logging.h"
#include "ortools/graph/graph.h"
#include "ortools/graph/graph_io.h"
#include "ortools/algorithms/find_graph_symmetries.h"
#include "ortools/algorithms/sparse_permutation.h"
#include "ortools/base/strong_vector.h"
#include "ortools/graph/util.h"
#include "ortools/port/proto_utils.h"
#include "ortools/sat/boolean_problem.pb.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/pb_constraint.h"
#include "ortools/sat/sat_base.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/sat/sat_solver.h"
#include "ortools/sat/simplification.h"
#include "ortools/util/strong_integers.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, 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	operations_research::sat::ExtractAssignment (const LinearBooleanProblem &problem, const SatSolver &solver, std::vector< bool > *assignment)
absl::Status	operations_research::sat::ValidateBooleanProblem (const LinearBooleanProblem &problem)
CpModelProto	operations_research::sat::BooleanProblemToCpModelproto (const LinearBooleanProblem &problem)
void	operations_research::sat::ChangeOptimizationDirection (LinearBooleanProblem *problem)
bool	operations_research::sat::LoadBooleanProblem (const LinearBooleanProblem &problem, SatSolver *solver)
bool	operations_research::sat::LoadAndConsumeBooleanProblem (LinearBooleanProblem *problem, SatSolver *solver)
void	operations_research::sat::UseObjectiveForSatAssignmentPreference (const LinearBooleanProblem &problem, SatSolver *solver)
bool	operations_research::sat::AddObjectiveUpperBound (const LinearBooleanProblem &problem, Coefficient upper_bound, SatSolver *solver)
bool	operations_research::sat::AddObjectiveConstraint (const LinearBooleanProblem &problem, bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, SatSolver *solver)
Coefficient	operations_research::sat::ComputeObjectiveValue (const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
bool	operations_research::sat::IsAssignmentValid (const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
std::string	operations_research::sat::LinearBooleanProblemToCnfString (const LinearBooleanProblem &problem)
void	operations_research::sat::StoreAssignment (const VariablesAssignment &assignment, BooleanAssignment *output)
void	operations_research::sat::ExtractSubproblem (const LinearBooleanProblem &problem, absl::Span< const int > constraint_indices, LinearBooleanProblem *subproblem)
template<typename Graph>
Graph *	operations_research::sat::GenerateGraphForSymmetryDetection (const LinearBooleanProblem &problem, std::vector< int > *initial_equivalence_classes)
void	operations_research::sat::MakeAllLiteralsPositive (LinearBooleanProblem *problem)
void	operations_research::sat::FindLinearBooleanProblemSymmetries (const LinearBooleanProblem &problem, std::vector< std::unique_ptr< SparsePermutation > > *generators)
void	operations_research::sat::ApplyLiteralMappingToBooleanProblem (const util_intops::StrongVector< LiteralIndex, LiteralIndex > &mapping, LinearBooleanProblem *problem)
void	operations_research::sat::ProbeAndSimplifyProblem (SatPostsolver *postsolver, LinearBooleanProblem *problem)
template<class Graph>
std::unique_ptr< Graph >	operations_research::sat::RemapGraph (const Graph &graph, absl::Span< const int > new_node_index)

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