静态SAT问题并行处理器的设计研究

针对SAT问题的复杂性及求解速度缓慢的问题，采用可重构器件FPGA设计，实现了静态回溯搜索算法SAT问题并行处理器，提出了研制动态SAT并行处理器的设想。     

An exact algorithm with learning for the graph coloring problem

Given an undirected graph G=(V,E), the Graph Coloring Problem (GCP) consists in assigning a color to each vertex of the graph G in such a way that any two adjacent vertices are assigned different colors, and the number of different colors used is minimized. State-of-the-art algorithms generally deal with the explicit constraints in GCP: any two adjacent vertices should be assigned different colors, but do not specially deal with the implicit constraints between non-adjacent vertices implied by the explicit constraints. In this paper, we propose an exact algorithm with learning for GCP which exploits the implicit constraints using propositional logic. Our algorithm is compared with several exact algorithms among the best in the literature. The experimental results show that our algorithm outperforms other algorithms on many instances. Specifically, our algorithm allows to close the open DIMACS instance 4-Fullins_5.     

基于硬件可编程逻辑的SAT求解算法研究与进展

布尔可满足性SAT问题作为第一个被证明的NP完全问题,是计算机理论与应用的核心问题,有着重要的应用价值,因此近年来涌现了各种各样SAT求解器。但是,SAT求解器的运算效率始终是影响其应用的关键因素,所以利用硬件的高性能与并行性来加速SAT求解过程已成为验证领域的一个研究热点。归纳总结了在SAT求解过程中,利用硬件现场可编程门逻辑FPGA的并行性和灵活性加速求解过程的各种算法研究,着重总结分析了应用型SAT求解器的加速策略。通过对各种方法的深入分析,指出它们的优缺点,为未来的研究提供了思路。     

Automatic Construction and Verification of Isotopy Invariants

We extend our previous study of the automatic construction of isomorphic classification theorems for algebraic domains by considering the isotopy equivalence relation. Isotopism is an important generalisation of isomorphism, and is studied by mathematicians in domains such as loop theory. This extension was not straightforward, and we had to solve two major technical problems, namely, generating and verifying isotopy invariants. Concentrating on the domain of loop theory, we have developed three novel techniques for generating isotopic invariants, by using the notion of universal identities and by using constructions based on subblocks. In addition, given the complexity of the theorems that verify that a conjunction of the invariants form an isotopy class, we have developed ways of simplifying the problem of proving these theorems. Our techniques employ an interplay of computer algebra, model generation, theorem proving, and satisfiability-solving methods. To demonstrate the power of the approach, we generate isotopic classification theorems for loops of size 6 and 7, which extend the previously known enumeration results. This work was previously beyond the capabilities of automated reasoning techniques. The author’s work was supported by EPSRC MathFIT grant GR/S31099.     

Improved Bounded Model Checking for the Universal Fragment of CTL

SAT-based bounded model checking (BMC) has been introduced as a complementary technique to BDD-based symbolic model checking in recent years, and a lot of successful work has been done in this direction. The approach was first introduced by A. Biere et al. in checking linear temporal logic (LTL) formulae and then also adapted to check formulae of the universal fragment of computation tree logic (ACTL) by W. Penczek et al. As the efficiency of model checking is still an important issue, we present an impr...     

求解SAT问题的分级重排搜索算法

局部搜索法在ＳＡＴ问题上的成功运用已引起越来越广泛的重视,然而,它在面对不可满足问题例时的局限性不能不被考虑．分级重排搜索算法ＭＳＲＡ（ｍｕｌｔｉ－ｓｔａｇｅｓｅａｒｃｈｒｅａｒｒａｎｇｅ－ｍｅｎｔａｌｇｏｒｉｔｈｍ）正是为克服局部搜索法的不完备性而提出的,准确地讲,它是几种算法在思想上的集成,但为明确起见,把其最典型的分级重排过程作为名称．分级重排搜索算法在求解ＳＡＴ问题时,能表现出优于单一求解策略（如局部搜索法或回溯算法）的明显特性．由于可根据约束条件的强弱来估计ＳＡＴ问题例的可满足性,因此能够以此来确定更有效的求解策略．     

Weak Schur numbers and the search for G.W. Walker’s lost partitions

A set A of integers is weakly sum-free if it contains no three distinct elements x,y,z such that x+y=z. Given k≥1, let WS(k) denote the largest integer n for which {1,…,n} admits a partition into k weakly sum-free subsets. In 1952, G.W. Walker claimed the value WS(5)=196, without proof. Here we show WS(5)≥196, by constructing a partition of {1,…,196} of the required type. It remains as an open problem to prove the equality. With an analogous construction for k=6, we obtain WS(6)≥572. Our approach involves translating the construction problem into a Boolean satisfiability problem, which can then be handled by a SAT solver.     

随机算法异步并行化的效率分析

随机算法的执行时间具有不确定性,这种不确定性为随机算法的异步并行提供了良好的基础,已有许多计算实验表明了随机算法的异步并行可以达到线性甚至超线性的加速.对于求解SAT问题的随机算法RDP,研究了异步并行效率与运行时间分布和处理器数目之间的关系.应用一种单峰分布──分段线性分布模型来模拟随机算法的运行时间分布.理论分析和计算结果均表明:当处理器数目k较小和单峰位于分布的前部时,随机算法的异步并行具有近线性加速.