两种改进的模拟退火算法求解大值域约束满足问题

随机约束满足问题的相变现象及求解算法是NP-完全问题的研究热点。RB模型（Revised B）是一个非平凡的随机约束满足问题,它具有精确的可满足性相变现象和极易产生难解实例这两个重要特征。针对RB模型这一类具有大值域的随机约束满足问题,提出了两种基于模拟退火的改进算法即RSA（Revised Simulated Annealing Algorithm）和GSA（Genetic-simulated Annealing Algorithm）。将这两种算法用于求解RB模型的随机实例,数值实验结果表明：在进入相变区域时,RSA和GSA算法依然可以有效地找到随机实例的解,并且在求解效率上明显优于随机游走算法。在接近相变阈值点时,由这两种算法得到的最优解仅使得极少数的约束无法满足。     

Many hard examples in exact phase transitions

This paper analyzes the resolution complexity of two random constraint satisfaction problem (CSP) models (i.e. Model RB/RD) for which we can establish the existence of phase transitions and identify the threshold points exactly. By encoding CSPs into CNF formulas, it is proved that almost all instances of Model RB/RD have no tree-like resolution proofs of less than exponential size. Thus, we not only introduce new families of CSPs and CNF formulas hard to solve, which can be useful in the experimental evaluation of CSP and SAT algorithms, but also propose models with both many hard instances and exact phase transitions. Finally, conclusions are presented, as well as a detailed comparison of Model RB/RD with the Hamiltonian cycle problem and random 3-SAT, which, respectively, exhibit three different kinds of phase transition behavior in NP-complete problems.     

Variable-Centered Consistency in Model RB

Model RB is a model of random constraint satisfaction problems, which exhibits exact satisfiability phase transition and many hard instances, both experimentally and theoretically. Benchmarks based on Model RB have been successfully used by various international algorithm competitions and many research papers. In a previous work, Xu and Li defined two notions called i-constraint assignment tuple and flawed i-constraint assignment tuple to show an exponential resolution complexity of Model RB. These two notions are similar to some kind of consistency in constraint satisfaction problems, but seem different from all kinds of consistency so far known in literatures. In this paper, we explicitly define this kind of consistency, called variable-centered consistency, and show an upper bound on a parameter in Model RB, such that up to this bound the typical instances of Model RB are variable-centered consistent.     

可满足实例的归结复杂度

GRB模型是一种随机约束满足问题模型,此模型具有精确的可满足相变现象。针对实验中出现的GRB模型在相变区域产生的可满足实例都是难解的现象,利用子句宽度和归结复杂度的关系证明了GRB模型在相变点附近产生的可满足实例对于树型归结证明具有指数下界。因此从理论上证明了在相变区域产生的可满足实例对基于归结的算法是难解的。     

置信传播和模拟退火相结合求解约束满足问题

约束满足问题是人工智能领域的一个重要问题。针对一个具有精确相变现象和能产生大量难解实例的随机约束满足问题,提出了置信传播和模拟退火相结合的求解算法。这种算法先通过置信传播方程收敛后得到变量取值的边际概率分布,分别采用最大概率和最小分量熵的策略产生一组启发式的初始赋值,再用模拟退火对这组赋值进行修正。实验结果表明：该算法大大提高了初始赋值向最优解收敛的速度,表现出了显著优越于模拟退火算法的求解性能。     

一种基于变量熵求解约束满足问题的置信传播算法

在置信传播(belief propagation,BP)算法中,提出一种基于变量熵来挑选变量从而固定变量赋值的策略,用于求解一类具有增长定义域的随机约束满足问题.RB模型是一个具有增长定义域的随机约束满足问题的典型代表,已经严格证明它不仅存在精确的可满足性相变现象,而且可以生成难解实例.在RB模型上选取两组不同的参数进行数值实验.结果表明:在接近可满足性相变点时,BP引导的消去算法仍然可以非常有效地找到随机实例的解;不断增加问题的规模,算法的运行时间呈指数级增长;并且当控制参数(约束紧度)增加时,变量的平均自由度逐渐降低.     

