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 wrote

The 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

  1. searches for all single-polar (or pure) literals
  2. assigns a boolean value to them such that each yields True
  3. in which case we can now delete all the clauses containing them

Here 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)?

  • "single-polar" = instances of either only straight literal or negated? it might also help (eg for self containment of the question, clarity etc) to define some of the other terms, although do understand they are std in the field – vzn Aug 2 '15 at 4:32
  • @vzn certainly. I have added more links & subtext – Archy Wilhes 魏何 Aug 2 '15 at 5:56
up vote 7 down vote accepted

Solvers that use the two-watched-literals algorithm to implement unit propagation don't keep track of which clauses have been deleted (by implication) to produce 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 any 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.

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.