C++ Reference: class SatPropagator

Note: This documentation is automatically generated.

Base class for all the SAT constraints.

Method
IsEmpty	Return type: virtual bool 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.
Propagate	Return type: virtual bool Arguments: Trail* trail 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.
PropagatePreconditionsAreSatisfied	Return type: bool Arguments: const Trail& trail Returns true if all the preconditions for Propagate() are satisfied. This is just meant to be used in a DCHECK.
PropagationIsDone	Return type: bool Arguments: const Trail& trail Returns true iff all the trail was inspected by this propagator.
PropagatorId	Return type: int
Reason	Return type: virtual absl::Span<const Literal> Arguments: const Trail& trail, int trail_index 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.
SatPropagator	Return type: explicit Arguments: const std::string& name
~SatPropagator	Return type: virtual
SetPropagatorId	Return type: void Arguments: int id Sets/Gets this propagator unique id.
Untrail	Return type: virtual void Arguments: const Trail& trail, int trail_index 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.