可满足性问题的归约技术(英文)

通过一个恰当的归约变换,可以将一个CNF公式变换为另一个具有某种特殊结构或性质的公式,使其两者具有相同的可满足性。一个典型的归约是将一般的CNF公式变换为3-CNF公式。通过构造一些恰当的工具,可以将公式类变换为所要求的正则类。极小不可满足公式具有一个临界特征,公式本身不可满足,从原始公式中删去任意一个子句后得到的公式可满足。我们提供了一种归约技术,通过构造恰当的极小不可满足公式作为工具,将公式类变换为具有正则结构的公式类。研究正则结构的公式的复杂性及性质很有意义。如,将一个从3-CNF公式变换为(34)-CNF公式,这里(34)-CNF公式是指公式中每个子句的长度恰为3,每个变元出现的次数恰为4。因此,(34)-SAT是一个NP-完全问题,并且正则二部图的诸多良好性质对于研究正则结构的SAT问题具有许多潜在的作用。

Background modeling methods in video analysis： A review and comparative evaluation

Foreground detection methods can be applied to efficiently distinguish foreground objects including moving or static objects from back- ground which is very important in the application of video analysis, especially video surveillance. An excellent background model can obtain a good foreground detection results. A lot of background modeling methods had been proposed, but few comprehensive evaluations of them are available. These methods suffer from various challenges such as illumination changes and dynamic background. This paper first analyzed advantages and disadvantages of various background modeling methods in video analysis applications and then compared their performance in terms of quality and the computational cost. The Change detection.Net （CDnet2014） dataset and another video dataset with different envi- ronmental conditions （indoor, outdoor, snow） were used to test each method. The experimental results sufficiently demonstrated the strengths and drawbacks of traditional and recently proposed state-of-the-art background modeling methods. This work is helpful for both researchers and engineering practitioners. Codes of background modeling methods evaluated in this paper are available atwww.yongxu.org/lunwen.html.

On the upper bounds of (1,0)-super solutions for the regular balanced random (k,2s)-SAT problem

This paper explores the conditions which make a regular balancedrandom(k,2s)-CNFformula(1,O)-unsatisfiable with high probability.The conditions also make a random instance of the regular balanced(k-1,2(k-1)s)-SAT problem unsatisfiable with high probability,where the instance obeys a distribution which differs from the distribution obeyed by a regular balanced random(k-1,2(k-1)s)-CNF formula.Let F be a regular balanced random(k,2s)-CNF formula where k≥3,then there exists a number so such that F is(1,O)-unsatisfiable with high probability if s>so.A numerical solution of the number so when k e(5,6,...,14)is given to conduct simulated experiments.The simulated experiments verify the theoretical result.Besides,the experiments also suggest that F is(1,O)-satisfiable with high probability if s is less than a certain value.

Exact satisfiability and phase transition analysis of the regular(k,d)-CNF formula

1Introduction The satisfiability(SAT)problem has been considered the"seed"of other NP-complete problems.The regular partial exact(k,d)-SAT problem is an important extension of the SAT problem.For any(k,d)-CNF formula with a variable set V,V'is a proper subset of V,the problem involves determining whether a truth assignment set on V'exists such that only a literal in each clause is true.When V'=V,it is a regular exact(k,d)-SAT problem.Currently,both experimental verifications and theoretical analyses of k-SAT problem have shown that the ratioα(clause constraint density)of the number of clauses m to the number of variables n is an important parameter affecting the satisfiability of the formula[1].However,the regular(k,d)-SAT problem has the same clause constraint density d/k.

一种求解双目标最小生成树的警示传播算法

双目标最小生成树问题是一个NP-难问题,在光缆通信、智能控制等领域有其重要的应用价值.警示传播(warning propagation,WP)算法是一种基于因子图的消息传递算法,可用于求解组合优化问题.借助于Boltzmann机模型使一个无向图转换为因子图,将求解无向图上的双目标最小生成树问题映射为求解因子图上的对应问题,进而设计一种求解双目标最小生成树问题的警示传播算法.选取由随机数种子产生的若干随机数构造邻接矩阵,生成对应的无向图实例,数值实验结果表明,该算法优于同类算法.

Properties of the satisfiability threshold of the strictly d-regular random(3,2s)-SAT problem

A k-CNF(conjunctive normal form)formula is a regular(k,s)-CNF one if every variable occurs s times in the formula,where k≥2 and s>0 are integers.Regular(3,s)-CNF formulas have some good structural properties,so carry-ing out a probability analysis of the structure for random formulas of this type is easier than conducting such an analysisfor random 3-CNF formulas.Some subclasses of the regular(3,s)-CNF formula have also characteristics of intractabilitythat differ from random 3-CNF formulas.For this purpose,we propose strictly d-regular(k,2s)-CNF formula,which is aregular(k,2s)-CNF formula for which d≥0 is an even num-ber and each literal occurs s-d/2 or s+d/2 times(the literals from a variable x are x and-x,where x is positive and-x isnegative).In this paper,we present a new model to generatestrictly d-regular random(k,2s)-CNF formulas,and focuson the strictly d-regular random(3,2s)-CNF formulas.Let F be a strictly d-regular random(3,2s)-CNF formula suchthat 2s>d.We show that there exists a real number so suchthat the formula F is unsatisfiable with high probability whens>so,and present a numerical solution for the real numberso.The result is supported by simulated experiments,and isconsistent with the existing conclusion for the case of d=0.Furthermore,we have a conjecture:for a given d,the strictlyd-regular random(3,2s)-SAT problem has an SAT-UNSAT(satisfiable-unsatisfiable)phase transition.Our experimentssupport this conjecture.Finally,our experiments also showthat the parameter d is correlated with the intractability of the 3-SAT problem.Therefore,our research maybe helpful for generating random hard instances of the 3-CNF formula.

An algorithm for solving satisfiability problem based on the structural information of formulas

1 Introduction The propositional satisfiability(SAT)problem is an important and prototypical NP-hard problem in theoretical computer science[1].Many efforts have been made for designing high-performance SAT solvers.The existing practical techniques for solving SAT problems are mainly divided into two categories:complete search technique and stochastic local search technique.

Satisfiability threshold of the random regular(s,c,k)-SAT problem

1Introduction The satisfiability(SAT)problem is always a core problem in the field of computer science.Its theoretical and applied research have long been the common attention of many scholars in the field of artificial intelligence and mathematical logic.In the real world,all issues related to combinatorial optimization and coordination verification are closely related to SAT problem.