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)

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.

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)
Pages1980-1987
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
https://www.ijcai-15.org/index.php?option=com_content&view=article&id=71:call-for-papers&catid=9:uncategorised&Itemid=477

Conference

ConferenceInternational Joint Conference on Artificial Intelligence 2015
Abbreviated titleIJCAI 2015
CountryArgentina
CityBuenos Aires
Period25/07/151/08/15
Internet address

Cite this