Detailed Description

This class holds a SAT problem (i.e. a set of clauses) and the logic to presolve it by a series of subsumption, self-subsuming resolution, and variable elimination by clause distribution.

Note: this does propagate unit-clauses, but probably much less efficiently than the propagation code in the SAT solver. So it is better to use a SAT solver to fix variables before using this class.

Todo: (user): Interact more with a SAT solver to reuse its propagation logic.

Todo: (user): Forbid the removal of some variables. This way we can presolve only the clause part of a general Boolean problem by not removing variables appearing in pseudo-Boolean constraints.

Definition at line 149 of file simplification.h.

#include <simplification.h>

Public Types
typedef int32_t	ClauseIndex

Public Member Functions
	SatPresolver (SatPostsolver postsolver, SolverLogger logger)
	SatPresolver (const SatPresolver &)=delete
	This type is neither copyable nor movable.
SatPresolver &	operator= (const SatPresolver &)=delete
void	SetParameters (const SatParameters &params)
void	SetTimeLimit (TimeLimit *time_limit)
void	SetEquivalentLiteralMapping (const util_intops::StrongVector< LiteralIndex, LiteralIndex > &mapping)
void	SetNumVariables (int num_variables)
	Adds new clause to the SatPresolver.
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
util_intops::StrongVector< BooleanVariable, BooleanVariable >	VariableMapping () const
void	LoadProblemIntoSatSolver (SatSolver *solver)
bool	ProcessClauseToSimplifyOthers (ClauseIndex clause_index)
bool	CrossProduct (Literal x)
void	PresolveWithBva ()
	Visible for testing. Just applies the BVA step of the presolve.
void	SetDratProofHandler (DratProofHandler *drat_proof_handler)

Member Typedef Documentation

◆ ClauseIndex

typedef int32_t operations_research::sat::SatPresolver::ClauseIndex

Todo: (user): use IntType!

Definition at line 152 of file simplification.h.

Constructor & Destructor Documentation

◆ SatPresolver() [1/2]

operations_research::sat::SatPresolver::SatPresolver	(	SatPostsolver *	postsolver,
		SolverLogger *	logger )

inlineexplicit

Definition at line 154 of file simplification.h.

◆ SatPresolver() [2/2]

operations_research::sat::SatPresolver::SatPresolver ( const SatPresolver & )

delete

This type is neither copyable nor movable.

Member Function Documentation

◆ AddBinaryClause()

void operations_research::sat::SatPresolver::AddBinaryClause	(	Literal	a,
		Literal	b )

Definition at line 169 of file simplification.cc.

◆ AddClause()

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

Check for trivial clauses:

The clause is trivial!

This needs to be done after the basic canonicalization above.

Definition at line 171 of file simplification.cc.

◆ Clause()

const std::vector< Literal > & operations_research::sat::SatPresolver::Clause ( ClauseIndex ci ) const

inline

Definition at line 193 of file simplification.h.

◆ CrossProduct()

bool operations_research::sat::SatPresolver::CrossProduct ( Literal x )

Visible for testing. Tries to eliminate x by clause distribution. This is also known as bounded variable elimination.

It is always possible to remove x by resolving each clause containing x with all the clauses containing not(x). Hence the cross-product name. Note that this function only do that if the number of clauses is reduced.

Note: if s1 or s2 is equal to 0, this function will implicitly just fix the variable x.

Heuristic. Abort if the work required to decide if x should be removed seems to big.

Compute the threshold under which we don't remove x.Variable().

For the BCE, we prefer s2 to be small.

Test whether we should remove the x.Variable().

Abort early if the "size" become too big.

This is an incomplete heuristic for blocked clause detection. Here, the clause i is "blocked", so we can remove it. Note that the code below already do that if we decide to eliminate x.

For more details, see the paper "Blocked clause elimination", Matti Jarvisalo, Armin Biere, Marijn Heule. TACAS, volume 6015 of Lecture Notes in Computer Science, pages 129–144. Springer, 2010.

Todo: (user): Choose if we use x or x.Negated() depending on the list sizes? The function achieve the same if x = x.Negated(), however the loops are not done in the same order which may change this incomplete "blocked" clause detection.

Add all the resolvant clauses.

Note: the variable priority queue will only be updated during the deletion.

Deletes the old clauses.

Todo: (user): We could only update the priority queue once for each variable instead of doing it many times.

Todo: (user): At this point x.Variable() is added back to the priority queue. Avoid doing that.

Definition at line 738 of file simplification.cc.

◆ LoadProblemIntoSatSolver()

void operations_research::sat::SatPresolver::LoadProblemIntoSatSolver ( SatSolver * solver )

Loads the current presolved problem in to the given sat solver.

Note: the variables will be re-indexed according to the mapping given by GetMapping() so that they form a dense set.

IMPORTANT: This is not const because it deletes the presolver clauses as they are added to the SatSolver in order to save memory. After this is called, only VariableMapping() will still works.

