![]() |
Google OR-Tools v9.12
a fast and portable software suite for combinatorial optimization
|
#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 ¶ms) |
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) |
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.
Definition at line 148 of file simplification.h.
typedef int32_t operations_research::sat::SatPresolver::ClauseIndex |
Definition at line 151 of file simplification.h.
|
inlineexplicit |
Definition at line 153 of file simplification.h.
|
delete |
This type is neither copyable nor movable.
Definition at line 167 of file simplification.cc.
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 169 of file simplification.cc.
|
inline |
Definition at line 192 of file simplification.h.
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.
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.
Add all the resolvant clauses.
Deletes the old clauses.
Definition at line 711 of file simplification.cc.
void operations_research::sat::SatPresolver::LoadProblemIntoSatSolver | ( | SatSolver * | solver | ) |
Loads the current presolved problem in to the given sat solver.
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 269 of file simplification.cc.
|
inline |
All the clauses managed by this class.
Definition at line 191 of file simplification.h.
|
inline |
The number of variables. This is computed automatically from the clauses added to the SatPresolver.
Definition at line 198 of file simplification.h.
|
delete |
bool operations_research::sat::SatPresolver::Presolve | ( | ) |
Presolves the problem currently loaded. Returns false if the model is proven to be UNSAT during the presolving.
This is slighlty inefficient, but the presolve algorithm is a lot more costly anyway.
Definition at line 327 of file simplification.cc.
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.
We apply BVA after a pass of the other algorithms.
Definition at line 334 of file simplification.cc.
void operations_research::sat::SatPresolver::PresolveWithBva | ( | ) |
Visible for testing. Just applies the BVA step of the presolve.
Definition at line 382 of file simplification.cc.
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.
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().
Recompute signature.
Definition at line 635 of file simplification.cc.
|
inline |
Definition at line 232 of file simplification.h.
|
inline |
Registers a mapping to encode equivalent literals. See ProbeAndFindEquivalentLiteral().
Definition at line 168 of file simplification.h.
void operations_research::sat::SatPresolver::SetNumVariables | ( | int | num_variables | ) |
Adds new clause to the SatPresolver.
Definition at line 224 of file simplification.cc.
|
inline |
Definition at line 163 of file simplification.h.
|
inline |
Definition at line 164 of file simplification.h.
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 254 of file simplification.cc.