OR-Tools  8.2
SatPresolver

Detailed Description

Definition at line 143 of file simplification.h.

Public Types

typedef int32 ClauseIndex
 

Public Member Functions

 SatPresolver (SatPostsolver *postsolver)
 
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, 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)
 

Member Typedef Documentation

◆ ClauseIndex

typedef int32 ClauseIndex

Definition at line 146 of file simplification.h.

Constructor & Destructor Documentation

◆ SatPresolver()

SatPresolver ( SatPostsolver postsolver)
inlineexplicit

Definition at line 148 of file simplification.h.

Member Function Documentation

◆ AddBinaryClause()

void AddBinaryClause ( Literal  a,
Literal  b 
)

Definition at line 159 of file simplification.cc.

◆ AddClause()

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

Definition at line 161 of file simplification.cc.

◆ Clause()

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

Definition at line 183 of file simplification.h.

◆ CrossProduct()

bool CrossProduct ( Literal  x)

Definition at line 701 of file simplification.cc.

◆ LoadProblemIntoSatSolver()

void LoadProblemIntoSatSolver ( SatSolver solver)

Definition at line 261 of file simplification.cc.

◆ NumClauses()

int NumClauses ( ) const
inline

Definition at line 182 of file simplification.h.

◆ NumVariables()

int NumVariables ( ) const
inline

Definition at line 189 of file simplification.h.

◆ Presolve() [1/2]

bool Presolve ( )

Definition at line 319 of file simplification.cc.

◆ Presolve() [2/2]

bool Presolve ( const std::vector< bool > &  var_that_can_be_removed,
bool  log_info = false 
)

Definition at line 326 of file simplification.cc.

◆ PresolveWithBva()

void PresolveWithBva ( )

Definition at line 373 of file simplification.cc.

◆ ProcessClauseToSimplifyOthers()

bool ProcessClauseToSimplifyOthers ( ClauseIndex  clause_index)

Definition at line 625 of file simplification.cc.

◆ SetDratProofHandler()

void SetDratProofHandler ( DratProofHandler drat_proof_handler)
inline

Definition at line 222 of file simplification.h.

◆ SetEquivalentLiteralMapping()

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

Definition at line 158 of file simplification.h.

◆ SetNumVariables()

void SetNumVariables ( int  num_variables)

Definition at line 216 of file simplification.cc.

◆ SetParameters()

void SetParameters ( const SatParameters &  params)
inline

Definition at line 153 of file simplification.h.

◆ SetTimeLimit()

void SetTimeLimit ( TimeLimit time_limit)
inline

Definition at line 154 of file simplification.h.

◆ VariableMapping()

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

Definition at line 246 of file simplification.cc.


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