I'm looking into various SAT-solvers and trying to understand how they work and why they are designed in certain ways. (But I'm not in a university at the moment and I do not know anyone who is a professor. So I'm posting here hoping that someone can help me out. I'd really appreciate.)In Chaff, BCP (Boolean Constraint Propagation) is implemented differently from the original DPLL: it does it by watching two literals at a time (a technique slightly different from one initially suggested in SATO: An Efficient Propositional Prover) according to the 2001 paper, Chaff: Engineering an Efficient SAT Solver. There is, however, no mention of pure literal elimination in this paper.In The Complexity of Pure Literal Elimination, Jan Johannsen wroteThe current best implementations of DLL-type SAT solvers, like Chaff  or BerkMin sacrifice this heuristic in order to gain efficiency in unit  propagation.where this heuristic is referring to pure literal elimination. My understanding of what pure literal elimination does is that it searches for all single-polar (or pure) literals assigns a boolean value to them such that each yields True in which case we can now delete all the clauses containing themHere is my question:How is the sacrifice necessary? Is there a good reason why pure literal elimination is absent in DPLL-based algorithms like Chaff? Can't we just do pure literal elimination in each decision level (or at least do it at the start before branching)?
Why is pure literal elimination absent in DPLL-based algorithms like Chaff?
algorithms;sat solvers
Solvers that use the two-watched-literals algorithm to implement unit propagation don't keep track of which clauses have been deleted (by implication) from the subformula implied by the current partial assignment.  By not tracking this information, solvers can avoid touching most of the clauses during assignments and avoid touching all of the clauses during backtracking.  Figuring out which variables are currently pure in the formula means losing these substantial efficiency gains.  Meanwhile there's nothing to suggest that pure literal removal will produce conflicts or satisfying assignments early enough to make up for the heavy tracking cost.Solvers that do formula simplification before starting the search procedure will generally include pure literal removal since it is quite cheap to do as a preprocessing step and could potentially remove many clauses.