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)
SatSolver
inline
AllPreferences
() const
SatSolver
inline
Assignment
() const
SatSolver
inline
AssumptionLevel
() const
SatSolver
inline
ASSUMPTIONS_UNSAT
enum value
SatSolver
Backtrack
(int target_level)
SatSolver
ClearNewlyAddedBinaryClauses
()
SatSolver
CurrentDecisionLevel
() const
SatSolver
inline
Decisions
() const
SatSolver
inline
deterministic_time
() const
SatSolver
EnqueueDecisionAndBackjumpOnConflict
(Literal true_literal)
SatSolver
EnqueueDecisionAndBacktrackOnConflict
(Literal true_literal)
SatSolver
EnqueueDecisionIfNotConflicting
(Literal true_literal)
SatSolver
ExtractClauses
(Output *out)
SatSolver
inline
FEASIBLE
enum value
SatSolver
FinishPropagation
()
SatSolver
GetLastIncompatibleDecisions
()
SatSolver
INFEASIBLE
enum value
SatSolver
IsModelUnsat
() const
SatSolver
inline
LIMIT_REACHED
enum value
SatSolver
LiteralTrail
() const
SatSolver
inline
MinimizeSomeClauses
(int decisions_budget)
SatSolver
model
()
SatSolver
inline
NewBooleanVariable
()
SatSolver
inline
NewlyAddedBinaryClauses
()
SatSolver
NotifyThatModelIsUnsat
()
SatSolver
inline
num_branches
() const
SatSolver
num_failures
() const
SatSolver
num_propagations
() const
SatSolver
num_restarts
() const
SatSolver
NumFixedVariables
() const
SatSolver
inline
NumVariables
() const
SatSolver
inline
parameters
() const
SatSolver
ProblemIsPureSat
() const
SatSolver
inline
ProcessNewlyFixedVariables
()
SatSolver
Propagate
()
SatSolver
ReapplyAssumptionsIfNeeded
()
SatSolver
ResetAndSolveWithGivenAssumptions
(const std::vector< Literal > &assumptions)
SatSolver
ResetDecisionHeuristic
()
SatSolver
inline
ResetDecisionHeuristicAndSetAllPreferences
(const std::vector< std::pair< Literal, double >> &prefs)
SatSolver
inline
ResetToLevelZero
()
SatSolver
ResetWithGivenAssumptions
(const std::vector< Literal > &assumptions)
SatSolver
RestoreSolverToAssumptionLevel
()
SatSolver
SatSolver
()
SatSolver
SatSolver
(Model *model)
SatSolver
explicit
SaveDebugAssignment
()
SatSolver
SetAssignmentPreference
(Literal literal, double weight)
SatSolver
inline
SetAssumptionLevel
(int assumption_level)
SatSolver
SetDratProofHandler
(DratProofHandler *drat_proof_handler)
SatSolver
inline
SetNumVariables
(int num_variables)
SatSolver
SetParameters
(const SatParameters ¶meters)
SatSolver
Solve
()
SatSolver
SolveWithTimeLimit
(TimeLimit *time_limit)
SatSolver
Status
enum name
SatSolver
TakePropagatorOwnership
(std::unique_ptr< SatPropagator > propagator)
SatSolver
inline
TrackBinaryClauses
(bool value)
SatSolver
inline
UnsatStatus
() const
SatSolver
inline
~SatSolver
()
SatSolver
Generated by
1.9.1