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

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.

CleanUpWatchers

Return type: void

DeleteDetachedClauses

Return type: void

Reclaims the memory of the detached clauses and remove them from AllClausesInCreationOrder() this work in O(num_clauses()).

Detach

Return type: void

Arguments: SatClause* clause

Detaches the given clause right away.

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.

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