Pure literal elimination

also: pure literal

A literal whose negation appears in no clause can be set true outright: doing so can only satisfy clauses, never falsify one, so the assignment needs no decision and is never undone. It is in the original DPLL paper and in almost no modern solver, because maintaining the occurrence counts costs more than the rule saves.

A literal is pure when its negation appears in no clause. Assigning it true can only satisfy clauses and can never falsify one, so the assignment needs no decision and never has to be undone.

let pure_literals (cs : int list list) : int list =
  let seen = Hashtbl.create 64 in
  List.iter (List.iter (fun l -> Hashtbl.replace seen l true)) cs;
  Hashtbl.fold
    (fun l _ acc -> if Hashtbl.mem seen (-l) then acc else l :: acc)
    seen []
  |> List.sort compare

pure: -3 1

It appears in the original DPLL paper and in almost no modern solver. The reason is cost: keeping the occurrence counts current under clause learning is more expensive than the rule saves, and the rule is incompatible with the watched-literal scheme, which deliberately does not know how many times a literal occurs.

It also does not preserve the set of models, only satisfiability. That is harmless for a decision procedure and wrong for model counting, which is the other reason it is usually left out.

DPLL · Unit propagation

• Implementing SAT in OCaml Part 1CNF, unit propagation, a full recursive DPLL solver, pure literal elimination, a DIMACS parser, and a command-line driver.