一种广义分子计算模型及其在 NP问题中的应用

目前各种分子计算模型多基于生物技术,求解一个问题的分子计算机算法很难不作修改地应用于其他类似的问题,尚不似传统计算机般通用。为此,提出一种基于图灵机的广义分子计算模型,其由一台单带图灵机、一条单向只写带和一条工作带组成,通过只写带与工作带之间特殊的映射函数实现并行的同时读、写操作。实验说明了该模型能够在多项式时间求解NP完全的满足性问题（SAT）,比现有分子计算模型在计算准确性和通用性上存在明显优势。     

一种基于单条程序执行路径的错误定位方法

当程序在测试中发生错误时,将形成一条错误的程序执行路径,程序员将会花费很多精力去检测程序代码和定位最终的程序错误．提出一种基于单条程序执行路径的错误定位方法,该方法通过对程序进行反向执行,计算出多个最弱前置条件及其相对应的疑似错误语句集,并生成错误定位树,来辅助程序员进行快速错误定位．对西门子测试数据集进行的实验表明了该方法具有良好的效果．     

一次性求解多个SAT问题

在实际应用中通常需要求解对应CNF（ConjunctiveNormalForm）公式之间仅相差几个子句的一系列SAT（SatisfiabilityProblem）问题,但目前绝大多数SAT求解算法都是针对单一SAT问题设计的。为此,基于DPLL提出了nDPLL算法,并在随机问题上对该算法的效率进行测试。实验结果表明,nDPLL算法能一次性求解多个SAT问题,对于特定范围的CNF公式集具有较高的效率,CNF公式集的规模越大、相近因子越高、子句数和变量数的比值越大,则nDPLL算法的效率越高。     

一种求解命题公式骨干集的警示传播算法

警示传播WP算法是一类重要的信息传播算法,在命题公式的可满足性判定中非常有效。通过对WP算法的数学原理分析发现,当算法收敛时以高概率固定部分变元的赋值,可以对公式进行化简。基于这样的特征修改WP算法的迭代方程和变元赋值条件,设计了一种求解命题公式骨干集的信息传播算法。当变元数目超过400时,与经典骨干集求解算法对比,效率提高了40%,与目前常用算法对比也有10%的提高。结果表明,所提算法求解命题公式骨干集时非常有效。     

基于动态符号执行的C代码缓冲区溢出检测

缓冲区溢出是C程序中众多安全隐患的根源之一,以C程序代码为目标对象,提出了一个基于底层虚拟机中间代码的缓冲区溢出检测工具PathChecker.该工具基于动态符号执行方法,使用无量词谓词公式刻画缓冲区操作的安全性质,并利用可满足模型理论求解器技术检验缓冲区操作的安全性.实验结果表明,该工具能有效检测C代码中的缓冲区溢出漏洞,且易于推广至其他高级程序语言代码和其他类型安全漏洞的检测.     

基于 DNA 自组装的全错位排列问题模型

针对全错位排列这类NP 完全问题,提出了一种基于DNA 自组装的全错位排列问题计算模型。该模型利用了DNA分子间的自组装能力,在具体操作时只用到凝胶电泳技术,在一定程度上减少了实验误差。     

COMPSPEN:对形状性质与数据约束进行融合推理的分离逻辑求解器

分离逻辑是经典霍尔逻辑的针对操作指针和动态数据结构的扩展,已经广泛用于对基础软件(比如操作系统内核等)的分析与验证.分离逻辑约束自动求解是提升对操作指针和动态数据结构的程序的验证的自动化程度的重要手段.针对动态数据结构的验证一般同时涉及形状性质(比如单链表、双链表、树等)和数据性质(比如有序性、数据不变性等).主要介绍能对动态数据结构的形状性质与数据约束进行融合推理的分离逻辑求解器COMPSPEN.首先介绍COMPSPEN的理论基础,包括能够同时描述线性动态数据结构的形状性质和数据约束的分离逻辑子集SLID_data、SLID_data的可满足性和蕴涵问题的判定算法.然后,介绍COMPSPEN工具的基本框架.最后,使用COMPSPEN工具进行了实例研究.收集整理了600个测试用例,在这600个测试用例上将COMPSPEN与已有的主流分离逻辑求解器Asterix、S2S、Songbird、SPEN进行了比较.实验结果表明COMPSPEN是唯一能够求解含有集合数据约束的分离逻辑求解器,而且总体来讲,能对线性数据结构上的同时含有形状性质和线性算术数据约...     

A comparative runtime analysis of heuristic algorithms for satisfiability problems

The satisfiability problem is a basic core NP-complete problem. In recent years, a lot of heuristic algorithms have been developed to solve this problem, and many experiments have evaluated and compared the performance of different heuristic algorithms. However, rigorous theoretical analysis and comparison are rare. This paper analyzes and compares the expected runtime of three basic heuristic algorithms: RandomWalk, (1+1) EA, and hybrid algorithm. The runtime analysis of these heuristic algorithms on two 2-SAT instances shows that the expected runtime of these heuristic algorithms can be exponential time or polynomial time. Furthermore, these heuristic algorithms have their own advantages and disadvantages in solving different SAT instances. It also demonstrates that the expected runtime upper bound of RandomWalk on arbitrary k-SAT (k?3) is O(n(k−1)), and presents a k-SAT instance that has Θ(n(k−1)) expected runtime bound.     

Data reductions, fixed parameter tractability, and random weighted d-CNF satisfiability

Data reduction is a key technique in the study of fixed parameter algorithms. In the AI literature, pruning techniques based on simple and efficient-to-implement reduction rules also play a crucial role in the success of many industrial-strength solvers. Understanding the effectiveness and the applicability of data reduction as a technique for designing heuristics for intractable problems has been one of the main motivations in studying the phase transition of randomly-generated instances of NP-complete problems.In this paper, we take the initiative to study the power of data reductions in the context of random instances of a generic intractable parameterized problem, the weighted d-CNF satisfiability problem. We propose a non-trivial random model for the problem and study the probabilistic behavior of the random instances from the model. We design an algorithm based on data reduction and other algorithmic techniques and prove that the algorithm solves the random instances with high probability and in fixed-parameter polynomial time O(dknm) where n is the number of variables, m is the number of clauses, and k is the fixed parameter. We establish the exact threshold of the phase transition of the solution probability and show that in some region of the problem space, unsatisfiable random instances of the problem have parametric resolution proof of fixed-parameter polynomial size. Also discussed is a more general random model and the generalization of the results to the model.     

随机正则(k,r)-SAT问题的可满足临界

研究k-SAT问题实例中每个变元恰好出现r=2s次,且每个变元对应的正、负文字都出现s次的严格随机正则（k,r）-SAT问题.通过构造一个特殊的独立随机实验,结合一阶矩方法,给出了严格随机正则（k,r）-SAT问题可满足临界值的上界.由于严格正则情形与正则情形的可满足临界值近似相等,因此得到了随机正则（k,r）-SAT问题可满足临界值的新上界.该上界不仅小于当前已有的随机正则（k,r）-SAT问题的可满足临界值上界,而且还小于一般的随机k-SAT问题的可满足临界值.因此,这也从理论上解释了在相变点处的随机正则（k,r）-SAT问题实例通常比在相应相变点处同规模的随机k-SAT问题实例更难满足的原因.最后,数值分析结果验证了所给上界的正确性.