集装箱装载的一种启发式算法

多约束条件下的三维装箱问题是一个复杂的组合优化问题,属于NP-HARD问题，其求解是很 困难的．所以在实际应用中,往往采用一些启发式算法来求解．本文在考虑一些实际应用中 的约束条件下，提出了一种三维集装箱装载的启发式算法．此算法采用了三空间分割、平均 高度装载、货物合并、空间合并等策略，考虑了方向、重量、优先顺序、货物的配置位置等 约束条件．通过逐步淘汰差的装载方案，最后达到满意的装载．实例仿真说明了该算法的有 效性和实用性，能够直接用于实际应用中．     

基于子句的动态检查强制文字的SAT求解器

检查强制文字是一种重要的预处理方法。结合学习子句,提出一种在求解过程中使用的策略—基于子句的动态检查强制文字(CNL),并且设计了一种易实现低成本的数据结构。分别实现了两个不同版本的求解器:Glucose_PRE和Glucose_CNL,前者在求解初始时将检查强制文字作为预处理,后者实现了基于子句的动态检查强制文字策略。实验测试结果表明,与Glucose_PRE和Glucose3.0求解器相比,求解器Glucose_CNL在求解2015年和2016年SAT竞赛的应用类型的实例时,求解实例个数更多,耗时更少,说明所提策略和所设计的数据结构均可提高求解器的求解性能。     

几何约束求解研究综述

综述了几何约束求解的历史发展、研究现状和应用．对常见的4类求解方法：数值计算的方法、符号计算的方法、基于规则的方法、基于图论的方法做了详细的介绍．同时还列举了几何约束求解在计算机视觉、连杆设计、机器人、分子结构设计和计算机辅助教学等方面的应用实例．     

一种新的求解无相关鉴别矢量集方法

无相关鉴别矢量集方法是解决模式识别问题的有效方法．通常情况下，无相关鉴别矢量集是通过递归方式获得的，计算时间较长．该文提出了一种求解无相关鉴别矢量集的非递归方法．首先根据总体散布矩阵构造无相关投影空间．对于无相关投影空间中的任何正交矢量集，其在原空间中的特征统计无关．然后在无相关投影空间求解基于Fisher线性判别准则的正交矢量集，从而得到原空间的无相关鉴别矢量集．理论分析和实验结果表明：该文方法和Jin等的方法所求解的无相关鉴别矢量集是一致的．而应用本文方法求解无相关鉴别矢量集计算时间较短，在类别数为C的情况下，二者的时间比为(C-1)：2．     

二维点模式图像的仿射变换配准

提出了一种图像特征点配准算法．该算法为二维点模式图像仿射配准建立了新的求解模型,此模型对参考图像的特征点集和浮动图像的特征点集分别进行Whitening变换,将点集间的一般仿射变换问题转换为刚性变换问题;在对刚性变换求解时,采用平滑性好、局部极值较少的新的目标函数;并引入了形变程度分量,使该算法更能符合实际应用．结合文中提出的新的仿射不变量,目标函数只需在平分法的基础上加入随机因素便能快速求解．实验结果证明,该算法在处理特征点仿射配准问题上具有速度快、精度高的特点．     

一个求解非线性方程组的区间检验算法

引言非线性方程组的数值求解一直是计算数学的中心任务之一，越来越受到人们的重视．以Newton迭代法为代表的点迭代方法一直是被广泛运用的求解方法．但是，点迭代方法难以进行可靠的误差估计，且对迭代初值有较为苛刻的要求．本世纪七十年代以后兴起的区间分析方法可用于求解非线性方程组，特别在解的误差估计和解的存在性检验方面是卓有成效的．但是，区间方法的致命缺点是计算速度慢，运算量大；而且由于区间运算的复杂性，其程序的实现难度很大，有时甚至难以用于实际计算．这些缺点严重地限制了区间方法的应用和发展．因此，人们自然…     

基于线性规划的RTL可满足性求解和性质检验

采用线性规划作为基本工具开发一个RTL可满足性求解器，并将其应用于解决RTL性质检验问题．深入研究了使用线性规划约束对RTL电路元器件的建模方法，得到了一种对RTL电路建模的通用方法．通过将RTL性质转化为虚拟RTL电路，找到了一种验证RTL性质的方法．通过实验，并与采用zchaff布尔可满足性求解器的模型检验工具NuSMV进行比较，证明了基于RTL可满足性求解器的性质验证方法在内存和时间消耗上具有相当大的优势．     

大型稀疏线性方程组新的ICCG方法

有限元线性方程组的系数矩阵一般具有稀疏性和对称性的特点,全稀疏存贮方法就是利用这些特点,只存贮对称部分的非零元素,采用链表式管理,即节省存贮空间,又便于动态更改．在完全Cholesky分解的基础上,构造出了新的预处理方法,应用适当的对角元修正策略,得到了一种新的ICCG方法,能够确保方程组高效准确的分解和求解．数值算例证明该算法在时间和存贮上都较为占优,可靠高效,能够应用于有限元线性方程组的求解．     

最大可行流问题中增值链的一种回溯求解算法

本文就最大可行流问题给出了一种回溯求解的算法，并证明了不可扩展结点的可剪裁性问题，旨在减少后续可能的搜索空间．在一定程度上可以减少求解过程中的时间消耗．     

一个约束可满足性问题的演化算法求解

约束可满足性问题是一大类常出现于现实应用中的复杂问题，因其繁多的约束条件而出名。本文针对一个经典的约束可满足性问题——斑马属谁问题．基于演化算法的框架进行求解。我们采用矩阵的表示方式．并设计了相应的杂交和变异算予。实验表明．演化算法能高效地解决该问题。     

