极小布尔不可满足子式的提取算法

Algorithms for Extracting Minimal Unsatisfiable Boolean Sub-formula

研究了极小布尔不可满足子式的提取算法 ,它分为近似算法和精确算法两种 文中就精确算法提出了局部预先赋值的优化方案 ,并且在理论上证明了该算法的正确性 ;通过实验显示了此算法可以获得更高的效率 通过模拟实验观察到 ,利用完全算法进行近似提取的一个有趣现象 ,即随着公式密度的增加 。

The paper is concerned with the algorithms for extraction of minimal unsatisfiable (MU) Boolean sub-formula The algorithms include approximate and exact methods We propose a method of pre-assignment for exact algorithm of traversing clauses, and the correctness is proved in theory Furthermore, the experiments demonstrated the efficiency of pre-assignment method Moreover, an observation revealed that the interesting phenomenon occurs in the simulating experiments on approximate method based on complete algorithm, with the increasing density of the formula, the average error of the extraction is decreasing