---
title: "Prime Compilation of Non-Clausal Formulae"
authors:
  - "Alessandro Previti"
  - "Alexey Ignatiev"
  - "António Morgado"
  - "João P. Marques Silva"
doi: ""
url: "https://ijcai.org/proceedings/2015/281"
pdf: "https://ijcai.org/proceedings/2015/0281.pdf"
venue: "Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence"
year: 2015
pages: "1980-1987"
track: "Main Track"
keywords:
---

# Prime Compilation of Non-Clausal Formulae

Alessandro Previti, Alexey Ignatiev, António Morgado, João P. Marques Silva

*Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence*, pages 1980-1987.

## 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.