The satisfiability problem in regular CNF-formulas

 In this paper we deal with the propositional satisfiability (SAT) problem for a kind of multiple-valued clausal forms known as regular CNF-formulas and extend some known results from classical logic to this kind of formulas. We present a Davis–Putnam-style satisfiability checking procedure for regular CNF-formulas equipped with suitable data structures and prove its completeness. Then, we describe a series of experiments for regular random 3-SAT instances. We observe that, for the regular 3-SAT problem with this procedure, there exists a threshold of the ratio of clauses to variables such that (i) the most computationally difficult instances tend to be found near the threshold, (ii) there is a sharp transition from satisfiable to unsatisfiable instances at the threshold and (iii) the value of the threshold increases as the number of truth values considered increases. Instances in the hard part provide benchmarks for the evaluation of regular satisfiability solvers.     

随机约束满足问题的回溯算法分析

提出一种新的随机CSP(constraint sa tisfaction problem)模型,并且通过研究搜索树的平均节点数,分析了回溯算法求解该模型 的平均复杂性.结果表明,这种模型能够生成难解的CSP实例,找到所有的解或证明无解所需的 平均节点数即随变量数的增加而指数增长.因此,该模型可以用来研究难解实例的性质和CSP 算法的性能等问题,从而有助于设计出更为高效的算法.     

Easy problems are sometimes hard

We present a detailed experimental investigation of the easy-hard-easy phase transition for randomly generated instances of satisfiability problems. Problems in the hard part of the phase transition have been extensively used for benchmarking satisfiability algorithms. This study demonstrates that problem classes and regions of the phase transition previously thought to be easy can sometimes be orders of magnitude more difficult than the worst problems in problem classes and regions of the phase transition considered hard. These difficult problems are either hard unsatisfiable problems or are satisfiable problems which give a hard unsatisfiable subproblem following a wrong split. Whilst these hard unsatisfiable problems may have short proofs, these appear to be difficult to find, and other proofs are long and hard.     

An Average Analysis of Backtracking on Random Constraint Satisfaction Problems

In this paper we propose a random CSP model, called Model GB, which is a natural generalization of standard Model B. This paper considers Model GB in the case where each constraint is easy to satisfy. In this case Model GB exhibits non-trivial behaviour (not trivially satisfiable or unsatisfiable) as the number of variables approaches infinity. A detailed analysis to obtain an asymptotic estimate (good to 1+o(1)) of the average number of nodes in a search tree used by the backtracking algorithm on Model GB is also presented. It is shown that the average number of nodes required for finding all solutions or proving that no solution exists grows exponentially with the number of variables. So this model might be an interesting distribution for studying the nature of hard instances and evaluating the performance of CSP algorithms. In addition, we further investigate the behaviour of the average number of nodes as r (the ratio of constraints to variables) varies. The results indicate that as r increases, random CSP instances get easier and easier to solve, and the base for the average number of nodes that is exponential in n tends to 1 as r approaches infinity. Therefore, although the average number of nodes used by the backtracking algorithm on random CSP is exponential, many CSP instances will be very easy to solve when r is sufficiently large.     

警示传播算法收敛的充分条件

信息传播算法求解可满足问题时有惊人的效果,难解区域变窄.然而,因子图带有环的实例,信息传播算法不总有效,常表现为不收敛.对于这种现象,至今缺少系统的理论解释.警示传播（warning propagation,简称WP）算法是一种基础的信息传播算法,对WP算法的收敛性研究是其他信息传播算法收敛性研究的重要基础.在WP算法中,将警示信息的取值从{0,1}松弛为[0,1],利用压缩函数的性质,给出了WP算法收敛的一个充分条件.选取了两组不同规模的随机3-SAT实例进行实验模拟,结果表明：当子句与变元的比值α<1.8时,该判定条件有效.     

Configuration landscape analysis and backbone guided local search.: Part I: Satisfiability and maximum satisfiability

Boolean satisfiability (SAT) and maximum satisfiability (Max-SAT) are difficult combinatorial problems that have many important real-world applications. In this paper, we first investigate the configuration landscapes of local minima reached by the WalkSAT local search algorithm, one of the most effective algorithms for SAT. A configuration landscape of a set of local minima is their distribution in terms of quality and structural differences relative to an optimal or a reference solution. Our experimental results show that local minima from WalkSAT form large clusters, and their configuration landscapes constitute big valleys, in that high quality local minima typically share large partial structures with optimal solutions. Inspired by this insight into WalkSAT and the previous research on phase transitions and backbones of combinatorial problems, we propose and develop a novel method that exploits the configuration landscapes of such local minima. The new method, termed as backbone-guided search, can be embedded in a local search algorithm, such as WalkSAT, to improve its performance. Our experimental results show that backbone-guided local search is effective on overconstrained random Max-SAT instances. Moreover, on large problem instances from a SAT library (SATLIB), the backbone guided WalkSAT algorithm finds satisfiable solutions more often than WalkSAT on SAT problem instances, and obtains better solutions than WalkSAT on Max-SAT problem instances, improving solution quality by 20% on average.     

