基于演化算法的SAT问题求解

SAT问题即布尔可满足性问题是逻辑学的一个基本问题,也是计算机科学和人工智能研究的核心问题。寻找求解SAT问题的快速算法不仅在理论研究上而且在许多应用领域都具有极其重要的意义。本文讨论了基于演化算法的SAT问题求解方法。     

组织进化算法求解SAT问题

基于组织的概念设计了一种新的进化算法——求解SAT问题的组织进化算法(Organizational Evolutionary Algorithm for SAT problem,0EASAT)．OEASAT将SAT问题分解成若干子问题,然后用每个子问题形成一个组织,并根据SAT问题的特点设计了三种组织进化算子——自学习算子、吞并算子和分裂算子以引导组织的进化．根据组织的适应度,将所有组织分成两个种群——最优种群和非最优种群,然后用进化的方式来控制各算子,以协调各组织间的相互作用．OEASAT通过先解决子问题,再协调相冲突变量的方式来求解SAT问题．由于子问题的规模较小,相对于原问题来说较容易解决,这样就达到了降低问题复杂度的目的．实验用标准SATLIB库中变量个数从20-250的3700个不同规模的标准SAT问题对OEASAT的性能作了全面的测试,并与著名的WalkSAT和RFEA2的结果作了比较．结果表明,OEASAT具有更高的成功率和更高的运算效率．对于具有250个变量、1065个子句的SAT问题,OEASAT仅用了1．524s,表现出了优越的性能．     

求解SAT问题的拟人退火算法

该文利用一个简单的变换,将可满足性（SAT）问题转换为一个求相应目标函数最小值的优化问题,提出了一种用于跳出局部陷阱的拟人策略,基于模拟退火算法和拟人策略,为SAT问题的高效近注解得出了拟人退火算法（PA）,该方法不仅具有模拟退火算法的全局收敛性质,而且具有一定的并行性,继承性。数值实验表明,对于本文随机产生的测试问题例,采用拟人策略的模拟退火算法的结果优于局部搜索算法,模拟退火算法以及近来国际上流行的WALKSAT算法,因此拟人退火算法是可行的和有效的。     

基于DPLL的混合遗传算法求解SAT问题

基于\"聚类排序选择\"优化遗传算法求解SAT问题时,引入交叉算子和变异算子,并根据适应度函数及问题本身特性,调节阈值δ,生成新的种群聚类。这种遗传算法有效地抑制了算法的延迟收敛,从而保证了为可满足性公式能够快速找到一个可满足性指派。同时,在遗传算法中引入了DPLL算法,对部分变元进行消解,提高了算法的求解效率。相关的实验数据表明,本算法的性能明显优于同类算法。     

求解SAT问题的算法的研究进展

SAT问题是研究最广泛的NPC问题之一。由于SAT问题本身的特性,除非P=NP,否则不存在最坏情况下多项式阶时间复杂度的SAT求解算法。因此设计出高效快速的SAT求解算法至今仍是研究热点。首先简要介绍了SAT问题;其次从完备算法、不完备算法和组合算法3个角度总结了新近的研究进展,深入分析了已有算法解决SAT问题的基本流程,并从适用问题类别、算法特点、求解效率等方面对各类先进的求解器进行了对比分析;最后讨论了求解SAT问题的算法面临的挑战,并对下一步研究工作进行了展望。     

SAT问题中局部搜索法的改进

局部搜索方法在求解SAT问题的高效率使其成为一研究热点.提出用初始概率的方法对局部搜索算法中变量的初始随机指派进行适当的约束.使在局部搜索的开始阶段,可满足的子句数大大增加,减少了翻转的次数,加快了求解的速度.用该方法对目前的一些重要的SAT问题的局部搜索算法(如WSAT,TSAT,NSAT,SDF等)进行改进,通过对不同规模的随机3-SAT问题的实例和一些不同规模的结构性SAT问题的实例,以及利用相变现象构造的难解SAT实例测试表明,改进后的这些局部搜索算法的求解效率有了很大的提高.该方法对其他局部搜索法的改进具有参考价值.     

求解SAT问题的量子免疫克隆算法

将量子计算应用于人工免疫系统中的克隆算子,提出了一种基于量子编码的免疫克隆算法(Quantum-Inspired Immune Clonal Algorithm,QICA)来求解SAT问题,并从理论上证明了算法的全局收敛性.算法中采用量子位的编码方式来表达种群中的抗体,针对这种编码方式采用量子旋转门和动态调整旋转角度策略对抗体进行演化,加速原有克隆算子的收敛;利用克隆算子的局部寻优能力强的特点,在各个子群体间采用量子交叉操作来增强信息交流,提高种群的多样性防止早熟.实验中,用标准SATLIB库中的3700个不同规模的标准SAT问题对QICA的性能作了全面的测试,并与单纯的量子遗传算法和简单免疫克隆算法以及著名的WalkSAT和PFEA2算法进行比较,仿真实验表明:QICA具有更高的成功率和运算效率.对于具有250个变量、1065个子句的SAT问题,QICA也仅用了1.357s,显示出了优越的性能.     

