Prime compilation of non-clausal formulae
Alessandro Previti, Alexey Ignatiev, António Morgado, João P. Marques-Silva · 2015
Formula compilation by generation of prime im-plicates or implicants finds a wide range of appli-cations in AI. Recent work on formula compila-tion by prime implicate/implicant generation often assumes a Conjunctive/Disjunctive Normal Form (CNF/DNF) representation. However, in many settings propositional formulae are naturally ex-pressed 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 hun-dred variables. This paper describes two novel ap-proaches for the compilation of non-clausal formu-lae either with prime implicants or implicates, that is based on propositional Satisfiability (SAT) solv-ing. These novel algorithms also find application when computing all prime implicates of a CNF for-mula. The proposed approach is shown to allow the compilation of non-clausal formulae of size signif-icantly larger than existing approaches. 1