Small optimization: If a propagator does not contain any "constraints"
there is no point calling propagate on it. Before each propagation, the
solver will checks for emptiness, and construct an optimized list of
propagator before looping many time over the list.
Inspects the trail from propagation_trail_index_ until at least one literal
is propagated. Returns false iff a conflict is detected (in which case
trail->SetFailingClause() must be called).
This must update propagation_trail_index_ so that all the literals before
it have been propagated. In particular, if nothing was propagated, then
PropagationIsDone() must return true.
Explains why the literal at given trail_index was propagated by returning a
reason for this propagation. This will only be called for literals that are
on the trail and were propagated by this class.
The interpretation is that because all the literals of a reason were
assigned to false, we could deduce the assignment of the given variable.
The returned Span has to be valid until the literal is untrailed. A client
can use trail_.GetEmptyVectorToStoreReason() if it doesn't have a memory
location that already contains the reason.
Reverts the state so that all the literals with a trail index greater or
equal to the given one are not processed for propagation. Note that the
trail current decision level is already reverted before this is called.
TODO(user): Currently this is called at each Backtrack(), but we could
bundle the calls in case multiple conflict one after the other are detected
even before the Propagate() call of a SatPropagator is called.
TODO(user): It is not yet 100% the case, but this can be guaranteed to be
called with a trail index that will always be the start of a new decision
level.
[[["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\u003e\u003ccode\u003eSatPropagator\u003c/code\u003e is a base class for defining SAT constraints within the OR-Tools solver.\u003c/p\u003e\n"],["\u003cp\u003eIt provides essential methods like \u003ccode\u003ePropagate\u003c/code\u003e for constraint enforcement and \u003ccode\u003eReason\u003c/code\u003e for explaining propagation decisions.\u003c/p\u003e\n"],["\u003cp\u003ePropagators interact with the solver's trail to track variable assignments and detect conflicts.\u003c/p\u003e\n"],["\u003cp\u003eKey functionalities include checking for emptiness (\u003ccode\u003eIsEmpty\u003c/code\u003e), confirming propagation completion (\u003ccode\u003ePropagationIsDone\u003c/code\u003e), and reverting state during backtracking (\u003ccode\u003eUntrail\u003c/code\u003e).\u003c/p\u003e\n"],["\u003cp\u003eEach propagator is uniquely identified using \u003ccode\u003ePropagatorId\u003c/code\u003e.\u003c/p\u003e\n"]]],["The `SatPropagator` class serves as a base for SAT constraints. Key actions include: `Propagate`, which inspects the trail to propagate literals and detect conflicts; `IsEmpty`, checking for the absence of constraints to optimize propagation; `Reason`, explaining why a literal was propagated; and `Untrail`, reverting the state to before a specific trail index. Other methods manage the propagator's unique ID, check if preconditions are met, and verify if all literals have been inspected.\n"],null,[]]
