C++ Reference: class SatPresolver

This documentation is automatically generated.

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 that 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.
Method
AddBinaryClause

Return type: void

Arguments: Literal a, Literal b

AddClause

Return type: void

Arguments: absl::Span<const Literal> clause

Clause

Return type: const std::vector<Literal>&

Arguments: ClauseIndex ci

CrossProduct

Return type: bool

Arguments: 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.

LoadProblemIntoSatSolver

Return type: void

Arguments: SatSolver* solver

Loads the current presolved problem in to the given sat solver. Note that 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.

NumClauses

Return type: int

All the clauses managed by this class. Note that deleted clauses keep their indices (they are just empty).

NumVariables

Return type: int

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

Presolve

Return type: bool

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.

Presolve

Return type: bool

Arguments: 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.

PresolveWithBva

Return type: void

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

ProcessClauseToSimplifyOthers

Return type: bool

Arguments: 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.

SatPresolver

Return type: explicit

Arguments: SatPostsolver* postsolver

SetDratProofHandler

Return type: void

Arguments: DratProofHandler* drat_proof_handler

SetEquivalentLiteralMapping

Return type: void

Arguments: const gtl::ITIVector<LiteralIndex, LiteralIndex>& mapping

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

SetNumVariables

Return type: void

Arguments: int num_variables

Adds new clause to the SatPresolver.

SetParameters

Return type: void

Arguments: const SatParameters& params

VariableMapping

Return type: gtl::ITIVector<BooleanVariable, BooleanVariable>

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).