基于子句权重学习的求解SAT问题的遗传算法

该文提出了一种求解SAT问题的改进遗传算法（SAT—WAGA）．SAT-WAGA算法有多个改进性特点：将SAT问题的结构信息量化为子句权重,增加了学习算子和判定早熟参数,学习算子能根据求解过程中的动态信息对子句权重进行调整,以便防止遗传进程的早熟,同时,算法还采用了最优染色体保存策略,防止进化过程的发散．该文最后描述了实现包括SAT—WAGA等多个算法的实验系统,对选择最佳早熟判定参数值给出了一些有效的建议．实验结果表明：与一般遗传算法相比,SAT—WAGA算法在求解速度、成功率和求解问题的规模等方面都有明显的改善．     

O（m^2）时间求解SAT问题的随机算法

传统的求解SAT问题的随机算法主要是对满足解进行搜索,在找不到满足解的情况下,则无法正确判断问题的可满足性。该文提出了两个时间复杂度为O（m^2）求解SAT问题的随机算法SatTestl和SatTest2,这里m为CNF公式中的子句数。这两个随机算法是通过对不满足解数的估计来判断SAT问题的可满足性,不同于传统的随机算法。其中第二个算法SatTest2在搜索满足解的同时又可以对不满足解数进行估计,是对传统随机算法的重要改进。试验结果表明,文中提出的算法对相变区域的难SAT实例有较好的求解能力。     

基于分支回溯的NAE-3SAT问题求解算法

NAESAT问题是可满足性问题的一个重要扩展,在集合分裂、最大割集等NP完全问题中有着重要的应用.针对NAESAT问题的泛化NAE-3SAT问题,提出了一个基于分支回溯的精确算法NAE.算法给出了多种化简规则,这些化简规则很好地提高了算法的时间效率.最后证明了算法在最坏情况下的时间复杂度上界为O(1.618n),其中n为公式中的变量数目.     

Relaxations of the Satisfiability Problem Using Semidefinite Programming

We derive a semidefinite relaxation of the satisfiability (SAT) problem and discuss its strength. We give both the primal and dual formulation of the relaxation. The primal formulation is an eigenvalue optimization problem, while the dual formulation is a semidefinite feasibility problem. We show that using the relaxation, a proof of the unsatisfiability of the notorious pigeonhole and mutilated chessboard problems can be computed in polynomial time. As a byproduct we find a new `sandwich" theorem that is similar to the sandwich theorem for Lovász' -function. Furthermore, the semidefinite relaxation gives a certificate of (un)satisfiability for 2SAT problems in polynomial time. By adding an objective function to the dual formulation, a specific class of polynomially solvable 3SAT instances can be identified. We conclude with discussing how the relaxation can be used to solve more general SAT problems and with some empirical observations.     

求解SAT问题的退火遗传算法

提出一种将遗传算法与模拟退火算法相结合的SAT问题求解算法SAT-SAGA.该算法以遗传算法流程为主体,并把模拟退火机制融入其中,用以调整优化群体,防止陷入局部最优和出现早熟;在进化过程中算法采用了最优染色体保存策略,防止进化过程的发散.实验表明:该算法在求解速度、成功率和求解问题的规模等方面都有明显的改善.     

可满足性问题的三维DNA图结构算法

论文提出用三维图结构解决DNA分子计算问题,给出了解决3-SAT问题的方法。在所提出的方法中,算法所要求的步骤与公式中变量的数目相等。     

线性规划的一种并行修正松弛算法

对求解线性规划问题的松弛算法进行了修正 ,在此基础上提出了一种基于 Cluster结构的并行算法 ,分析了算法的性能 ;基于曙光— 30 0 0大规模并行计算机 ,给出了算法用于求解线性规划问题实例的实验结果 .理论分析和实验结果表明 :修正算法改进了松弛算法的实际性能 ,同时具有较好的并行性和稳定性 ,可用于求解此类大规模科学与工程规划问题的高性能计算     

基于变元加权的一种求解SAT问题的新方法

研究合取范式可满足性的SAT问题作为一个NP完全问题,在计算机科学及组合优化问题领域中有着中心课题的重要地位。由于其NP问题的性质决定了它尚无通用快速的完全算法,因此基于“实验算法学”的思想,按照平均性态而不是最坏情况性态的原则,对具有启发式策略的不完全算法的研究成为近年来大家关注与努力的焦点。该文正是立足于此,提出了“加权消元”这一种全新而且高效的算法。     

Unsupervised Learning of Image Manifolds by Semidefinite Programming

Can we detect low dimensional structure in high dimensional data sets of images? In this paper, we propose an algorithm for unsupervised learning of image manifolds by semidefinite programming. Given a data set of images, our algorithm computes a low dimensional representation of each image with the property that distances between nearby images are preserved. More generally, it can be used to analyze high dimensional data that lies on or near a low dimensional manifold. We illustrate the algorithm on easily visualized examples of curves and surfaces, as well as on actual images of faces, handwritten digits, and solid objects.