C++ Reference: class Inprocessing

Note: This documentation is automatically generated.

We need to keep some information from one call to the next, so we use a class. Note that as this becomes big, we can probably split it.

TODO(user): Some algorithms here use the normal SAT propagation engine. However we might want to temporarily disable activities/phase saving and so on if we want to run them as in-processing steps so that they do not "pollute" the normal SAT search.

TODO(user): For the propagation, this depends on the SatSolver class, which mean we cannot really use it without some refactoring as an in-processing from the SatSolver::Solve() function. So we do need a special InprocessingSolve() that lives outside SatSolver. Alternatively, we can extract the propagation main loop and conflict analysis from SatSolver.

Method
DetectEquivalencesAndStamp	Return type: bool Arguments: bool use_transitive_reduction, bool log_info Detects equivalences in the implication graph and propagates any failed literal found during the process.
Inprocessing	Return type: explicit Arguments: Model* model
InprocessingRound	Return type: bool When the option use_sat_inprocessing is true, then this is called at each restart. It is up to the heuristics here to decide what inprocessing we do or if we wait for the next call before doing anything.
LevelZeroPropagate	Return type: bool Simple wrapper that makes sure all the clauses are attached before a propagation is performed.
MoreFixedVariableToClean	Return type: bool Returns true if there is new fixed variables or new equivalence relations since RemoveFixedAndEquivalentVariables() was last called.
MoreRedundantVariableToClean	Return type: bool
PresolveLoop	Return type: bool Arguments: SatPresolveOptions options Does some simplifications until a fix point is reached or the given deterministic time is passed.
RemoveFixedAndEquivalentVariables	Return type: bool Arguments: bool log_info Removes fixed variables and exploit equivalence relations to cleanup the clauses. Returns false if UNSAT.
SubsumeAndStrenghtenRound	Return type: bool Arguments: bool log_info Processes all clauses and see if there is any subsumption/strenghtening reductions that can be performed. Returns false if UNSAT.