boolean_problem.h File Reference

#include <memory>
#include <string>
#include <vector>
#include "absl/status/status.h"
#include "ortools/algorithms/sparse_permutation.h"
#include "ortools/base/strong_vector.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_solver.h"
#include "ortools/sat/simplification.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
CpModelProto	operations_research::sat::BooleanProblemToCpModelproto (const LinearBooleanProblem &problem)
double	operations_research::sat::AddOffsetAndScaleObjectiveValue (const LinearBooleanProblem &problem, Coefficient v)
	Adds the offset and returns the scaled version of the given objective value.
void	operations_research::sat::ChangeOptimizationDirection (LinearBooleanProblem *problem)
void	operations_research::sat::ExtractAssignment (const LinearBooleanProblem &problem, const SatSolver &solver, std::vector< bool > *assignment)
absl::Status	operations_research::sat::ValidateBooleanProblem (const LinearBooleanProblem &problem)
bool	operations_research::sat::LoadBooleanProblem (const LinearBooleanProblem &problem, SatSolver *solver)
	Loads a BooleanProblem into a given SatSolver instance.
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)
	Adds the constraint that the objective is smaller than the given upper bound.
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)
	Returns the objective value under the current assignment.
bool	operations_research::sat::IsAssignmentValid (const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
	Checks that an assignment is valid for the given BooleanProblem.
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, const std::vector< int > &constraint_indices, LinearBooleanProblem *subproblem)
	Constructs a sub-problem formed by the constraints with given indices.
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)