| AddBinaryClause(Literal a, Literal b) | operations_research::sat::SatSolver | |
| AddBinaryClauses(absl::Span< const BinaryClause > clauses) | operations_research::sat::SatSolver | |
| AddClauseDuringSearch(absl::Span< const Literal > literals) | operations_research::sat::SatSolver | |
| AddLastPropagator(SatPropagator *propagator) | operations_research::sat::SatSolver | |
| AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst) | operations_research::sat::SatSolver | |
| AddProblemClause(absl::Span< const Literal > literals) | operations_research::sat::SatSolver | |
| AddPropagator(SatPropagator *propagator) | operations_research::sat::SatSolver | |
| AddTernaryClause(Literal a, Literal b, Literal c) | operations_research::sat::SatSolver | |
| AddUnitClause(Literal true_literal) | operations_research::sat::SatSolver | |
| AdvanceDeterministicTime(TimeLimit *limit) | operations_research::sat::SatSolver | inline |
| AllPreferences() const | operations_research::sat::SatSolver | inline |
| Assignment() const | operations_research::sat::SatSolver | inline |
| AssumptionLevel() const | operations_research::sat::SatSolver | inline |
| ASSUMPTIONS_UNSAT enum value | operations_research::sat::SatSolver | |
| Backtrack(int target_level) | operations_research::sat::SatSolver | |
| ClearNewlyAddedBinaryClauses() | operations_research::sat::SatSolver | |
| counters() const | operations_research::sat::SatSolver | inline |
| CurrentDecisionLevel() const | operations_research::sat::SatSolver | inline |
| Decisions() const | operations_research::sat::SatSolver | inline |
| deterministic_time() const | operations_research::sat::SatSolver | |
| EnqueueDecisionAndBackjumpOnConflict(Literal true_literal) | operations_research::sat::SatSolver | |
| EnqueueDecisionAndBacktrackOnConflict(Literal true_literal, int *first_propagation_index=nullptr) | operations_research::sat::SatSolver | |
| EnqueueDecisionIfNotConflicting(Literal true_literal) | operations_research::sat::SatSolver | |
| EnsureNewClauseIndexInitialized() | operations_research::sat::SatSolver | inline |
| ExtractClauses(Output *out) | operations_research::sat::SatSolver | inline |
| FEASIBLE enum value | operations_research::sat::SatSolver | |
| FinishPropagation() | operations_research::sat::SatSolver | |
| GetDecisionsFixing(absl::Span< const Literal > literals) | operations_research::sat::SatSolver | |
| GetLastIncompatibleDecisions() | operations_research::sat::SatSolver | |
| INFEASIBLE enum value | operations_research::sat::SatSolver | |
| LIMIT_REACHED enum value | operations_research::sat::SatSolver | |
| LiteralTrail() const | operations_research::sat::SatSolver | inline |
| LoadDebugSolution(absl::Span< const Literal > solution) | operations_research::sat::SatSolver | |
| MinimizeByPropagation(double dtime, bool minimize_new_clauses_only=false) | operations_research::sat::SatSolver | |
| model() | operations_research::sat::SatSolver | inline |
| ModelIsUnsat() const | operations_research::sat::SatSolver | inline |
| mutable_logger() | operations_research::sat::SatSolver | inline |
| NewBooleanVariable() | operations_research::sat::SatSolver | inline |
| NewlyAddedBinaryClauses() | operations_research::sat::SatSolver | |
| NotifyThatModelIsUnsat() | operations_research::sat::SatSolver | inline |
| num_backtracks() const | operations_research::sat::SatSolver | |
| num_branches() const | operations_research::sat::SatSolver | |
| num_failures() const | operations_research::sat::SatSolver | |
| num_propagations() const | operations_research::sat::SatSolver | |
| num_restarts() const | operations_research::sat::SatSolver | |
| NumFixedVariables() const | operations_research::sat::SatSolver | inline |
| NumVariables() const | operations_research::sat::SatSolver | inline |
| operator=(const SatSolver &)=delete | operations_research::sat::SatSolver | |
| parameters() const | operations_research::sat::SatSolver | |
| ProcessCurrentConflict() | operations_research::sat::SatSolver | |
| ProcessNewlyFixedVariables() | operations_research::sat::SatSolver | |
| Propagate() | operations_research::sat::SatSolver | |
| ReapplyAssumptionsIfNeeded() | operations_research::sat::SatSolver | |
| ResetAndSolveWithGivenAssumptions(const std::vector< Literal > &assumptions, int64_t max_number_of_conflicts=-1) | operations_research::sat::SatSolver | |
| ResetDecisionHeuristic() | operations_research::sat::SatSolver | inline |
| ResetToLevelZero() | operations_research::sat::SatSolver | |
| ResetWithGivenAssumptions(const std::vector< Literal > &assumptions) | operations_research::sat::SatSolver | |
| RestoreSolverToAssumptionLevel() | operations_research::sat::SatSolver | |
| SatSolver() | operations_research::sat::SatSolver | |
| SatSolver(Model *model) | operations_research::sat::SatSolver | explicit |
| SatSolver(const SatSolver &)=delete | operations_research::sat::SatSolver | |
| SaveDebugAssignment() | operations_research::sat::SatSolver | |
| SetAssignmentPreference(Literal literal, float weight) | operations_research::sat::SatSolver | inline |
| SetAssumptionLevel(int assumption_level) | operations_research::sat::SatSolver | |
| SetDratProofHandler(DratProofHandler *drat_proof_handler) | operations_research::sat::SatSolver | inline |
| SetNumVariables(int num_variables) | operations_research::sat::SatSolver | |
| SetParameters(const SatParameters ¶meters) | operations_research::sat::SatSolver | |
| Solve() | operations_research::sat::SatSolver | |
| SolveWithTimeLimit(TimeLimit *time_limit) | operations_research::sat::SatSolver | |
| Status enum name | operations_research::sat::SatSolver | |
| TakePropagatorOwnership(std::unique_ptr< SatPropagator > propagator) | operations_research::sat::SatSolver | inline |
| TrackBinaryClauses(bool value) | operations_research::sat::SatSolver | inline |
| UnsatStatus() const | operations_research::sat::SatSolver | inline |
| ~SatSolver() | operations_research::sat::SatSolver | |
1.14.0