ML Anthology

Prime Compilation of Non-Clausal Formulae

Alessandro Previti, Alexey Ignatiev, António Morgado, João Marques-Silva
IJCAI 2015 pp. 1980-1988
/ijcai/2015/previti2015ijcai-prime/

Abstract

Formula compilation by generation of prime implicates or implicants finds a wide range of applications in AI. Recent work on formula compilation by prime implicate/implicant generation often assumes a Conjunctive/Disjunctive Normal Form (CNF/DNF) representation. However, in many settings propositional formulae are naturally expressed in non-clausal form. Despite a large body of work on compilation of non-clausal formulae, in practice existing approaches can only be applied to fairly small formulae, containing at most a few hundred variables. This paper describes two novel approaches for the compilation of non-clausal formulae either with prime implicants or implicates, that is based on propositional Satisfiability (SAT) solving. These novel algorithms also find application when computing all prime implicates of a CNF formula. The proposed approach is shown to allow the compilation of non-clausal formulae of size significantly larger than existing approaches.

PDF IJCAI Semantic Scholar

Cite

Text

Previti et al. "Prime Compilation of Non-Clausal Formulae." International Joint Conference on Artificial Intelligence, 2015.

Markdown

[Previti et al. "Prime Compilation of Non-Clausal Formulae." International Joint Conference on Artificial Intelligence, 2015.](https://mlanthology.org/ijcai/2015/previti2015ijcai-prime/)

BibTeX

@inproceedings{previti2015ijcai-prime,
  title     = {{Prime Compilation of Non-Clausal Formulae}},
  author    = {Previti, Alessandro and Ignatiev, Alexey and Morgado, António and Marques-Silva, João},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2015},
  pages     = {1980-1988},
  url       = {https://mlanthology.org/ijcai/2015/previti2015ijcai-prime/}
}