Optimal implementation of watched literals and more general techniques

I prove that an implementation technique for scanning lists in
backtracking search algorithms is optimal. The result applies to
a simple general framework, which I present: applications include
watched literal unit propagation in SAT and a number of examples
in constraint satisfaction. Techniques like watched literals are
known to be highly space efficient and effective in practice. When
implemented in the 'circular' approach described here, these
techniques also have optimal run time per branch in big-O terms
when amortized across a search tree. This also applies when multiple
list elements must be found. The constant factor overhead of the
worst case is only 2. Replacing the existing non-optimal implementation
of unit propagation in MiniSat speeds up propagation by 29%, though
this is not enough to improve overall run time significantly.