OR-Tools  9.6
Classes | Public Types | Public Member Functions | List of all members
SatPresolver

Detailed Description

Definition at line 146 of file simplification.h.

Public Types

typedef int32_t ClauseIndex
 

Public Member Functions

 SatPresolver (SatPostsolver *postsolver, SolverLogger *logger)
 
void SetParameters (const SatParameters &params)
 
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)
 
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)
 

Member Typedef Documentation

◆ ClauseIndex

typedef int32_t ClauseIndex

Definition at line 149 of file simplification.h.

Constructor & Destructor Documentation

◆ SatPresolver()

SatPresolver ( SatPostsolver *  postsolver,
SolverLogger *  logger 
)
inlineexplicit

Definition at line 151 of file simplification.h.

Member Function Documentation

◆ AddBinaryClause()

void AddBinaryClause ( Literal  a,
Literal  b 
)

Definition at line 169 of file simplification.cc.

◆ AddClause()

void AddClause ( absl::Span< const Literal >  clause)

Definition at line 171 of file simplification.cc.

◆ Clause()

const std::vector<Literal>& Clause ( ClauseIndex  ci) const
inline

Definition at line 186 of file simplification.h.

◆ CrossProduct()

bool CrossProduct ( Literal  x)

Definition at line 711 of file simplification.cc.

◆ LoadProblemIntoSatSolver()

void LoadProblemIntoSatSolver ( SatSolver *  solver)

Definition at line 271 of file simplification.cc.

◆ NumClauses()

int NumClauses ( ) const
inline

Definition at line 185 of file simplification.h.

◆ NumVariables()

int NumVariables ( ) const
inline

Definition at line 192 of file simplification.h.

◆ Presolve() [1/2]

bool Presolve ( )

Definition at line 329 of file simplification.cc.

◆ Presolve() [2/2]

bool Presolve ( const std::vector< bool > &  var_that_can_be_removed)

Definition at line 336 of file simplification.cc.

◆ PresolveWithBva()

void PresolveWithBva ( )

Definition at line 383 of file simplification.cc.

◆ ProcessClauseToSimplifyOthers()

bool ProcessClauseToSimplifyOthers ( ClauseIndex  clause_index)

Definition at line 635 of file simplification.cc.

◆ SetDratProofHandler()

void SetDratProofHandler ( DratProofHandler *  drat_proof_handler)
inline

Definition at line 225 of file simplification.h.

◆ SetEquivalentLiteralMapping()

void SetEquivalentLiteralMapping ( const absl::StrongVector< LiteralIndex, LiteralIndex > &  mapping)
inline

Definition at line 162 of file simplification.h.

◆ SetNumVariables()

void SetNumVariables ( int  num_variables)

Definition at line 226 of file simplification.cc.

◆ SetParameters()

void SetParameters ( const SatParameters &  params)
inline

Definition at line 157 of file simplification.h.

◆ SetTimeLimit()

void SetTimeLimit ( TimeLimit *  time_limit)
inline

Definition at line 158 of file simplification.h.

◆ VariableMapping()

absl::StrongVector< BooleanVariable, BooleanVariable > VariableMapping ( ) const

Definition at line 256 of file simplification.cc.

The documentation for this class was generated from the following files: