一种求解布尔不可满足子式的局部搜索算法

A Local Search Algorithm for the Boolean Unsatisfiable Subformulae Extraction

解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而不可满足子式能够为公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由。近年来涌现了许多基于SAT求解器DPLL回溯搜索过程的完全算法,但关于不完全方法提取不可满足子式的研究相对较少。因此,本文提出一种采用启发式局部搜索过程从公式的不可满足性证明中求解布尔不可满足子式的算法。该算法根据公式的消解规则通过局部搜索过程直接构造证明不可满足性的消解序列,并融合了布尔推理技术以提高搜索效率;而后通过一个递归过程遍历证明序列从而得到不可满足子式。通过实验与贪心遗传算法进行对比,结果表明本文提出的算法优于贪心遗传算法。

Explaining the causes of infeasibility of the Boolean formulae has practical applications in various fields. A small unsatisfiable subformula can provide a succinct explanation of infeasibility, and help automatic tools to rapidly locate the errors, and determine the underlying reasons for the failure. In recent years finding unsatisfiable subformulae has been addressed frequently by researchers, mostly based on the SAT solvers with the DPLL backtrack-search algorithm. However little attention has been concentrated on the extraction of unsatisfiable subformulae using incomplete methods. In this paper, we propose a heuristic local search algorithm to extract unsatisfiable subformulae from the resolving traces of a formula. This approach directly constructs the resolution sequences for proving unsatisfiability with a local search procedure, combines with reasoning heuristics, and then recursively derives unsatisfiable subformulae from the resolving traces. The experimental results show that our algorithm outperforms the greedy genetic algorithm on the same benchmarks.