Theory
Unit Propagation
For unit propagation, two-watched literals with circular updates is asymptotically optimal. I suggest reading "Optimal Implementation of Watched Literals and More General Techniques" which generalizes the concept and proves optimality. (It can also be helpful to read "An Efficient Algorithm for Unit Propagation" to see why head/tail meets the same optimality, though with larger storage costs and backtracking costs.)
When a watcher is falsified, it must find some unassigned literal in the clause to replace it. (If it cannot, then in a two-watcher scheme the remaining watcher has become unit; in a one-watcher scheme the clause has become empty.) Critically, when doing this search for a replacement literal one must begin where the last search ended, treating the clause as a circular buffer.
When done this way, updating watchers takes constant time when amortized across the search tree. Therefore unit resolution takes amortized linear time. (Older solvers did not do this circular tracking, and instead always began the search from the start of the clause; this leads to quadratic worst-case complexity instead.)
When backtracking, watched literals require no updates.
Pure Literal Elimination
For pure literal elimination, after unit propagation we need to determine all unassigned literals with zero instances of a polarity. Polarity count can only change when a clause transitions between satisfied and unsatisfied, so when a literal is assigned/unassigned we must necessarily scan over all the clauses it occurs in (not just watches, but occurs) and update polarity counts. Care must be taken not to double-count clauses, but updating literals in a clause is already linear so this doesn't affect asymptotic worst case.
When a literal has zero instances of a polarity, it may be assigned. No unit propagation is necessary, since a pure literal has no clauses to resolve with.
When backtracking, polarity counts do require updates.
Conditional Autarkies
As an aside, the kind of pure literals DPLL seeks to find are actually a special case of a more general concept called conditional autarkies.
An autarky α is a (partial) assignment that satisfies all clauses it touches. A conditional autarky is an autarky with an assumption, i.e. if α_aut is an autarky for F ∧ α_con, then α_con ∪ α_aut is a conditional autarky.
Given a conditional autarky for F, the formula F ^ (α_con → α_aut) is not implied but is equisatisfiable. Note that the conditional part may be empty, so vanilla autarkies may also be assumed.
Pure literals are just a special case of autarky, satisfying every clause they touch. If the literal is only pure after assigning some variables then that is a conditional pure literal, a special case of a conditional autarky.
Practice
Unit Propagation
Modern solvers spend a bulk of their time doing unit propagation, so this is a highly-optimized section of code. Although the worst case for unit resolution is amortized linear, in practice the number of clauses updated is less than this. With watched literals you might even hit a best case of not being a watcher for any clauses! That's one of the reasons why this is so efficient in practice.
To optimize storage, a clause will store the two watchers as the first two literals in its elements list. This partitions the clause into the watcher half (size 2) and the remainder half. This allows the search for a new watcher to never consider the other watcher as viable.
Memory is slow, so cache misses are a significant cause of latency in watchlist updates. Iterating a watchlist is fast, since it is contiguous and the prefetcher does its thing well. But to actually iterate the literals of a clause (as well as retrieve the clause search position for circular updates) requires an indirection which is almost certainly going to be a cache miss.
To remedy this, each watch in a watchlist stores a cached literal from the clause called a 'blocking literal'. If this literal is satisfied, we don't need to do anything and move on. This check is likely to hit cache and be ~free. Otherwise we go ahead and perform the indirection to find a new watcher. (And the blocking literal will be updated to a more likely useful literal as a side effect.)
The next optimization is to note that for binary clauses, the watcher along with the blocking literal is enough space for the entire clause. No indirection is required at all and no clause ID is needed, provided we know this is a binary clause. To do that, we declare that our solver doesn't support more than 2^31 literals. This lets us store literals in a u32 with the MSB free for other uses; in our case we will set this MSB if the clause is binary.
That is, if the MSB is set then this value (with the MSB cleared) is the other literal of a binary clause, else this value is a blocking literal for a long clause and the clause ID is the next u32 after it. The result is that we get a watchlist containing variable-length elements:
[Other][Blocking][Clause ID][Blocking][Clause ID][Other][Other]etc.
As we iterate, we check the MSB to know which case we are in. Large real-world problems contain huge numbers of binary clauses. Not only does this speed up solving such problems due to more things fitting in cache and fewer indirections, but it saves a substantial amount of memory as well since binary clauses never allocate clause IDs.
Allocating clauses is an entirely other thing that is left as an exercise for the reader. (Hint: storing data together means it lives in cache together, so store the clause metadata like search position contiguous with the clause literals.)
I'd recommend reading over CaDiCal's propagation code with these concepts in mind.
Pure Literal Elimination
Pure literal elimination during assignment search loop is practically never worth it. Given everything outlined above, tacking on more tracking to count polarities nullifies the efficiency of propagation for something that almost never provides value. It also requires occurrence lists instead of just watch lists. You can have both, but the memory costs for occurrence lists are difficult to minimize.
This inefficiency also rears its head during backtracking, because now you have to increase polarity counts on clauses no longer satisfied. Unit propagation with watched literals doesn't require any work for backtracking.
All of this is especially true with clause learning. If p is some conditional pure variable, then (α_con → p) is merely a single clause and the solver can learn a lot more than this on its own.†
PLE can be cheaply performed once at the start of search. Since no unit propagation is occurring, the propagation engine remains unscathed. This is fairly common in basic solvers, but advanced solvers do not explicitly do this.
Bounded Variable Elimination
A much more powerful technique called bounded variable elimination can be performed during preprocessing or inprocessing. This takes a variable and generates all of the resolvents over it, adding them to the formula and removing the original clauses uttering this variable. The variable now no longer appears anywhere; the 'bounded' part comes in when we decide not to do this if the formula would become unhelpfully larger if we went through with it.
BVE is one of the more important processing techniques to apply in modern solving. As part of BVE, pure literals are trivially detected because they have no resolvents to produce. This technique subsumes performing any explicit PLE at the start of search.
This isn't quite the same as assigning pure literals during assignment search, but given this technique is applied arbitrarily often during search it probably approximates it pretty well at a negligible cost. Due to this, research into integrating PLE to propagation is, as far as I know, dead.
†
There is a bleeding-edge paradigm called satisfiability-driven clause learning (SDCL), which not only learns clauses from conflicts but learns clauses by solving small generated formulas during search. This allows it to learn not just implied clauses, but also equisatisfiable ones (called 'redundant clauses').
The generated formulas are called pruning predicates, and are a function of the formula being solved and the current partial assignment. If the predicate is satisfiable, then the current partial assignment may be pruned from the search space.
One kind of redundant clause, SBC (sometimes SET), can be found by solving a so-called positive reduct. All satisfying assignments for the positive reduct are conditional autarkies for F. So in effect this is finding conditional autarkies (rather than just conditional pures) during the search.
Incorporating this with practical effectiveness is an open problem.
For more on this I suggest reading "Encoding Redundancy for Satisfaction-Driven Clause Learning".
