![]() |
OR-Tools
8.2
|
Definition at line 143 of file simplification.h.
Public Types | |
typedef int32 | ClauseIndex |
Public Member Functions | |
SatPresolver (SatPostsolver *postsolver) | |
void | SetParameters (const SatParameters ¶ms) |
void | SetTimeLimit (TimeLimit *time_limit) |
void | SetEquivalentLiteralMapping (const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping) |
void | SetNumVariables (int num_variables) |
void | AddBinaryClause (Literal a, Literal b) |
void | AddClause (absl::Span< const Literal > clause) |
bool | Presolve () |
bool | Presolve (const std::vector< bool > &var_that_can_be_removed, bool log_info=false) |
int | NumClauses () const |
const std::vector< Literal > & | Clause (ClauseIndex ci) const |
int | NumVariables () const |
absl::StrongVector< BooleanVariable, BooleanVariable > | VariableMapping () const |
void | LoadProblemIntoSatSolver (SatSolver *solver) |
bool | ProcessClauseToSimplifyOthers (ClauseIndex clause_index) |
bool | CrossProduct (Literal x) |
void | PresolveWithBva () |
void | SetDratProofHandler (DratProofHandler *drat_proof_handler) |
typedef int32 ClauseIndex |
Definition at line 146 of file simplification.h.
|
inlineexplicit |
Definition at line 148 of file simplification.h.
Definition at line 159 of file simplification.cc.
void AddClause | ( | absl::Span< const Literal > | clause | ) |
Definition at line 161 of file simplification.cc.
|
inline |
Definition at line 183 of file simplification.h.
bool CrossProduct | ( | Literal | x | ) |
Definition at line 701 of file simplification.cc.
void LoadProblemIntoSatSolver | ( | SatSolver * | solver | ) |
Definition at line 261 of file simplification.cc.
|
inline |
Definition at line 182 of file simplification.h.
|
inline |
Definition at line 189 of file simplification.h.
bool Presolve | ( | ) |
Definition at line 319 of file simplification.cc.
bool Presolve | ( | const std::vector< bool > & | var_that_can_be_removed, |
bool | log_info = false |
||
) |
Definition at line 326 of file simplification.cc.
void PresolveWithBva | ( | ) |
Definition at line 373 of file simplification.cc.
bool ProcessClauseToSimplifyOthers | ( | ClauseIndex | clause_index | ) |
Definition at line 625 of file simplification.cc.
|
inline |
Definition at line 222 of file simplification.h.
|
inline |
Definition at line 158 of file simplification.h.
void SetNumVariables | ( | int | num_variables | ) |
Definition at line 216 of file simplification.cc.
|
inline |
Definition at line 153 of file simplification.h.
|
inline |
Definition at line 154 of file simplification.h.
absl::StrongVector< BooleanVariable, BooleanVariable > VariableMapping | ( | ) | const |
Definition at line 246 of file simplification.cc.