Spines of random constraint satisfaction problems: definition and connection with computational complexity

We study the connection between the order of phase transitions in combinatorial problems and the complexity of decision algorithms for such problems. We rigorously show that, for a class of random constraint satisfaction problems, a limited connection between the two phenomena indeed exists. Specifically, we extend the definition of the spine order parameter of Bollobás et al. [10] to random constraint satisfaction problems, rigorously showing that for such problems a discontinuity of the spine is associated with a 2^Ω(n) resolution complexity (and thus a 2^Ω(n) complexity of DPLL algorithms) on random instances. The two phenomena have a common underlying cause: the emergence of “large” (linear size) minimally unsatisfiable subformulas of a random formula at the satisfiability phase transition.We present several further results that add weight to the intuition that random constraint satisfaction problems with a sharp threshold and a continuous spine are “qualitatively similar to random 2-SAT”. Finally, we argue that it is the spine rather than the backbone parameter whose continuity has implications for the decision complexity of combinatorial problems, and we provide experimental evidence that the two parameters can behave in a different manner.AMS subject classification 68Q25, 82B27     

Hard constraint satisfaction problems have hard gaps at location 1

An instance of the maximum constraint satisfaction problem (Max CSP) is a finite collection of constraints on a set of variables, and the goal is to assign values to the variables that maximises the number of satisfied constraints. Max CSP captures many well-known problems (such as Maxk-SAT and Max Cut) and is consequently NP-hard. Thus, it is natural to study how restrictions on the allowed constraint types (or constraint language) affect the complexity and approximability of Max CSP. The PCP theorem is equivalent to the existence of a constraint language for which Max CSP has a hard gap at location 1; i.e. it is NP-hard to distinguish between satisfiable instances and instances where at most some constant fraction of the constraints are satisfiable. All constraint languages, for which the CSP problem (i.e., the problem of deciding whether all constraints can be satisfied) is currently known to be NP-hard, have a certain algebraic property. We prove that any constraint language with this algebraic property makes Max CSP have a hard gap at location 1 which, in particular, implies that such problems cannot have a PTAS unless P=NP. We then apply this result to Max CSP restricted to a single constraint type; this class of problems contains, for instance, Max Cut and Max DiCut. Assuming P≠NP, we show that such problems do not admit PTAS except in some trivial cases. Our results hold even if the number of occurrences of each variable is bounded by a constant. Finally, we give some applications of our results.     

Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances

An analysis of the average-case complexity of solving random 3-Satisfiability (SAT) instances with backtrack algorithms is presented. We first interpret previous rigorous works in a unifying framework based on the statistical physics notions of dynamical trajectories, phase diagram and growth process. It is argued that, under the action of the Davis–Putnam–Loveland–Logemann (DPLL) algorithm, 3-SAT instances are turned into 2+p-SAT instances whose characteristic parameters (ratio of clauses per variable, fraction p of 3-clauses) can be followed during the operation, and define resolution trajectories. Depending on the location of trajectories in the phase diagram of the 2+p-SAT model, easy (polynomial) or hard (exponential) resolutions are generated. Three regimes are identified, depending on the ratio of the 3-SAT instance to be solved. Lower satisfiable (sat) phase: for small ratios, DPLL almost surely finds a solution in a time growing linearly with the number N of variables. Upper sat phase: for intermediate ratios, instances are almost surely satisfiable but finding a solution requires exponential time (2^Nω with ω>0) with high probability. Unsat phase: for large ratios, there is almost always no solution and proofs of refutation are exponential. An analysis of the growth of the search tree in both upper sat and unsat regimes is presented, and allows us to estimate ω as a function of . This analysis is based on an exact relationship between the average size of the search tree and the powers of the evolution operator encoding the elementary steps of the search heuristic.     

Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints

