C++ Reference: class SatPresolver

Note: 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, SolverLogger* logger
SetDratProofHandler	Return type: void Arguments: DratProofHandler* drat_proof_handler
SetEquivalentLiteralMapping	Return type: void Arguments: const absl::StrongVector<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
SetTimeLimit	Return type: void Arguments: TimeLimit* time_limit
VariableMapping	Return type: absl::StrongVector<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).