Cleanup some memory that is not needed anymore. Note that we do need literal_to_clause_sizes_ for VariableMapping() to work.

Definition at line 283 of file simplification.cc.

◆ NumClauses()

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

inline

All the clauses managed by this class.

Note: deleted clauses keep their indices (they are just empty).

Definition at line 192 of file simplification.h.

◆ NumVariables()

int operations_research::sat::SatPresolver::NumVariables ( ) const

inline

The number of variables. This is computed automatically from the clauses added to the SatPresolver.

Definition at line 199 of file simplification.h.

◆ operator=()

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

delete

◆ Presolve() [1/2]

bool operations_research::sat::SatPresolver::Presolve ( )

Presolves the problem currently loaded. Returns false if the model is proven to be UNSAT during the presolving.

Todo: (user): Add support for a time limit and some kind of iterations limit so that this can never take too much time.

This is slighlty inefficient, but the presolve algorithm is a lot more costly anyway.

Definition at line 341 of file simplification.cc.

◆ Presolve() [2/2]

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

Same as Presolve() but only allow to remove BooleanVariable whose index is set to true in the given vector.

Todo: (user): When a clause is strengthened, add it to a queue so it can be processed again?

We apply BVA after a pass of the other algorithms.

Definition at line 348 of file simplification.cc.

◆ PresolveWithBva()

void operations_research::sat::SatPresolver::PresolveWithBva ( )

Visible for testing. Just applies the BVA step of the presolve.

Todo: (user): Put work limit in place !

Definition at line 400 of file simplification.cc.

◆ ProcessClauseToSimplifyOthers()

bool operations_research::sat::SatPresolver::ProcessClauseToSimplifyOthers ( ClauseIndex clause_index )

Visible for Testing. Takes a given clause index and looks for clause that can be subsumed or strengthened using this clause. Returns false if the model is proven to be unsat.

Todo: (user): Binary clauses are really common, and we can probably do this more efficiently for them. For instance, we could just take the intersection of two sorted lists to get the simplified clauses.

If there is another "short" occurrence list, use it. Otherwise use the one corresponding to the negation of lit.

Treat the clauses containing lit.Negated().

Todo: (user): not super optimal since we could abort earlier if opposite_literal is not the negation of shortest_list. Note that this applies to the second call to ProcessClauseToSimplifyOthersUsingLiteral() above too.

Todo: (user): remove the old clauses_[ci] afterwards.

Recompute signature.

Definition at line 653 of file simplification.cc.

◆ SetDratProofHandler()

void operations_research::sat::SatPresolver::SetDratProofHandler ( DratProofHandler * drat_proof_handler )

inline

Definition at line 233 of file simplification.h.

◆ SetEquivalentLiteralMapping()

void operations_research::sat::SatPresolver::SetEquivalentLiteralMapping ( const util_intops::StrongVector< LiteralIndex, LiteralIndex > & mapping )

inline

Registers a mapping to encode equivalent literals. See ProbeAndFindEquivalentLiteral().

Definition at line 169 of file simplification.h.

◆ SetNumVariables()

void operations_research::sat::SatPresolver::SetNumVariables ( int num_variables )

Adds new clause to the SatPresolver.

Definition at line 226 of file simplification.cc.

◆ SetParameters()

void operations_research::sat::SatPresolver::SetParameters ( const SatParameters & params )

inline

Definition at line 164 of file simplification.h.

◆ SetTimeLimit()

void operations_research::sat::SatPresolver::SetTimeLimit ( TimeLimit * time_limit )

inline

Definition at line 165 of file simplification.h.

◆ VariableMapping()

util_intops::StrongVector< BooleanVariable, BooleanVariable > operations_research::sat::SatPresolver::VariableMapping ( ) const

After presolving, Some variables in [0, NumVariables()) have no longer any clause pointing to them. This return a mapping that maps this interval to [0, new_size) such that now all variables are used. The unused variable will be mapped to BooleanVariable(-1).

Definition at line 268 of file simplification.cc.

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

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

Detailed Description

Public Types

Public Member Functions

Member Typedef Documentation

◆ ClauseIndex

Constructor & Destructor Documentation

◆ SatPresolver() [1/2]

◆ SatPresolver() [2/2]

Member Function Documentation

◆ AddBinaryClause()

◆ AddClause()

◆ Clause()

◆ CrossProduct()

◆ LoadProblemIntoSatSolver()

◆ NumClauses()

◆ NumVariables()

◆ operator=()

◆ Presolve() [1/2]

◆ Presolve() [2/2]

◆ PresolveWithBva()

◆ ProcessClauseToSimplifyOthers()

◆ SetDratProofHandler()

◆ SetEquivalentLiteralMapping()

◆ SetNumVariables()

◆ SetParameters()

◆ SetTimeLimit()

◆ VariableMapping()