利用近似解加速求解SAT问题的启发式完全算法

结合DPLL完全算法能够证明可满足性(SAT)问题的不可满足性和局部搜索算法快速的优点,提出利用近似解加速求解SAT问题的启发式完全算法.首先利用局部搜索算法快速地得到一个近似解,并将该近似解作为完全算法的初始输入,用于其中分支变量的相位决策.该算法引导完全算法优先搜索近似解所在的子空间,加速解决器找到可满足解的过程,为SAT问题的求解提供了一种新的有效途径.实验结果表明,该算法有效地提高了决策的精度和SAT解决器的效率,对很多实例非常有效.     

基于寻找可满足2SAT子问题的SAT算法*

可满足问题（SAT）是一个NP-Hard问题。提出了一种求解SAT的新算法（FFSAT）。该算法将SAT问题转换为寻找一个可满足的2-SAT子问题。SAT问题虽然是NP完全问题,但是当所有子句长度不大于2时,SAT问题可以在线性时间求解。使用2-SAT算法-BinSat求解2-SAT子问题,当它不满足时,根据赋值选择新的2-SAT子问题。实验结果表明,采用本算法的结果优于UnitWalk。     

二元可满足性问题有解的充要条件

二元可满足性问题是一个多项式可解的问题．本文首先证明了该问题有解的充要条件，然后给出了判定该问题的一个新的多项式算法．如果判定某个表达式是可满足的话，那么求解算法不需要任何回溯就能准确地给出它的每个解．本文试图通过对二元可满足性的研究为研究其它问题提供一点启示．     

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

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

O(m~2)时间求解SAT问题的随机算法

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

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

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

可满足问题中的模型计数

模型计数问题是指计算给定问题的解的个数,这是一类比决策更困难的问题,也是人工智能领域研究的一个热点问题.对模型计数问题的研究不仅可以提高算法的求解效率,更能促进对问题困难本质的了解.以可满足问题（命题可满足（SAT）和约束可满足问题（CSP））为例,从精确算法和近似求解两方面综述了模型计数问题的研究现状,重点介绍了相关概念以及各个算法之间的优缺点,并提出了有待解决的开放性问题,对模型计数问题的研究予以了总结和展望.     

求解SAT问题的线性半定规划算法

将线性半定规划应用到SAT问题的求解过程中。首先将SAT实例转化为整数规划问题,然后松弛为线性规划模型,最后再转化为一般的线性半定规划模型去求解。用SDPA-M软件求解线性半定规划问题后,规定了如何根据目标函数值去判定SAT实例和当CNF公式可满足时如何根据最优指派的概率X^＊i（i=1,…,n）去进行变元赋值,以期求得该公式的可满足指派。上述算法不仅可以判定SAT问题,而且对于符合算法规定可满足的CNF公式皆可给出一个可满足指派。求解SAT问题的线性半定规划算法在文章中被描述并被给予相应算例。     

求解SAT问题的改进粒子群优化算法

利用限制哆公式的相关理论将可满足性问题（SAT）等价转换为定义在{0，1}^n上的多项式函数优化问题，并将二进制粒子群优化算法（BPSO）与局部爬山搜索策略相结合，给出了一种求解SAT问题的新算法：基于局部爬山搜索的改进二进制粒子群优化算法（简称IBPSO）．数值实验表明，对于随机产生的3-SAT问题测试实例，该算法的计算结果均优于著名的WalkSAT算法和SATI．3算法．     

求解多文字可满足SAT问题的置信传播算法

可满足(SAT)问题是指:是否存在一组布尔变元赋值,使得合取范式公式中每个子句至少有一个文字为真.多文字可满足SAT问题是指:是否存在一组布尔变元赋值,使得CNF公式中每个子句至少有两个文字为真.显然,此问题仍然是一个NP难问题.为了研究解决多文字可满足SAT问题的算法,引入随机实例产生模型,设计求解多文字可满足SAT问题的置信传播算法.最后,用实例模型产生了大量数据进行实验验证,结果表明:该算法求解多文字可满足SAT问题的性能优于其他启发式算法.     

Computing An Optimal Hatching Direction In Layered Manufacturing

In Layered Manufacturing (LM), a prototype of a virtual polyhedral object is built by slicing the object into polygonal layers, and then building the layers one after another. In StereoLithography, a specific LM-technology, a layer is built using a laser which follows paths along equally-spaced parallel lines and hatches all segments on these lines that are contained in the layer. We consider the problem of computing a direction of these lines for which the number of segments to be hatched is minimum, and present an algorithm that solves this problem exactly. The algorithm has been implemented and experimental results are reported for real-world polyhedral models obtained from industry.     

Code generation based on formal BURS theory and heuristic search

