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.

Return type: void

Arguments: Literal a, Literal b


Return type: void

Arguments: absl::Span<const Literal> clause


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

Arguments: ClauseIndex ci


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.


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.


Return type: int

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


Return type: int

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


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.


Return type: bool

Arguments: const std::vector<bool>& var_that_can_be_removed, bool log_info = false

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


Return type: void

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


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.


Return type: explicit

Arguments: SatPostsolver* postsolver


Return type: void

Arguments: DratProofHandler* drat_proof_handler


Return type: void

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

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


Return type: void

Arguments: int num_variables

Adds new clause to the SatPresolver.


Return type: void

Arguments: const SatParameters& params


Return type: void

Arguments: TimeLimit* time_limit


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