Go to the source code of this file.
|  | 
| void | operations_research::sat::MinimizeCoreWithPropagation (TimeLimit *limit, SatSolver *solver, std::vector< Literal > *core) | 
| void | operations_research::sat::MinimizeCoreWithSearch (TimeLimit *limit, SatSolver *solver, std::vector< Literal > *core) | 
| bool | operations_research::sat::ProbeLiteral (Literal assumption, SatSolver *solver) | 
| void | operations_research::sat::FilterAssignedLiteral (const VariablesAssignment &assignment, std::vector< Literal > *core) | 
|  | A core cannot be all true. 
 | 
| SatSolver::Status | operations_research::sat::MinimizeIntegerVariableWithLinearScanAndLazyEncoding (IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model) | 
| void | operations_research::sat::RestrictObjectiveDomainWithBinarySearch (IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model) | 
| void | operations_research::sat::PresolveBooleanLinearExpression (std::vector< Literal > *literals, std::vector< Coefficient > *coefficients, Coefficient *offset) |