Module varisat::prop::watch

Watchlists to detect clauses that became unit.

Each (long) clause has always two watches pointing to it. The watches are kept in the watchlists of two different literals of the clause. Whenever the watches are moved to different literals the litereals of the clause are permuted so the watched literals are in position 0 and 1.

When a clause is not unit under the current assignment, the watched literals point at two non-false literals. When a clause is unit and thus propagating, the true literal is watched and in position 0, the other watched literal is the one with the largest decision level and kept in position 1. When a clause becomes satisfied before becoming unit the watches can be kept as they were.

When a literal is assigned false that invariant can be invalidated. This can be detected by scanning the watches of the assigned literal. When the assignment is processed the watches are moved to restore that invariant. Unless there is a conflict, i.e. a clause with no non-false literals, this can always be done. This also finds all clauses that became unit. The new unit clauses are exactly those clauses where no two non-false literals can be found.

There is no need to update watchlists on backtracking, as unassigning variables cannot invalidate the invariant.

See Section 4.5.1 of the "Handbook of Satisfiability" for more details and references.

As a further optimization we use blocking literals. This means that each watch stores a literal of the clause that is different from the watched literal. It can be the other watched literal or any unwatched literal. When that literal is true, the clause is already satisfied, meaning that no watches need to be updated. This can be detected by just looking at the watch, avoiding access of the clause database. This variant was introduced by Niklas Sörensson and Niklas Eén in "MINISAT 2.1 and MINISAT++1.0 — SAT Race 2008 Editions".

Structs

Watch	A watch on a long clause.
Watchlists	Watchlists to detect clauses that became unit.

Functions

enable_watchlists

Enable and rebuild watchlists.