王 帅，王晓峰，梁 田，李 志

(北方民族大学计算机科学与工程学院，宁夏 银川 750021)

1 引言

骨干集一词是在布尔可满足性SAT(SATisfiability)问题相变研究中提出的[1 - 6]，一个可满足命题公式的骨干集文字必将会出现在所有满足指派中[7 - 10]，它对命题公式的可满足性判定难度有重要影响[11 - 17]。骨干集越大，公式的判定难度越大。如果给定一个命题公式的骨干集，那么公式的判定将会变得容易。然而，一般情况下，求解命题公式的骨干集是困难的。目前，学术界主要使用以下几种算法求解骨干集，最为基础的是Marques-Silva等人[18]利用骨干文字位于所有的满足指派中的性质，使用minisat求解器求出所有满足指派，并使之相交得到骨干集。Janota等人[19]通过对文献[18]方法的改进，提出一种更少迭代次数的骨干集求解算法，同时利用骨干文字反向赋值会使公式不满足的性质，提出一种文字翻转技术求解骨干集。Previti等人[20]利用抽象论证中理想语义和骨干集的联系，设计一种新的主干网络并利用带有偏好的SAT求解器求解骨干集。Guo等人[21]以一次测试算法为基础，运用启发式思维设计出一种评分机制与过滤机制相结合的骨干集算法。de Haan等人[22]利用结构化实例中的局部骨干文字很大一部分都是全局骨干文字的特点，以局部计算的复杂度来判断局部子句的骨干文字，进而求解骨干集。Zhu等人[23]利用集成电路中的错误空间和时间定位复杂化，设计了一个基于该技术的SAT求解方法，求解大规模公式中的骨干集。Ivrii等人[24]利用权重与数值等启发式信息，在逻辑上假设骨干文字用以加快算法的搜索速度。……