PDF | PostScript | doi:10.1613/jair.4016
Appendix 1 - Additional proofs (pdf) | Appendix 2 - Additional proofs (ps) | Appendix 3 - Code, scripts and data
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.
Click here to return to Volume 48 contents list