C++ Reference: class LiteralWatchers

Note: This documentation is automatically generated.

Stores the 2-watched literals data structure. See http://www.cs.berkeley.edu/~necula/autded/lecture24-sat.pdf for detail.

This class is also responsible for owning the clause memory and all related information.

TODO(user): Rename ClauseManager. This does more than just watching the clauses and is the place where all the clauses are stored.

Method
AddClause	Return type: bool Arguments: absl::Span<const Literal> literals, Trail* trail Adds a new clause and perform initial propagation for this clause only.
AddClause	Return type: bool Arguments: absl::Span<const Literal> literals
AddRemovableClause	Return type: SatClause* Arguments: const std::vector<Literal>& literals, Trail* trail Same as AddClause() for a removable clause. This is only called on learned conflict, so this should never have all its literal at false (CHECKED).
AllClausesInCreationOrder	Return type: const std::vector<SatClause*>&
Attach	Return type: void Arguments: SatClause* clause, Trail* trail Attaches the given clause. The first two literal of the clause must be unassigned and the clause must not be already attached.
AttachAllClauses	Return type: void
CleanUpWatchers	Return type: void
DeleteRemovedClauses	Return type: void Reclaims the memory of the lazily removed clauses (their size was set to zero) and remove them from AllClausesInCreationOrder() this work in O(num_clauses()).
Detach	Return type: void Arguments: SatClause* clause Detaches the given clause right away. TODO(user): It might be better to have a "slower" mode in PropagateOnFalse() that deal with detached clauses in the watcher list and is activated until the next CleanUpWatchers() calls.
DetachAllClauses	Return type: void During an inprocessing phase, it is easier to detach all clause first, then simplify and then reattach them. Note however that during these two calls, it is not possible to use the solver unit-progation. Important: When reattach is called, we assume that none of their literal are fixed, so we don't do any special checks. These functions can be called multiple-time and do the right things. This way before doing something, you can call the corresponding function and be sure to be in a good state. I.e. always AttachAllClauses() before propagation and DetachAllClauses() before going to do an inprocessing pass that might transform them.
InprocessingAddClause	Return type: SatClause* Arguments: absl::Span<const Literal> new_clause This can return nullptr if new_clause was of size one or two as these are treated differently. Note that none of the variable should be fixed in the given new clause.
InprocessingFixLiteral	Return type: ABSL_MUST_USE_RESULT bool Arguments: Literal true_literal
InprocessingRemoveClause	Return type: void Arguments: SatClause* clause These must only be called between [Detach/Attach]AllClauses() calls.
InprocessingRewriteClause	Return type: ABSL_MUST_USE_RESULT bool Arguments: SatClause* clause, absl::Span<const Literal> new_clause
IsRemovable	Return type: bool Arguments: SatClause* const clause True if removing this clause will not change the set of feasible solution. This is the case for clauses that were learned during search. Note however that some learned clause are kept forever (heuristics) and do not appear here.
LazyDetach	Return type: void Arguments: SatClause* clause Lazily detach the given clause. The deletion will actually occur when CleanUpWatchers() is called. The later needs to be called before any other function in this class can be called. This is DCHECKed. Note that we remove the clause from clauses_info_ right away.
literal_size	Return type: int64_t The number of different literals (always twice the number of variables).
LiteralWatchers	Return type: explicit Arguments: Model* model
~LiteralWatchers
mutable_clauses_info	Return type: absl::flat_hash_map<SatClause*, ClauseInfo>*
NextClauseToMinimize	Return type: SatClause* Really basic algorithm to return a clause to try to minimize. We simply loop over the clause that we keep forever, in creation order. This starts by the problem clauses and then the learned one that we keep forever.
num_clauses	Return type: int64_t
num_inspected_clause_literals	Return type: int64_t
num_inspected_clauses	Return type: int64_t Total number of clauses inspected during calls to PropagateOnFalse().
num_removable_clauses	Return type: int64_t
num_watched_clauses	Return type: int64_t Number of clauses currently watched.
Propagate	Return type: bool Arguments: Trail* trail SatPropagator API.
Reason	Return type: absl::Span<const Literal> Arguments: const Trail& trail, int trail_index
ReasonClause	Return type: SatClause* Arguments: int trail_index Returns the reason of the variable at given trail_index. This only works for variable propagated by this class and is almost the same as Reason() with a different return format.
ResetToMinimizeIndex	Return type: void Restart the scan in NextClauseToMinimize() from the first problem clause.
Resize	Return type: void Arguments: int num_variables Must be called before adding clauses referring to such variables.
SetDratProofHandler	Return type: void Arguments: DratProofHandler* drat_proof_handler
WatcherListOnFalse	Return type: const std::vector<Watcher>& Arguments: Literal false_literal This is exposed since some inprocessing code can heuristically exploit the currently watched literal and blocking literal to do some simplification.