C++ Reference: class SatPropagator

Note: This documentation is automatically generated.

Base class for all the SAT constraints.

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.


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.


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.


Return type: bool

Arguments: const Trail& trail

Returns true iff all the trail was inspected by this propagator.


Return type: int


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.


Return type: explicit

Arguments: const std::string& name


Return type: virtual


Return type: void

Arguments: int id

Sets/Gets this propagator unique id.


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.