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.