Output details

Optimal Implementation of Watched Literals and More General Techniques

<11>This paper proves an entirely unexpected theoretical result concerning a key implementation technique for Satisfiability and Constraint Programming solvers. Watched Literals were introduced in 2001 in the famous Chaff solver which revolutionised Satisfiability solving. This paper shows that a simple and widely used technique for implementing watched literals is optimal. The result even applies to existing implementations which their authors stated were not optimal. The impact of this paper will lie in greater understanding of this key technique, and more informed choice of implementation technique. This paper appeared in JAIR, one of the top two journals in Artificial Intelligence.