Prime compilation aims to generate all prime implicates/implicants of a Boolean formula. Recently, prime compilation of non-clausal formulae has received great attention. Since it is hard for$\Sigma_{2}^{P}$, existing methods have performance issues. We argue that the main performance bottleneck stems from enlarging the search space using dual rail (DR) encoding, and computing a minimal clausal formula as a by-product. To deal with the issue, we propose a two-phase approach, namely CoAPI, for prime compilation of non-clausal formulae. Thanks to the two-phase framework, we construct a clausal formula without using DR encoding. In addition, to improve performance, the key in our work is a novel bounded prime extraction (BPE) method that, interleaving extracting prime implicates with extracting small implicates, enables constructing a succinct clausal formula rather than a minimal one. Following the assessment way of the state-of-the-art (SOTA) work, we show that CoAPI achieves SOTA performance. Particularly, for generating all prime implicates, CoAPI is up to about one order of magnitude faster. Moreover, we evaluate CoAPI on a benchmark sourcing from real-world industries. The results also confirm the outperformance of CoAPI11Our code and benchmarks are publicly available at https://github.com/LuoWeiLinWillam/CoAPI.

The boundary conditions (BCs) have shown great potential in requirements engineering because a BC captures the particular combination of circumstances, i.e., divergence, in which the goals of the requirement cannot be satisfied as a whole. Existing researches have attempted to automatically identify lots of BCs. Unfortunately, a large number of identified BCs make assessing and resolving divergences expensive. Existing methods adopt a coarse-grained metric, generality, to filter out less general BCs. However, the results still retain a large number of redundant BCs since a general BC potentially captures redundant circumstances that do not lead to a divergence. Furthermore, the likelihood of BC can be misled by redundant BCs resulting in costly repeatedly assessing and resolving divergences. In this paper, we present a fine-grained metric to filter out the redundant BCs. We first introduce the concept of contrasty of BC. Intuitively, if two BCs are contrastive, they capture different divergences. We argue that a set of contrastive BCs should be recommended to engineers, rather than a set of general BCs that potentially only indicates the same divergence. Then we design a post-processing framework (PPFc) to produce a set of contrastive BCs after identifying BCs. Experimental results show that the contrasty metric dramatically reduces the number of BCs recommended to engineers. Results also demonstrate that lots of BCs identified by the state-of-the-art method are redundant in most cases. Besides, to improve efficiency, we propose a joint framework (JFc) to interleave assessing based on the contrasty metric with identifying BCs. The primary intuition behind JFc is that it considers the search bias toward contrastive BCs during identifying BCs, thereby pruning the BCs capturing the same divergence. Experiments confirm the improvements of JFc in identifying contrastive BCs.

In goal-oriented requirements engineering, goal conflict identification is of fundamental importance for requirements analysis. The task aims to find the feasible situations which make the goals diverge within the domain, called boundary conditions (BCs). However, the existing approaches for goal conflict identification fail to find sufficient BCs and general BCs which cover more combinations of circumstances. From the BCs found by these existing approaches, we have observed an interesting phenomenon that there are some pairs of BCs are similar in formula structure, which occurs frequently in the experimental cases. In other words, once a BC is found, a new BC may be discovered quickly by slightly changing the former. It inspires us to develop a local search algorithm named LOGION to find BCs, in which the structural similarity is captured by the neighborhood relation of formulae. Based on structural similarity, LOGION can find a lot of BCs in a short time. Moreover, due to the large number of BCs identified, it potentially selects more general BCs from them. By taking experiments on a set of cases, we show that LOG I ON effectively exploits the structural similarity of BCs. We also compare our algorithm against the two state-of-the-art approaches. The experimental results show that LOGION produces one order of magnitude more BCs than the state-of-the-art approaches and confirm that LOGION finds out more general BCs thanks to a large number of BCs.