Heuristics Based on Unit Propagation for Satisfiability Problems

Abstract

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 evaluations of di erent alternatives a new simple unit propagation based heuristic is put forward. This compares favorably with the heuristics employed in the current state-of-the-art DPL implementations (C-SAT, Tableau, POSIT). 1

Cite

Text

Li and Anbulagan. "Heuristics Based on Unit Propagation for Satisfiability Problems." International Joint Conference on Artificial Intelligence, 1997. doi:10.1038/bjc.1951.8

Markdown

[Li and Anbulagan. "Heuristics Based on Unit Propagation for Satisfiability Problems." International Joint Conference on Artificial Intelligence, 1997.](https://mlanthology.org/ijcai/1997/li1997ijcai-heuristics/) doi:10.1038/bjc.1951.8

BibTeX

@inproceedings{li1997ijcai-heuristics,
  title     = {{Heuristics Based on Unit Propagation for Satisfiability Problems}},
  author    = {Li, Chu Min and Anbulagan, },
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {1997},
  pages     = {366-371},
  doi       = {10.1038/bjc.1951.8},
  url       = {https://mlanthology.org/ijcai/1997/li1997ijcai-heuristics/}
}