C++ Reference: class LiteralWatchers

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

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

num_inspected_clause_literals

Return type: int64

num_inspected_clauses

Return type: int64

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

num_removable_clauses

Return type: int64

num_watched_clauses

Return type: int64

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