Much research in the area of constraint processing has recently been focused on extracting small unsatisfiable “cores” from unsatisfiable constraint systems with the goal of finding minimal unsatisfiable subsets (MUSes). While most techniques have provided ways to find an approximation of an MUS (not necessarily minimal), we have developed a sound and complete algorithm for producing all MUSes of an unsatisfiable constraint system. In this paper, we describe a relationship between satisfiable and unsatisfiable subsets of constraints that we subsequently use as the foundation for MUS extraction algorithms, implemented for Boolean satisfiability constraints. The algorithms provide a framework with which many related subproblems can be solved, including relaxations of completeness to handle intractable instances, and we develop several variations of the basic algorithms to illustrate this. Experimental results demonstrate the performance of our algorithms, showing how the base algorithms run quickly on many instances, while the variations are valuable for producing results on instances whose complete results are intractably large. Furthermore, our algorithms are shown to perform better than the existing algorithms for solving either of the two distinct phases of our approach.     

Improving configuration checking for satisfiable random <Emphasis Type="Italic">k</Emphasis>-SAT instances

Local search algorithms based on the Configuration Checking (CC) strategy have been shown to be efficient in solving satisfiable random k-SAT instances. The purpose of the CC strategy is to avoid the cycling problem, which corresponds to revisiting already flipped variables too soon. It is done by considering the neighborhood of the formula variables. In this paper, we propose to improve the CC strategy on the basis of an empirical study of a powerful algorithm using this strategy. The first improvement introduces a new and simple criterion, which refines the selection of the variables to flip for the 3-SAT instances. The second improvement is achieved by using the powerful local search algorithm Novelty with the adaptive noise setting. This algorithm enhances the efficiency of the intensification and diversification phases when solving k-SAT instances with k ≥ 4. We name the resulting local search algorithm Ncca+ and show its effectiveness when treating satisfiable random k-SAT instances issued from the SAT Challenge 2012. Ncca+ won the bronze medal of the random SAT track of the SAT Competition 2013.     

Scalable satisfiability checking and test data generation from modeling diagrams

We explore the automatic generation of test data that respect constraints expressed in the Object-Role Modeling (ORM) language. ORM is a popular conceptual modeling language, primarily targeting database applications, with significant uses in practice. The general problem of even checking whether an ORM diagram is satisfiable is quite hard: restricted forms are easily NP-hard and the problem is undecidable for some expressive formulations of ORM. Brute-force mapping to input for constraint and SAT solvers does not scale: state-of-the-art solvers fail to find data to satisfy uniqueness and mandatory constraints in realistic time even for small examples. We instead define a restricted subset of ORM that allows efficient reasoning yet contains most constraints overwhelmingly used in practice. We show that the problem of deciding whether these constraints are consistent (i.e., whether we can generate appropriate test data) is solvable in polynomial time, and we produce a highly efficient (interactive speed) checker. Additionally, we analyze over 160 ORM diagrams that capture data models from industrial practice and demonstrate that our subset of ORM is expressive enough to handle their vast majority.     

Random 2-SAT with Prescribed Literal Degrees

Two classic "phase transitions" in discrete mathematics are the emergence of a giant component in a random graph as the density of edges increases, and the transition of a random 2-SAT formula from satisfiable to unsatisfiable as the density of clauses increases. The random-graph result has been extended to the case of prescribed degree sequences, where the almost-sure nonexistence or existence of a giant component is related to a simple property of the degree sequence. We similarly extend the satisfiability result, by relating the almost-sure satisfiability or unsatisfiability of a random 2-SAT formula to an analogous property of its prescribed literal-degree sequence. The extension has proved useful in analyzing literal-degree-based algorithms for (uniform) random 3-SAT.     

A graph-based immune-inspired constraint satisfaction search

We propose an artificial immune algorithm to solve constraint satisfaction problems (CSPs). Recently, bio-inspired algorithms have been proposed to solve CSPs. They have shown to be efficient in solving hard problem instances. Given that recent publications indicate that immune-inspired algorithms offer advantages to solve complex problems, our main goal is to propose an efficient immune algorithm which can solve CSPs. We have calibrated our algorithm using relevance estimation and value calibration (REVAC), which is a new technique recently introduced to find the parameter values for evolutionary algorithms. The tests were carried out using randomly generated binary constraint satisfaction problems and instances of the three-colouring problem with different constraint networks. The results suggest that the technique may be successfully applied to solve CSPs.