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

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

组织进化算法求解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，表现出了优越的性能．     

Accelerating Boolean Satisfiability (SAT) solving by common subclause elimination

Boolean Satisfiability (SAT) is an important problem in many domains. Modern SAT solvers have been widely used in important industrial applications including automated planning and verification. To solve more problems in real applications, new techniques are needed to speed up SAT solving. Inspired by the success of common subexpression elimination in programming languages and other related areas, we study the impact of common subclause elimination (CSE) on SAT solving. Intensive experiments on many SAT solvers and benchmarks with 48-h timeout show that CSE can consistently improve SAT solving. Up to 5% more SAT13 instances can be solved after CSE. LZW-based CSE shows the best overall performance, particularly in the category of application benchmarks. A potential use of this result is that one may consider the heuristic of applying CSE to boost SAT solver performance on real life applications. Because of many possible ways to improve the benefit of CSE, we hope future research can unleash the full potential of CSE in SAT solving.     

求解TSP问题的社会演化算法

将社会演化算法和蚁群算法相结合,以蚁群算法作为认知主体的推理过程,再以范式的学习和更新方式获得最优解,提出一种求解TSP问题的社会演化算法。最后通过两个算例实验仿真与TSP已知最优解进行对比分析,结果表明,社会演化算法在种群规模较小,迭代次数较少的情况下也可获得TSP最优解。     

结合启发式算子的单变量边缘分布算法求解SAT问题

单变量边缘分布算法(UMDA)是一种新的进化算法,是求解复杂问题的一种有效算法.根据SAT问题的特点,本文提出了一种求解SAT问题的改进单变量边缘分布算法(HeUMDASAT),该算法结合SAT问题本身固有的结构信息与当前群体的优秀解所提供的全局信息,构造了一个新的启发算子,并将此算子结合到单变量边缘分布算法中.此算子不同于随机搜索算子,由其产生的个体可以使得算法跳出局部最优并探索新的潜在区域,并且加快算法的收敛速度.用SATLIB库中的标准SAT问题对HeUMDASAT算法进行测试,实验结果表明该算法在求解速度和成功率方面都有明显的改善.     

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

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

由一阶逻辑公式得到命题逻辑可满足性问题实例

命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.     

Hybrid evolutionary method for obstacle location-allocation

In this paper we propose a hybrid evolutionary method for Obstacle Location-allocation problem. This problem can be described as a tri-level mixed integer programming problem. Since this problem is very complex and with many local solutions, no direct method is effective to solve it. Heuristic methods were proposed to it, but optimality is not guaranteed yet. Our hybrid evolutionary method adopts the main structure of Genetic Algorithms (GA) absorbing ideas from Evolutionary Strategy (ES) and combines with some traditional optimization techniques. In this way we can pursue global optimization maintaining a good efficiency of our method. A case study shows the effectiveness of this method.     

Easy Cases of Probabilistic Satisfiability

The Probabilistic Satisfiability problem (PSAT) can be considered as a probabilistic counterpart of the classical SAT problem. In a PSAT instance, each clause in a CNF formula is assigned a probability of being true; the problem consists in checking the consistency of the assigned probabilities. Actually, PSAT turns out to be computationally much harder than SAT, e.g., it remains difficult for some classes of formulas where SAT can be solved in polynomial time. A column generation approach has been proposed in the literature, where the pricing sub-problem reduces to a Weighted Max-SAT problem on the original formula. Here we consider some easy cases of PSAT, where it is possible to give a compact representation of the set of consistent probability assignments. We follow two different approaches, based on two different representations of CNF formulas. First we consider a representation based on directed hypergraphs. By extending a well-known integer programming formulation of SAT and Max-SAT, we solve the case in which the hypergraph does not contain cycles; a linear time algorithm is provided for this case. Then we consider the co-occurrence graph associated with a formula. We provide a solution method for the case in which the co-occurrence graph is a partial 2-tree, and we show how to extend this result to partial k-trees with k>2.     

Fuzzy programming for mixed-integer optimization problems

