Definition at line 57 of file sat_solver.h.
|
| SatSolver () |
|
| SatSolver (Model *model) |
|
| ~SatSolver () |
|
Model * | model () |
|
void | SetParameters (const SatParameters ¶meters) |
|
const SatParameters & | parameters () const |
|
void | SetNumVariables (int num_variables) |
|
int | NumVariables () const |
|
BooleanVariable | NewBooleanVariable () |
|
bool | AddUnitClause (Literal true_literal) |
|
bool | AddBinaryClause (Literal a, Literal b) |
|
bool | AddTernaryClause (Literal a, Literal b, Literal c) |
|
bool | AddProblemClause (absl::Span< const Literal > literals) |
|
bool | AddLinearConstraint (bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst) |
|
bool | IsModelUnsat () const |
|
void | AddPropagator (SatPropagator *propagator) |
|
void | AddLastPropagator (SatPropagator *propagator) |
|
void | TakePropagatorOwnership (std::unique_ptr< SatPropagator > propagator) |
|
void | SetAssignmentPreference (Literal literal, double weight) |
|
std::vector< std::pair< Literal, double > > | AllPreferences () const |
|
void | ResetDecisionHeuristic () |
|
void | ResetDecisionHeuristicAndSetAllPreferences (const std::vector< std::pair< Literal, double >> &prefs) |
|
Status | Solve () |
|
Status | SolveWithTimeLimit (TimeLimit *time_limit) |
|
Status | ResetAndSolveWithGivenAssumptions (const std::vector< Literal > &assumptions) |
|
void | SetAssumptionLevel (int assumption_level) |
|
int | AssumptionLevel () const |
|
std::vector< Literal > | GetLastIncompatibleDecisions () |
|
int | EnqueueDecisionAndBackjumpOnConflict (Literal true_literal) |
|
int | EnqueueDecisionAndBacktrackOnConflict (Literal true_literal) |
|
bool | EnqueueDecisionIfNotConflicting (Literal true_literal) |
|
void | Backtrack (int target_level) |
|
bool | RestoreSolverToAssumptionLevel () |
|
bool | FinishPropagation () |
|
bool | ResetToLevelZero () |
|
bool | ResetWithGivenAssumptions (const std::vector< Literal > &assumptions) |
|
bool | ReapplyAssumptionsIfNeeded () |
|
Status | UnsatStatus () const |
|
template<typename Output > |
void | ExtractClauses (Output *out) |
|
void | TrackBinaryClauses (bool value) |
|
bool | AddBinaryClauses (const std::vector< BinaryClause > &clauses) |
|
const std::vector< BinaryClause > & | NewlyAddedBinaryClauses () |
|
void | ClearNewlyAddedBinaryClauses () |
|
const std::vector< Decision > & | Decisions () const |
|
int | CurrentDecisionLevel () const |
|
const Trail & | LiteralTrail () const |
|
const VariablesAssignment & | Assignment () const |
|
int64 | num_branches () const |
|
int64 | num_failures () const |
|
int64 | num_propagations () const |
|
int64 | num_restarts () const |
|
double | deterministic_time () const |
|
void | SaveDebugAssignment () |
|
bool | ProblemIsPureSat () const |
|
void | SetDratProofHandler (DratProofHandler *drat_proof_handler) |
|
void | NotifyThatModelIsUnsat () |
|
bool | AddClauseDuringSearch (absl::Span< const Literal > literals) |
|
bool | Propagate () |
|
void | MinimizeSomeClauses (int decisions_budget) |
|
void | AdvanceDeterministicTime (TimeLimit *limit) |
|
void | ProcessNewlyFixedVariables () |
|
int64 | NumFixedVariables () const |
|