BURS theory provides a powerful mechanism to efficiently generate pattern matches in a given expression tree. BURS, which stands for bottom-up rewrite system, is based on term rewrite systems, to which costs are added. We formalise the underlying theory, and derive an algorithm that computes all pattern matches. This algorithm terminates if the term rewrite system is finite. We couple this algorithm with the well-known search algorithm A that carries out pattern selection. The search algorithm is directed by a cost heuristic that estimates the minimum cost of code that has yet to be generated. The advantage of using a search algorithm is that we need to compute only those costs that may be part of an optimal rewrite sequence (and not the costs of all possible rewrite sequences as in dynamic programming). A system that implements the algorithms presented in this work has been built. Received: 20 November 1995 / 26 June 1996     

行为建模及其在多Agent系统中的应用

五行学说蕴含信息动力学,然而在网络中却一直未被很好地利用,为此提出一种基于五行原理的五行粒子模型方法来求解多Agent系统的分布式问题。五行粒子模型可以很好地描述和处理多Agent系统中Agent之间存在的随机、并发、多类型的交互行为。基于五行粒子模型内部存在的生克关系,以及五行自身蕴含的稳定性和平衡性,对五行粒子模型和多Agent系统分布式问题求解进行探讨,并对多Agent系统中的各个Agent进行行为建模,进而提出多Agent系统分布式问题求解的五行粒子模型算法。最后,通过实验验证了该算法的有效性。     

基于DBR理论的柔性流水车间动态调度

针对柔性流水车间动态调度求解困难的问题,首先分析调度问题的特征,构建问题模型;然后运用DBR（鼓-缓冲器-绳子）理论对问题进行分解简化,并采用混合重调度策略和启发式算法进行动态调度;最后建立瓶颈和非瓶颈资源调度的协调机制,实现问题求解.仿真实例表明,所提出的算法是可行而有效的.     

交叉熵方法在车辆路径问题中的应用研究

车辆路径问题已被研究证实为NP 难题,属于经典的复杂组合优化问题。首先建立了带货物权重的随机需求的车辆路径问题的模型;其次针对问题的性质,设计了一种基于交叉熵方法的算法对问题进行求解;最后计算结果验证了所提算法对于解决此类问题的有效性。     

一种基于遗传算法的软件测试用例生成新方法

建立了一个基于遗传算法测试用例生成的系统模型,在该模型下通过分支函数插装的方法构造遗传算法所需的评价函数并针对软件测试用例生成问题的特点对传统遗传算法进行了改进;最后,给出了一个实例并分析了实例的执行情况。     

Deleting files in the Celeste peer-to-peer storage system

Celeste is a robust peer-to-peer object store built on top of a distributed hash table (DHT). Celeste is a working system, developed by Sun Microsystems Laboratories. During the development of Celeste, we faced the challenge of complete object deletion, and moreover, of deleting “files” composed of several different objects. This important problem is not solved by merely deleting meta-data, as there are scenarios in which all file contents must be deleted, e.g., due to a court order. Complete file deletion in a realistic peer-to-peer storage system has not been previously dealt with due to the intricacy of the problem — the system may experience high churn rates, nodes may crash or have intermittent connectivity, and the overlay network may become partitioned at times. We present an algorithm that eventually deletes all file contents, data and meta-data, in the aforementioned complex scenarios. The algorithm is fully functional and has been successfully integrated into Celeste.     

用于网格计算的Overlay Network设计算法的研究*

针对如何提供丰富的通信交互提出了一种基于Overlay Network的网格架构,设计Overlay Network,给出了一种动态环境中分布式拉格朗日启发式算法DLagr OTDP,计算的结果显示该算法具有更快的适应性。     

加权SVDD算法在人体姿态估计中的研究与应用

支持向量数据描述（SVDD）算法是解决单类分类问题的最好方法之一,在人体姿态估计问题中获得了成功的应用,在建立部位外观模型方面取得了良好的效果,但现有利用SVDD算法建立的部位外观模型将所有训练样本和样本不同特征都平等对待。为克服存在的这两个缺陷,提出了一种样本和特征加权的SVDD算法,并用其建立了一种基于样本和特征加权SVDD算法的部位外观模型。样本的权重系数根据样本到样本中心的距离远近来确定,样本特征的权重系数根据特征对应图像区域被训练图像中真实人体部位包含次数的多少来确定。仿真实验结果表明所建立的部位外观模型比利用标准SVDD算法建立的部位外观模型能更准确地描述真实人体部位的外观,能得到更高的人体姿态估计准确度。     

不确定旅行商问题的鲁棒模型与算法

考虑到不确定参数在旅行商问题(TSP)中广泛存在,在Bertsimas鲁棒离散优化理论的框架下,建立了不确定旅行商问题的鲁棒优化模型,并按转换规则将鲁棒模型转换为鲁棒对等模型。给出了一种求解旅行商问题的基于Prufer数编码的单亲遗传算法,与求解该类问题的传统遗传算法相比,该算法缩减了染色体长度,避免了传统交叉和变异操作破坏染色体可行解的缺陷。通过算例验证,表明该算法有较高的求解效率,所建立的鲁棒模型在不确定环境下能得到较好的鲁棒解。