Mixed-integer optimization problems belong to the group of NP-hard combinatorial problems. Therefore, they are difficult to search for global optimal solutions. Mixed-integer optimization problems are always described by precise mathematical programming models. However, many practical mixed-integer optimization problems have inherited a more or less imprecise nature. Under these circumstances, if we take into account the flexibility of the constraints and the fuzziness of the objectives, the original mixed-integer optimization problems can be formulated as fuzzy mixed-integer optimization problems. Mixed-integer hybrid differential evolution (MIHDE) is an evolutionary search algorithm which has been successfully applied to many complex mixed-integer optimization problems. In this article, a fuzzy mixed-integer mathematical programming model is developed to formulate the fuzzy mixed-integer optimization problem. In addition the MIHDE is introduced to solve the fuzzy mixed-integer programming problem. Finally, the illustrative example shows that satisfactory results can be obtained by the proposed method. This demonstrates that MIHDE can effectively handle fuzzy mixed-integer optimization problems.     

Solving a leader–follower facility problem via parallel evolutionary approaches

A leader–follower facility problem is considered in this paper. The objective is to maximize the profit obtained by a chain (the leader) knowing that a competitor (the follower) will react by locating another single facility after the leader locates its own facility. A subpopulation-based evolutionary algorithm called TLUEGO was recently proposed to cope with this hard-to-solve global optimization problem. However, it requires high computational effort, even to manage small-size problems. In this work, three parallelizations of TLUEGO are proposed, a distributed memory programming algorithm, a shared memory programming algorithm, and a hybrid of the two previous algorithms, which not only allow us to obtain the solution faster, but also to solve larger instances.     

SAT–LP–IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata

As discrete jumps and continuous flows tangle in the behavior of linear hybrid automata (LHA), the bounded model checking (BMC) for reachability of LHA is a challenging problem. Current works try to handle this problem by encoding all the discrete and continuous behaviors in the bound into a set of SMT formulas which can then be solved by SMT solvers. However, when the system size is large, the object SMT problem could be huge and difficult to solve. Instead of encoding everything into one constraint set, this paper proposes a SAT–LP–IIS joint-directed solution to conduct the BMC for reachability of LHA in a layered way. First, the bounded graph structure of LHA is encoded into a propositional formula set, and solved by SAT solvers to find potential paths which can reach the target location on the graph. Then, the feasibility of certain path is encoded into a set of linear constraints which can then be solved by linear programming (LP) efficiently. If the path is not feasible, irreducible infeasible set (IIS) technique is deployed to locate an infeasible path segment which will be fed to the SAT solver to accelerate the enumerating process. Experiments show that by this SAT–LP–IIS joint-directed solution, the memory usage of the BMC of LHA is well-controlled and the performance outperforms the state-of-the-art SMT-style competitors significantly.     

复杂并行机调度问题基于分解的优化算法

针对纺织生产过程中广泛存在的带特殊工艺约束的大规模并行机调度问题，提出了一种基于分解的优化算法。首先将原调度问题分解为机台选择和工件排序两个子问题，然后针对机台选择子问题提出一种进化规划算法，并采用一种具有多项式时间复杂度的最优算法求解工件排序子问题，以得到问题特征信息（即每台机器对应拖期工件数的最小值），该问题特征信息用以指导进化规划算法的迭代过程。不同规模并行机调度问题的数值计算结果及实际制造企业应用效果表明，本文提出的算法是有效的。     

A genetic algorithm/mathematical programming approach to solve a two-level soft drink production problem

This study applies a genetic algorithm embedded with mathematical programming techniques to solve a synchronized and integrated two-level lot sizing and scheduling problem motivated by a real-world problem that arises in soft drink production. The problem considers a production process compounded by raw material preparation/storage and soft drink bottling. The lot sizing and scheduling decisions should be made simultaneously for raw material preparation/storage in tanks and soft drink bottling in several production lines minimizing inventory, shortage and setup costs. The literature provides mixed-integer programming models for this problem, as well as solution methods based on evolutionary algorithms and relax-and-fix approaches. The method applied by this paper uses a new approach which combines a genetic algorithm (GA) with mathematical programming techniques. The GA deals with sequencing decisions for production lots, so that an exact method can solve a simplified linear programming model, responsible for lot sizing decisions. The computational results show that this evolutionary/mathematical programming approach outperforms the literature methods in terms of production costs and run times when applied to a set of real-world problem instances provided by a soft drink company.     

社会认识优化在非线性规划问题中的应用