A survey of recent advances in SAT-based formal verification

Dramatic improvements in SAT solver technology over the last decade and the growing need for more efficient and scalable verification solutions have fueled research in verification methods based on SAT solvers. This paper presents a survey of the latest developments in SAT-based formal verification, including incomplete methods such as bounded model checking and complete methods for model checking. We focus on how the surveyed techniques formulate the verification problem as a SAT problem and how they exploit crucial aspects of a SAT solver, such as application-specific heuristics and conflict-driven learning. Finally, we summarize the noteworthy achievements in this area so far and note the major challenges in making this technology more pervasive in industrial design verification flows.     

使用输出分组和电路可满足性的等价性验证算法

介绍了一种使用电路可满足性解算器的组合电路等价性验证算法．对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题．同时,注意各个子问题间的有用隐含信息的共享,减小了SAT推理的搜索空间．实验结果表明,该算法是实用有效的．     

应用吴方法进行高层次定界模型检验

以吴方法为理论基础,提出一种针对高层次设计验证的定界模型检验方法.通过使用多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并用吴方法有效地解决该定理证明问题.实验结果表明,与基于布尔SAT、基于LP的RTL SAT以及基于非线性求解器的性质检验方法相比,该方法在时间消耗上具有相当大的优势.     

Solving satisfiability in combinational circuits

As EDA evolves, researchers continue to find modeling tools to solve problems of test generation, design verification, logic, and physical synthesis, among others. One such modeling tool is Boolean satisfiability (SAT), which has very broad applicability in EDA. The authors review modern SAT algorithms, show how these algorithms can account for structural information in combinational circuits, and explain what recursive learning can add to SAT.     

Compositional encoding for bounded model checking

Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, a highly non-trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit onthe-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems.     

原理图自动审查系统中的协同技术

该文提出了一种原理图级电路设计自动审查系统协同设计实现方案。这种技术的关键就在于将设计和测试向量融为一体,即当设计和测试单独进行时,能够根据设计资料生成标准的测试向量,依据测试向量实现原理图的自动测试。该文介绍了此协同设计体系的系统结构、集成框架结构及扩展EDA内置的测试功能。     

并发反应式系统的组合模型检验与组合精化检验

模型检验和精化检验是两种重要的形式验证方法,其应用的主要困难在于如何缓解状态爆炸问题.基于分而治之的思想进行组合模型检验和组合精化检验是应对这个问题的重要方法,它们利用系统的组合结构对问题进行分解,通过对各子系统性质的检验和综合推理导出整个系统的性质.在一个统一的框架下对组合模型检验和组合精化检验作了系统的分析和归纳,从模块检验的角度阐述了上述两种组合验证方法的原理及其相应的组合验证策略.同时总结了各类问题的复杂性,并对上述两种方法作了比较分析,揭示了它们之间的内在联系.最后展望了组合模型检验与组合精化检验的发展方向.     

Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure

We present an abstraction refinement algorithm for model checking of safety properties that relies exclusively on a SAT solver for checking the abstract model, testing abstract counterexamples on the concrete model, and refinement. Model checking of the abstractions is based on bounded model checking extended with checks for the existence of simple paths that help in deciding passing properties. All minimum-length spurious counterexamples are eliminated in one refinement step by an incremental procedure that combines the analysis of the conflict dependency graph produced by the SAT solver while looking for concrete counterexamples with an effective refinement minimization procedure.     

Using Markov Chain Based Estimation of Distribution Algorithm for Model-Based Safety Analysis of Graph Transformation

The ability to assess the reliability of safety-critical systems is one of the most crucial requirements in the design of modern safety-critical systems where even a minor failure can result in loss of life or irreparable damage to the environment. Model checking is an automatic technique that verifies or refutes system properties by exploring all reachable states (state space) of a model. In large and complex systems, it is probable that the state space explosion problem occurs. In exploring the state space of systems modeled by graph transformations, the rule applied on the current state specifies the rule that can perform on the next state. In other words, the allowed rule on the current state depends only on the applied rule on the previous state, not the ones on earlier states. This fact motivates us to use a Markov chain (MC) to capture this type of dependencies and applies the Estimation of Distribution Algorithm (EDA) to improve the quality of the MC. EDA is an evolutionary algorithm directing the search for the optimal solution by learning and sampling probabilistic models through the best individuals of a population at each generation. To show the effectiveness of the proposed approach, we implement it in GROOVE, an open source toolset for designing and model checking graph transformation systems. Experimental results confirm that the proposed approach has a high speed and accuracy in comparison with the existing meta-heuristic and evolutionary techniques in safety analysis of systems specified formally through graph transformations.     

基于格局检测的模型计数方法

模型计数是指求出给定命题公式的模型数,是SAT问题的泛化.模型计数在人工智能领域取得了广泛应用,很多现实问题都可以规约为模型计数进行求解.目前,常用的模型计数求解器主要有Cachet与sharpSAT,它们均采用完备方法且具有高效的求解能力,但其求解效率对模型数不敏感.有理由猜测：当给定问题的模型较少时,不完备算法可能发挥其效率优势而更适合模型计数.局部搜索是求解SAT问题的高效不完备方法,Cai等人提出了格局检测策略,并将其应用到局部搜索方法中,提出了SWcc算法,具有很高的求解效率.对SWcc算法进行扩充,分别得到了迭代法与优化后的增量法两种效率较高的不完备模型计数方法,给出了两种方法的思路和具体实现.最后给出了大量测试样例的实验结果,以验证当给定合取范式的模型较少时,该迭代法与优化后的增量法的求解效率有所提升.