Stay organized with collections Save and categorize content based on your preferences.

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.

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.


Return type: explicit

Arguments: Model* model


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.


Return type: bool

Simple wrapper that makes sure all the clauses are attached before a propagation is performed.


Return type: bool

Returns true if there is new fixed variables or new equivalence relations since RemoveFixedAndEquivalentVariables() was last called.


Return type: bool


Return type: bool

Arguments: SatPresolveOptions options

Does some simplifications until a fix point is reached or the given deterministic time is passed.


Return type: bool

Arguments: bool log_info

Removes fixed variables and exploit equivalence relations to cleanup the clauses. Returns false if UNSAT.


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.