OR-Tools  8.2
SatSolver Member List

This is the complete list of members for SatSolver, including all inherited members.

AddBinaryClause(Literal a, Literal b)SatSolver
AddBinaryClauses(const std::vector< BinaryClause > &clauses)SatSolver
AddClauseDuringSearch(absl::Span< const Literal > literals)SatSolver
AddLastPropagator(SatPropagator *propagator)SatSolver
AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)SatSolver
AddProblemClause(absl::Span< const Literal > literals)SatSolver
AddPropagator(SatPropagator *propagator)SatSolver
AddTernaryClause(Literal a, Literal b, Literal c)SatSolver
AddUnitClause(Literal true_literal)SatSolver
AdvanceDeterministicTime(TimeLimit *limit)SatSolverinline
AllPreferences() constSatSolverinline
Assignment() constSatSolverinline
AssumptionLevel() constSatSolverinline
ASSUMPTIONS_UNSAT enum valueSatSolver
Backtrack(int target_level)SatSolver
ClearNewlyAddedBinaryClauses()SatSolver
CurrentDecisionLevel() constSatSolverinline
Decisions() constSatSolverinline
deterministic_time() constSatSolver
EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)SatSolver
EnqueueDecisionAndBacktrackOnConflict(Literal true_literal)SatSolver
EnqueueDecisionIfNotConflicting(Literal true_literal)SatSolver
ExtractClauses(Output *out)SatSolverinline
FEASIBLE enum valueSatSolver
FinishPropagation()SatSolver
GetLastIncompatibleDecisions()SatSolver
INFEASIBLE enum valueSatSolver
IsModelUnsat() constSatSolverinline
LIMIT_REACHED enum valueSatSolver
LiteralTrail() constSatSolverinline
MinimizeSomeClauses(int decisions_budget)SatSolver
model()SatSolverinline
NewBooleanVariable()SatSolverinline
NewlyAddedBinaryClauses()SatSolver
NotifyThatModelIsUnsat()SatSolverinline
num_branches() constSatSolver
num_failures() constSatSolver
num_propagations() constSatSolver
num_restarts() constSatSolver
NumFixedVariables() constSatSolverinline
NumVariables() constSatSolverinline
parameters() constSatSolver
ProblemIsPureSat() constSatSolverinline
ProcessNewlyFixedVariables()SatSolver
Propagate()SatSolver
ReapplyAssumptionsIfNeeded()SatSolver
ResetAndSolveWithGivenAssumptions(const std::vector< Literal > &assumptions)SatSolver
ResetDecisionHeuristic()SatSolverinline
ResetDecisionHeuristicAndSetAllPreferences(const std::vector< std::pair< Literal, double >> &prefs)SatSolverinline
ResetToLevelZero()SatSolver
ResetWithGivenAssumptions(const std::vector< Literal > &assumptions)SatSolver
RestoreSolverToAssumptionLevel()SatSolver
SatSolver()SatSolver
SatSolver(Model *model)SatSolverexplicit
SaveDebugAssignment()SatSolver
SetAssignmentPreference(Literal literal, double weight)SatSolverinline
SetAssumptionLevel(int assumption_level)SatSolver
SetDratProofHandler(DratProofHandler *drat_proof_handler)SatSolverinline
SetNumVariables(int num_variables)SatSolver
SetParameters(const SatParameters &parameters)SatSolver
Solve()SatSolver
SolveWithTimeLimit(TimeLimit *time_limit)SatSolver
Status enum nameSatSolver
TakePropagatorOwnership(std::unique_ptr< SatPropagator > propagator)SatSolverinline
TrackBinaryClauses(bool value)SatSolverinline
UnsatStatus() constSatSolverinline
~SatSolver()SatSolver