Efficient Consequence Finding

Abstract

We present an extensive experimental study of consequence-finding algorithms based on kernel resolution, using both a trie-based and a novel ZBDD-based implementation, which uses Zero-Suppressed Binary Decision Diagrams to concisely store and process very large clause sets. Our study considers both the full prime implicate task and applications of consequence-finding for restricted target languages in abduction, model-based and fault-tree diagnosis, and polynomially-bounded knowledge compilation. We show that the ZBDD implementation can push consequence-finding to a new limit, solving problems which generate over 10^70 clauses.

Cite

Text

Simon and del Val. "Efficient Consequence Finding." International Joint Conference on Artificial Intelligence, 2001.

Markdown

[Simon and del Val. "Efficient Consequence Finding." International Joint Conference on Artificial Intelligence, 2001.](https://mlanthology.org/ijcai/2001/simon2001ijcai-efficient/)

BibTeX

@inproceedings{simon2001ijcai-efficient,
  title     = {{Efficient Consequence Finding}},
  author    = {Simon, Laurent and del Val, Alvaro},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2001},
  pages     = {359-370},
  url       = {https://mlanthology.org/ijcai/2001/simon2001ijcai-efficient/}
}