Stay organized with collections Save and categorize content based on your preferences.

C++ Reference: class LiteralWatchers

Note: This documentation is automatically generated.

Stores the 2-watched literals data structure. See 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.

Return type: bool

Arguments: absl::Span<const Literal> literals, Trail* trail

Adds a new clause and perform initial propagation for this clause only.


Return type: bool

Arguments: absl::Span<const Literal> literals


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).


Return type: const std::vector<SatClause*>&


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.


Return type: void


Return type: void


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()).


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.


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.


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.


Return type: ABSL_MUST_USE_RESULT bool

Arguments: Literal true_literal


Return type: void

Arguments: SatClause* clause

These must only be called between [Detach/Attach]AllClauses() calls.


Return type: ABSL_MUST_USE_RESULT bool

Arguments: SatClause* clause, absl::Span<const Literal> new_clause


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.


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.


Return type: int64_t

The number of different literals (always twice the number of variables).


Return type: explicit

Arguments: Model* model



Return type: absl::flat_hash_map<SatClause*, ClauseInfo>*


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.


Return type: int64_t


Return type: int64_t


Return type: int64_t

Total number of clauses inspected during calls to PropagateOnFalse().


Return type: int64_t


Return type: int64_t

Number of clauses currently watched.


Return type: bool

Arguments: Trail* trail

SatPropagator API.


Return type: absl::Span<const Literal>

Arguments: const Trail& trail, int trail_index


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.


Return type: void

Restart the scan in NextClauseToMinimize() from the first problem clause.


Return type: void

Arguments: int num_variables

Must be called before adding clauses referring to such variables.


Return type: void

Arguments: DratProofHandler* drat_proof_handler


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.