极小不可满足核及其提取

The Minimal Unsatisfiable Core and Its Extraction

在极小不可满足公式和可满足公式的基础上给出极小不可满足核的定义,并给出用布尔可满足求解器提取不可满足公式的极小不可满足核的方法。

The minimal unsatisfiable core is a hot research field in theoretical computer science.Based on the minimal unsatisfable formula and satisfiable formula,this paper defines the minimal unsatisfiable core,and gives out the method to extract the minimal unsatisfiable cores of the minimal unsatisfiable formula with the sat-resolver.