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< Literal >	Clause (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:

• simplification.h
• simplification.cc