Prime compilation of non-clausal formulae

A. Previti, A. Ignatiev, A. Morgado, J. Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

22 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationProceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence
EditorsQiang Yang, Michael Wooldridge
Place of PublicationPalo Alto CA USA
PublisherAssociation for the Advancement of Artificial Intelligence (AAAI)
Number of pages8
ISBN (Electronic)9781577357384
Publication statusPublished - 2015
Externally publishedYes
EventInternational Joint Conference on Artificial Intelligence 2015 - Buenos Aires, Argentina
Duration: 25 Jul 20151 Aug 2015
Conference number: 24th


ConferenceInternational Joint Conference on Artificial Intelligence 2015
Abbreviated titleIJCAI 2015
CityBuenos Aires
Internet address

Cite this