operations_research::sat::SatPostsolver Class Reference

Detailed Description

A simple sat postsolver.

The idea is that any presolve algorithm can just update this class, and at the end, this class will recover a solution of the initial problem from a solution of the presolved problem.

Definition at line 46 of file simplification.h.

#include <simplification.h>

Public Member Functions
	SatPostsolver (int num_variables)
	SatPostsolver (const SatPostsolver &)=delete
	This type is neither copyable nor movable.
SatPostsolver &	operator= (const SatPostsolver &)=delete
void	Add (Literal x, absl::Span< const Literal > clause)
void	FixVariable (Literal x)
void	ApplyMapping (const util_intops::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
const VariablesAssignment &	assignment ()

Constructor & Destructor Documentation

SatPostsolver() [1/2]

operations_research::sat::SatPostsolver::SatPostsolver ( int num_variables )

explicit

Definition at line 47 of file simplification.cc.

SatPostsolver() [2/2]

operations_research::sat::SatPostsolver::SatPostsolver ( const SatPostsolver & )

delete

This type is neither copyable nor movable.

Member Function Documentation

Add()

void operations_research::sat::SatPostsolver::Add	(	Literal	x,
		absl::Span< const Literal >	clause )

The postsolver will process the Add() calls in reverse order. If the given clause has all its literals at false, it simply sets the literal x to true.

Note

x must be a literal of the given clause.

Definition at line 56 of file simplification.cc.

ApplyMapping()

void operations_research::sat::SatPostsolver::ApplyMapping

(

const util_intops::StrongVector< BooleanVariable, BooleanVariable > &

mapping

)

This assumes that the given variable mapping has been applied to the problem. All the subsequent Add() and FixVariable() will refer to the new problem. During postsolve, the initial solution must also correspond to this new problem. Note that if mapping[v] == -1, then the literal v is assumed to be deleted.

This can be called more than once. But each call must refer to the current variables set (after all the previous mapping have been applied).

We have new variables.

Definition at line 71 of file simplification.cc.

assignment()

const VariablesAssignment & operations_research::sat::SatPostsolver::assignment ( )

inline

This will initially contains the Fixed variable. If PostsolveSolution() is called, it will contain the final solution.

Definition at line 108 of file simplification.h.

Clause()

std::vector< Literal > operations_research::sat::SatPostsolver::Clause ( int i ) const

inline

Todo

(user): we could avoid the copy here, but because clauses_literals_ is a deque, we do need a special return class and cannot just use absl::Span<Literal> for instance.

Definition at line 87 of file simplification.h.

ExtractAndPostsolveSolution()

std::vector< bool > operations_research::sat::SatPostsolver::ExtractAndPostsolveSolution

(

const SatSolver &

solver

)

Extracts the current assignment of the given solver and postsolve it.

Node(fdid): This can currently be called only once (but this is easy to change since only some CHECK will fail).

Definition at line 139 of file simplification.cc.

FixVariable()

void operations_research::sat::SatPostsolver::FixVariable

(

Literal

x

)

Tells the postsolver that the given literal must be true in any solution. We currently check that the variable is not already fixed.

Todo

(user): this as almost the same effect as adding an unit clause, and we should probably remove this to simplify the code.

Definition at line 66 of file simplification.cc.

NumClauses()

int operations_research::sat::SatPostsolver::NumClauses ( ) const

inline

Getters to the clauses managed by this class. Important: This will always put the associated literal first.

Definition at line 86 of file simplification.h.

operator=()

SatPostsolver & operations_research::sat::SatPostsolver::operator= ( const SatPostsolver & )

delete

PostsolveSolution()

std::vector< bool > operations_research::sat::SatPostsolver::PostsolveSolution

(

const std::vector< bool > &

solution

)

Definition at line 150 of file simplification.cc.

---

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

• ortools/sat/simplification.h
• ortools/sat/simplification.cc