# CoAPI: An Efficient Two-Phase Algorithm Using Core-Guided Over-Approximate Cover for Prime Compilation of Non-Clausal Formulae

## TL;DR

CoAPI is a novel two-phase algorithm that efficiently generates all prime implicates of non-clausal formulas by avoiding dual rail encoding and using core-guided rewriting and cover shrinking techniques.

## Contribution

The paper introduces CoAPI, a new two-phase method that improves prime compilation efficiency for non-clausal formulas without relying on dual rail encoding.

## Key findings

- CoAPI significantly reduces computation time compared to state-of-the-art methods.
- The multi-order shrinking method effectively compresses the cover size.
- Experimental results demonstrate superior performance of CoAPI in prime implicate generation.

## Abstract

Prime compilation, i.e., the generation of all prime implicates or implicants (primes for short) of formulae, is a prominent fundamental issue for AI. Recently, the prime compilation for non-clausal formulae has received great attention. The state-of-the-art approaches generate all primes along with a prime cover constructed by prime implicates using dual rail encoding. However, the dual rail encoding potentially expands search space. In addition, constructing a prime cover, which is necessary for their methods, is time-consuming. To address these issues, we propose a novel two-phase method -- CoAPI. The two phases are the key to construct a cover without using dual rail encoding. Specifically, given a non-clausal formula, we first propose a core-guided method to rewrite the non-clausal formula into a cover constructed by over-approximate implicates in the first phase. Then, we generate all the primes based on the cover in the second phase. In order to reduce the size of the cover, we provide a multi-order based shrinking method, with a good tradeoff between the small size and efficiency, to compress the size of cover considerably. The experimental results show that CoAPI outperforms state-of-the-art approaches. Particularly, for generating all prime implicates, CoAPI consumes about one order of magnitude less time.