Heuristics Based on Unit Propagation for satisfiability Problems

摘要

The paper studies new unit propagation based heuristics for Davis-Putnam-Loveland (DPL) procedure. These are the novel combinations of unit propagation and the usual "Maximum Occurrences in clauses of Minimum Size" heuristics. Based on the experimental evalutions of different alternatives a new simple unit propagation based heuristic is pur forward. This compares favorably with the heuristics employed in the current state-of-the-art DPL implementations (C-SAT, Tableau, POSIT).