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.
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.
[[["Easy to understand","easyToUnderstand","thumb-up"],["Solved my problem","solvedMyProblem","thumb-up"],["Other","otherUp","thumb-up"]],[["Missing the information I need","missingTheInformationINeed","thumb-down"],["Too complicated / too many steps","tooComplicatedTooManySteps","thumb-down"],["Out of date","outOfDate","thumb-down"],["Samples / code issue","samplesCodeIssue","thumb-down"],["Other","otherDown","thumb-down"]],["Last updated 2024-08-06 UTC."],[[["\u003cp\u003eThe \u003ccode\u003eInprocessing\u003c/code\u003e class in C++ is used to store and manage information between SAT solver calls, potentially to be split into smaller components in the future.\u003c/p\u003e\n"],["\u003cp\u003eSome algorithms within this class may require adjustments to avoid conflicts with the main SAT search process.\u003c/p\u003e\n"],["\u003cp\u003eRefactoring may be necessary to integrate in-processing seamlessly within the SatSolver, potentially by extracting core functionalities or introducing a dedicated InprocessingSolve method.\u003c/p\u003e\n"],["\u003cp\u003eThe class provides various functionalities for simplifying and preprocessing the problem, including detecting equivalences, removing fixed variables, and strengthening clauses, all aimed at improving solver efficiency.\u003c/p\u003e\n"],["\u003cp\u003eThese in-processing techniques can be applied at different stages, such as during restarts or in a dedicated presolve loop, offering flexibility in their utilization.\u003c/p\u003e\n"]]],["The `Inprocessing` class manages information across calls and performs in-processing steps for SAT solving. Key actions include `DetectEquivalencesAndStamp` to find and propagate equivalences, `InprocessingRound` to decide and run in-processing during restarts, `LevelZeroPropagate` for clause attachment and propagation, `PresolveLoop` to simplify until a fix point, `RemoveFixedAndEquivalentVariables` to remove fixed variables and equivalences, and `SubsumeAndStrenghtenRound` to reduce clauses. The class also tracks new fixed variables and equivalences with `MoreFixedVariableToClean` and provides similar functionality with `MoreRedundantVariableToClean`.\n"],null,["# Inprocessing\n\nC++ Reference: class Inprocessing\n=================================\n\n\nNote: This documentation is automatically generated.\nWe 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. \n\nTODO(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. \n\nTODO(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.\n\n| Method ||\n|-------------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|\n| [`DetectEquivalencesAndStamp`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/sat_inprocessing.h#L128) | 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. |\n| [`Inprocessing`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/sat_inprocessing.h#L98) | Return type: `explicit ` Arguments: `Model* model` \u003cbr /\u003e |\n| [`InprocessingRound`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/sat_inprocessing.h#L120) | 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. |\n| [`LevelZeroPropagate`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/sat_inprocessing.h#L124) | Return type: `bool ` Simple wrapper that makes sure all the clauses are attached before a propagation is performed. |\n| [`MoreFixedVariableToClean`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/sat_inprocessing.h#L136) | Return type: `bool ` Returns true if there is new fixed variables or new equivalence relations since RemoveFixedAndEquivalentVariables() was last called. |\n| [`MoreRedundantVariableToClean`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/sat_inprocessing.h#L137) | Return type: `bool ` \u003cbr /\u003e |\n| [`PresolveLoop`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/sat_inprocessing.h#L115) | Return type: `bool ` Arguments: `SatPresolveOptions options` Does some simplifications until a fix point is reached or the given deterministic time is passed. |\n| [`RemoveFixedAndEquivalentVariables`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/sat_inprocessing.h#L132) | Return type: `bool ` Arguments: `bool log_info` Removes fixed variables and exploit equivalence relations to cleanup the clauses. Returns false if UNSAT. |\n| [`SubsumeAndStrenghtenRound`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/sat_inprocessing.h#L141) | 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. |"]]
