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."],[[["The `Inprocessing` class in C++ is used to store and manage information between SAT solver calls, potentially to be split into smaller components in the future."],["Some algorithms within this class may require adjustments to avoid conflicts with the main SAT search process."],["Refactoring may be necessary to integrate in-processing seamlessly within the SatSolver, potentially by extracting core functionalities or introducing a dedicated InprocessingSolve method."],["The 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."],["These in-processing techniques can be applied at different stages, such as during restarts or in a dedicated presolve loop, offering flexibility in their utilization."]]],["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"]]
