OR-Tools  8.2
SatPostsolver

Detailed Description

Definition at line 47 of file simplification.h.

Public Member Functions

 SatPostsolver (int num_variables)
 
void Add (Literal x, const absl::Span< const Literal > clause)
 
void FixVariable (Literal x)
 
void ApplyMapping (const absl::StrongVector< BooleanVariable, BooleanVariable > &mapping)
 
std::vector< bool > ExtractAndPostsolveSolution (const SatSolver &solver)
 
std::vector< bool > PostsolveSolution (const std::vector< bool > &solution)
 
int NumClauses () const
 
std::vector< LiteralClause (int i) const
 

Constructor & Destructor Documentation

◆ SatPostsolver()

SatPostsolver ( int  num_variables)
explicit

Definition at line 38 of file simplification.cc.

Member Function Documentation

◆ Add()

void Add ( Literal  x,
const absl::Span< const Literal clause 
)

Definition at line 47 of file simplification.cc.

◆ ApplyMapping()

void ApplyMapping ( const absl::StrongVector< BooleanVariable, BooleanVariable > &  mapping)

Definition at line 62 of file simplification.cc.

◆ Clause()

std::vector<Literal> Clause ( int  i) const
inline

Definition at line 84 of file simplification.h.

◆ ExtractAndPostsolveSolution()

std::vector< bool > ExtractAndPostsolveSolution ( const SatSolver solver)

Definition at line 129 of file simplification.cc.

◆ FixVariable()

void FixVariable ( Literal  x)

Definition at line 57 of file simplification.cc.

◆ NumClauses()

int NumClauses ( ) const
inline

Definition at line 83 of file simplification.h.

◆ PostsolveSolution()

std::vector< bool > PostsolveSolution ( const std::vector< bool > &  solution)

Definition at line 140 of file simplification.cc.


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