C++ Reference: class SatPropagator

This documentation is automatically generated.

Base class for all the SAT constraints.
Method
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 assignement 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.

Send feedback about...