社会认识优化(Society Cognitive Optimization,SCO)是一种基于社会认知理论提出的模拟人类社会的演化算法.社会认识优化是通过竞争选择和领域搜索来模拟社会认知理论中的社会学习能力,用代理来代表社会中的人,用知识库来代表社会中的知识,通过代理与知识库之间不断的交互来模拟人类的社会学习过程,从而达到优化学习的目的.命题逻辑中合取范式的可满足性(Satisfyability,SAT)问题是当代理论计算机科学的核心问题,是一典型的NP完全问题.可满足性问题的有效解决有着重要的理论意义和实际应用价值.文中将社会认识优化算法应用于求解可满足性问题,得到了比较满意的结果.     

求解随机时变背包问题的精确算法与进化算法

随机时变背包问题(RTVKP)是一种新的动态背包问题,也是一种新的动态组合优化问题,目前它的求解算法主要是动态规划的精确算法、近似算法和遗传算法.本文首先利用动态规划提出了一个求解RTVKP问题的新精确算法,对算法时间复杂度的比较结果表明:它比已有的精确算法更适于求解背包载重较大的一类RTVKP实例.然后,分别基于差分演化和粒子群优化与贪心修正策略相结合,提出了求解RTVKP问题的两个进化算法.对5个RTVKP实例的数值计算结果比较表明: 精确算法一般不宜求解大规模的RTVKP实例,而基于差分演化、粒子群优化和遗传算法与贪心修正策略相结合的进化算法却不受实例规模与数据大小的影响,对于振荡频率大且具有较大数据的大规模RTVKP实例均能求得的一个极好的近似解.     

基于进化规划的多Agent系统任务调度

Agent任务调度是多Agent系统研究的重要内容之一.调度方法直接影响调度方案的优劣与否和系统的执行效率.进化规划是近年来兴起的一种进化计算方法,具有对实数直接操作及全局寻优能力.将之用于Agent任务调度,建立了Agent任务调度模型,设计了进化规划调度算法.采取多个体竞争策略有效地解决了进化规划的早熟问题.实例验证了这种方法的可行性及性能,进一步的研究是在资源及优先度限制的条件下,如何用进化规划算法解决Agent任务调度问题.     

Scheduling projects with multi-skilled personnel by a hybrid MILP/CP benders decomposition algorithm

We study an assignment type resource-con- strained project scheduling problem with resources being multi-skilled personnel to minimize the total staffing costs. We develop a hybrid Benders decomposition (HBD) algorithm that combines the complimentary strengths of both mixed-integer linear programming (MILP) and constraint programming (CP) to solve this NP-hard optimization problem. An effective cut-generating scheme based on temporal analysis in project scheduling is devised for resolving resource conflicts. The computational study shows that our hybrid MILP/CP algorithm is both effective and efficient compared to the pure MILP or CP method alone.     

Local Search-based Hybrid Algorithms for Finding Golomb Rulers

The Golomb ruler problem is a very hard combinatorial optimization problem that has been tackled with many different approaches, such as constraint programming (CP), local search (LS), and evolutionary algorithms (EAs), among other techniques. This paper describes several local search-based hybrid algorithms to find optimal or near-optimal Golomb rulers. These algorithms are based on both stochastic methods and systematic techniques. More specifically, the algorithms combine ideas from greedy randomized adaptive search procedures (GRASP), scatter search (SS), tabu search (TS), clustering techniques, and constraint programming (CP). Each new algorithm is, in essence, born from the conclusions extracted after the observation of the previous one. With these algorithms we are capable of solving large rulers with a reasonable efficiency. In particular, we can now find optimal Golomb rulers for up to 16 marks. In addition, the paper also provides an empirical study of the fitness landscape of the problem with the aim of shedding some light about the question of what makes the Golomb ruler problem hard for certain classes of algorithm.     

Multi-objective optimisation and decision-making of space station logistics strategies

Space station logistics strategy optimisation is a complex engineering problem with multiple objectives. Finding a decision-maker-preferred compromise solution becomes more significant when solving such a problem. However, the designer-preferred solution is not easy to determine using the traditional method. Thus, a hybrid approach that combines the multi-objective evolutionary algorithm, physical programming, and differential evolution (DE) algorithm is proposed to deal with the optimisation and decision-making of space station logistics strategies. A multi-objective evolutionary algorithm is used to acquire a Pareto frontier and help determine the range parameters of the physical programming. Physical programming is employed to convert the four-objective problem into a single-objective problem, and a DE algorithm is applied to solve the resulting physical programming-based optimisation problem. Five kinds of objective preference are simulated and compared. The simulation results indicate that the proposed approach can produce good compromise solutions corresponding to different decision-makers’ preferences.