Optimal implementation of watched literals and more general techniques

Research output: Contribution to journalArticlepeer-review

10 Citations (Scopus)
2 Downloads (Pure)

Abstract

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.
Original languageEnglish
Pages (from-to)231-252
Number of pages22
JournalJournal of Artificial Intelligence Research
Volume48
Publication statusPublished - Oct 2013

Fingerprint

Dive into the research topics of 'Optimal implementation of watched literals and more general techniques'. Together they form a unique fingerprint.

Cite this