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/meta/type_traits.h"
#include "absl/status/status.h"
#include "absl/strings/str_format.h"
#include "absl/strings/string_view.h"
#include "ortools/base/logging.h"
#include "ortools/graph/graph.h"
#include "ortools/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
	In SWIG mode, we don't want anything besides these top-level includes.
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)
	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.
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)

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

Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.