取定s的严格d-正则随机(3,2s)-SAT问题的可满足临界

3-CNF公式的随机难解实例生成对于揭示3-SAT问题的难解实质和设计满足性测试的有效算法有着重要意义.对于整数k>2和s>0,如果在一个k-CNF公式中每个变量正负出现次数均为s,则称该公式是严格正则（k,2s）-CNF公式.受严格正则（k,2s）-CNF公式的结构特征启发,提出每个变量正负出现次数之差的绝对值均为d的严格d-正则（k,2s）-CNF公式,并使用新提出的SDRRK2S模型生成严格d-正则随机（k,2s）-CNF公式.取定整数5<s<11,模拟实验显示,严格d-正则随机（3,2s）-SAT问题存在SAT-UNSAT相变现象和HARD-EASY相变现象.因此,立足于3-CNF公式的随机难解实例生成,研究了严格d-正则随机（3,2s）-SAT问题在s取定时的可满足临界.通过构造一个特殊随机实验和使用一阶矩方法,得到了严格d-正则随机（3,2s）-SAT问题在s取定时可满足临界值的一个下界.模拟实验结果验证了理论证明所得下界的正确性.     

RB模型实例集上置信传播算法的收敛性

置信传播算法求解RB（k,n,α,r_c,p）模型实例时非常有效,几乎能够有效求解接近可满足性相变点的难解实例.然而,因子图带有回路的实例,置信传播算法不总有效,常表现为不收敛.对于这种现象,至今缺少系统的理论解释.置信传播算法是最为基础的信息传播算法,对置信传播算法的收敛性分析是其他信息传播算法收敛性分析的重要基础.在RB（k,n,α,r_c,p）模型中,取k=2,α>（1/k）,r_c>0均为常数,且满足ke^{-（α/（r_c））}≥1.证明了如果p∈（0,n^-2α）,则置信传播算法在RB（k,n,α,r_c,p）模型产生的随机实例集上高概率收敛.最后,在RB（k,n,α,r_c,p）模型上选取了几组不同的数据进行数值模拟,实验结果表明该结论有效.当问题规模n增大时,在RB（k,n,α,r_c,p）模型的可满足区域,实验收敛区间趋于一个固定范围,而理论收敛区间逐渐变窄.原因在于,RB（k,n,α,r_c,p）模型是一个具有增长定义域的随机CSP实例产生模型,不协调赋值的数目与参数p及问题规模n有关.     

一类可分离SAT问题的O(1.890n)精确算法

布尔可满足性问题（SAT）是指对于给定的布尔公式,是否存在一个可满足的真值指派.这是第1个被证明的NP完全问题,一般认为不存在多项式时间算法,除非P=NP.学者们大都研究了子句长度不超过k的SAT问题（k-SAT）,从全局搜索到局部搜索,给出了大量的相对有效算法,包括随机算法和确定算法.目前,最好算法的时间复杂度不超过O（（2-2/k）ⁿ）,当k=3时,最好算法时间复杂度为O（1.308ⁿ）.而对于更一般的与子句长度k无关的SAT问题,很少有文献涉及.引入了一类可分离SAT问题,即3-正则可分离可满足性问题（3-RSSAT）,证明了3-RSSAT是NP完全问题,给出了一般SAT问题3-正则可分离性的O（1.890ⁿ）判定算法.然后,利用矩阵相乘算法的研究成果,给出了3-RSSAT问题的O（1.890ⁿ）精确算法,该算法与子句长度无关.     

2-3-SAT问题相变现象剖析及其应用

3-SAT问题有一个非常奇妙的相变现象.对于固定的变量数N，合取范式的可满足概率随着子句个数K的变化而发生剧烈的变化;当K≈4.3*N 时,可满足概率急剧地从1变为0.相变现象决定了问题的难易分布,对于快速求解算法的设计有着非常重要的意义.文章着重讨论了SAT问题的更一般形式，即2-3-SAT问题的相变现象.研究了相变点处的2-子句和3-子句个数的关系，发现了2-子句和3-子句在约束能力意义下的当量关系，并提出了如何有效地利用2-3-SAT的相变现象.     

k-Median近似计算复杂度与局部搜索近似算法分析

k-Median问题的近似算法研究一直是计算机科学工作者关注的焦点,现有研究结果大多是关于欧式空间和Metric空间的,一般距离空间k-Median的结果多年来一直未见.考虑一般距离空间k-Median问题,设d_max/d_min表示k-Median实例中与客户点邻接的最长边长比最短边长的最大者.首先证明d_max/d_min≤ω+ε的k-Median问题不存在近似度小于1+ω-1/e的多项式时间近似算法,除非,由此推出Metric k-Median问题不可近似到1+2/e,除非NP(∈)DTME(N^{O(log logn)}).然后给出k-Median问题的一个局部搜索算法,分析表明,若有d_max/d_min≤ω,则算法的近似度为1+ω-1/2.该结果亦适用于Metric k-Median,ω≤5时,局部搜索算法求解Metric k-Median的近似度为3,好于现有结果3+2/P.通过计算机实验,进一步研究了k-Median局部搜索求解算法的实际计算效果和该算法的改进方法.     

k-LSAT (k≥3)是NP-完全的

合取范式(conjunctive normal form,简称CNF)公式F是线性公式,如果F中任意两个不同子句至多有一个公共变元.如果F中的任意两个不同子句恰好含有一个公共变元,则称F是严格线性的.所有的严格线性公式均是可满足的,而对于线性公式类LCNF,对应的判定问题LSAT仍然是NP-完全的.LCNF_≥k是子句长度大于或等于k的CNF公式子类,判定问题LSA(≥k)的NP-完全性与LCNF(≥k)中是否含有不可满足公式密切相关.即LSAT_≥k的NP-完全性取决于LCNF_≥k是否含有不可满足公式.S.Porschen等人用超图和拉丁方的方法构造了LCNF_≥3和LCNF_≥4中的不可满足公式,并提出公开问题:对于k≥5,LCNF_≥k是否含有不可满足公式?将极小不可满足公式应用于公式的归约,引入了一个简单的一般构造方法.证明了对于k≥3,k-LCNF含有不可满足公式,从而证明了一个更强的结果:对于k≥3,k-LSAT是NP-完全的.     

Goguen命题逻辑系统公理化扩张的Γ-k真度理论及性质

本文首先对n值Goguen命题逻辑进行公理化扩张,Goguen_~,△,记为Π_~,△.利用公式的诱导函数给出公式在k（k任取~或△）连接词下相对于局部有限理论Γ的Γ-k真度的定义;讨论了Π_~,△中Γ-k真度的MP规则、HS规则等相关性质;最后,在Π_~,△中定义了两公式间的Γ-k相似度与Γ-k伪距离,得到了公式在连接词下相对于局部有限理论Γ的Γ-k相似度与Γ-k伪距离所具有的一些良好性质.     

面向移动对象连续k近邻查询的双层索引结构

移动对象连续k近邻（CKNN）查询是指给定一个连续移动的对象集合,对于任意一个k近邻查询q,实时计算查询q的k近邻并在查询有效时间内对查询结果进行实时更新.现实生活中,交通出行、社交网络、电子商务等领域许多基于位置的应用服务都涉及移动对象连续k近邻查询这一基础问题.已有研究工作解决连续k近邻查询问题时,大多需要通过多次迭代确定一个包含k近邻的查询范围,而每次迭代需要根据移动对象的位置计算当前查询范围内移动对象的数量,整个迭代过程的计算代价占查询代价的很大部分.为此,提出了一种基于网络索引和混合高斯函数移动对象分布密度的双重索引结构（grid GMM index,GGI）,并设计了移动对象连续k近邻增量查询算法（incremental search for continuous k nearest neighbors,IS-CKNN）.GGI索引结构的底层采用网格索引对海量移动对象进行维护,上层构建混合高斯模型模拟移动对象在二维空间中的分布.对于给定的k近邻查询q,IS-CKNN算法能够基于混合高斯模型直接确定一个包含q的k近邻的查询区域,减少了已有算法求解该区域的多次迭代过程;当移动对象和查询q位置发生变化时,进一步提出一种高效的增量查询策略,能够最大限度地利用已有查询结果减少当前查询的计算量.最后,在滴滴成都网约车数据集以及两个模拟数据集上进行大量实验,充分验证了算法的性能.     

改进k值自动获取VDBSCAN聚类算法

针对DBSCAN聚类算法不能对变密度分布数据集进行有效聚类,VDBSCAN算法借助k-dist图来自动获取各个密度层次的数据对象的邻域半径,解决了具有不同密度层次分布数据集的聚类问题. k-VDBSCAN算法通过对k值的自动获取,减小了VDBSCAN中参数k对最终聚类结果的影响. 针对k值的自动获取,在原有的k-VDBSCAN聚类算法基础上,依据数据集本身,利用数据对象间距离的特征,提出了一种k值改进自动获取聚类算法. 理论分析与实验结果表明,新的改进算法能够有效的自动获得参数k的值,并且在聚类结果、时间效率方面都有明显的提高.     

用户群体满意度最大化的Top-k在线服务评价

考虑用户评价准则不一致的在线服务评价通常以服务的完整排序作为评价结果,而不是选择出使用户群体满意度最大的Top-k在线服务集合,使评价结果难以满足Top-k在线服务评价场景的合理性和公平性需求.为此,提出了一种用户群体满意度最大化的Top-k在线服务评价方法.该方法首先定义用户群体满意度指标,以衡量选择的k个在线服务的合理性;其次,考虑用户评价准则不一致及用户偏好信息不完整的情况,采用Borda规则将用户对在线服务的偏好关系构造为用户-服务满意度矩阵;然后借鉴Monroe比例代表思想,将Top-k在线服务评价问题建模为寻找最大化用户群体满意度的在线服务集合的优化问题;最后采用贪心算法对该优化问题进行求解,将得到的在线服务集合作为Top-k评价结果.通过理论分析和实验验证了该方法的合理性和有效性.理论分析表明,该方法满足Top-k在线服务评价所需的比例代表性和公平性.同时,实验结果也表明,该方法能够在合理的时间内获得接近用户群体满意度理想上界的评价结果,可以有效地辅助用户群体做出正确的服务选择决策.另外,该方法还可以在用户偏好不完整的情况下实现Top-k在线服务评价.     

d-正则(k,s)-SAT问题的NP完全性

研究具有正则结构的SAT问题是否是NP完全问题,具有重要的理论价值.(k,s)-CNF公式类和正则(k,s)-CNF公式类已被证明存在一个临界函数f(k),使得当s≤f(k)时,所有实例都可满足;当s≥f(k)+1时,对应的SAT问题是NP完全问题.研究具有更强正则约束的d-正则(k,s)-SAT问题,其要求实例中每个变元的正负出现次数之差不超过给定的自然数d.通过设计一种多项式时间的归约方法,证明d-正则(k,s)-SAT问题存在一个临界函数f(k,d),使得当s≤f(k,d)时,所有实例都可满足;当s≥f(k,d)+1时,d-正则(k,s)-SAT问题是NP完全问题.这种多项式时间的归约变换方法通过添加新的变元和新的子句,可以更改公式的子句约束密度,并约束每个变元正负出现次数的差值.这进一步说明,只用子句约束密度不足以刻画CNF公式结构的特点,对临界函数f(k,d)的研究有助于在更强正则约束条件下构造难解实例.     

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.     

Regular Random k-SAT: Properties of Balanced Formulas

We consider a model for generating random k-SAT formulas, in which each literal occurs approximately the same number of times in the formula clauses (regular random and k-SAT). Our experimental results show that such regular random k-SAT instances are much harder than the usual uniform random k-SAT problems. This is in agreement with other results that show that more balanced instances of random combinatorial problems are often much more difficult to solve than uniformly random instances, even at phase transition boundaries. There are almost no formal results known for such problem distributions. The balancing constraints add a dependency between variables that complicates a standard analysis. Regular random 3-SAT exhibits a phase transition as a function of the ratio α of clauses to variables. The transition takes place at approximately α = 3.5. We show that for α > 3.78 with high probability (w.h.p.) random regular 3-SAT formulas are unsatisfiable. Specifically, the events hold with high probability if Pr when n → ∞. We also show that the analysis of a greedy algorithm proposed by Kaporis et al. for the uniform 3-SAT model can be adapted for regular random 3-SAT. In particular, we show that for formulas with ratio α < 2.46, a greedy algorithm finds a satisfying assignment with positive probability.     

A comparative runtime analysis of heuristic algorithms for satisfiability problems

The satisfiability problem is a basic core NP-complete problem. In recent years, a lot of heuristic algorithms have been developed to solve this problem, and many experiments have evaluated and compared the performance of different heuristic algorithms. However, rigorous theoretical analysis and comparison are rare. This paper analyzes and compares the expected runtime of three basic heuristic algorithms: RandomWalk, (1+1) EA, and hybrid algorithm. The runtime analysis of these heuristic algorithms on two 2-SAT instances shows that the expected runtime of these heuristic algorithms can be exponential time or polynomial time. Furthermore, these heuristic algorithms have their own advantages and disadvantages in solving different SAT instances. It also demonstrates that the expected runtime upper bound of RandomWalk on arbitrary k-SAT (k?3) is O(n(k−1)), and presents a k-SAT instance that has Θ(n(k−1)) expected runtime bound.     

A deterministic (2−2/(k+1))n algorithm for k-SAT based on local search

Local search is widely used for solving the propositional satisfiability problem. Papadimitriou (1991) showed that randomized local search solves 2-SAT in polynomial time. Recently, Schöning (1999) proved that a close algorithm for k-SAT takes time (2−2/k)ⁿ up to a polynomial factor. This is the best known worst-case upper bound for randomized 3-SAT algorithms (cf. also recent preprint by Schuler et al.).We describe a deterministic local search algorithm for k-SAT running in time (2−2/(k+1))ⁿ up to a polynomial factor. The key point of our algorithm is the use of covering codes instead of random choice of initial assignments. Compared to other “weakly exponential” algorithms, our algorithm is technically quite simple. We also describe an improved version of local search. For 3-SAT the improved algorithm runs in time 1.481ⁿ up to a polynomial factor. Our bounds are better than all previous bounds for deterministic k-SAT algorithms.     

More efficient two-mode stochastic local search for random 3-satisfiability

Stochastic local search (SLS) is a popular paradigm in incomplete solving for the Boolean satisfiability problem (SAT). Most SLS solvers for SAT switch between two modes, i.e., the greedy (intensification) mode and the diversification mode. However, the performance of these two-mode SLS algorithms lags far behind on solving random 3-satisfiability (3-SAT) problem, which is a significant special case of the SAT problem. In this paper, we propose a new hybrid scoring function called M C based on a linear combination of a greedy property m a k e and a diversification property C o n f T i m e s, and then utilize M C to develop a new two-mode SLS solver called CCMC. To evaluate the performance of CCMC, we conduct extensive experiments to compare CCMC with five state-of-the-art two-mode SLS solvers (i.e., Sparrow2011, Sattime2011, EagleUP, gNovelty+PCL and CCASat) on a broad range of random 3-SAT instances, including all large 3-SAT ones from SAT Competition 2009 and SAT Competition 2011 as well as 200 generated satisfiable huge random 3-SAT ones. The experiments illustrate that CCMC obviously outperforms its competitors, indicating the effectiveness of CCMC. We also analyze the effectiveness of the underlying ideas in CCMC and further improve the performance of CCMC on solving random 5-SAT instances.     

A Probabilistic Algorithm for k -SAT Based on Limited Local Search and Restart

Abstract. A simple probabilistic algorithm for solving the NP-complete problem k -SAT is reconsidered. This algorithm follows a well-known local-search paradigm: randomly guess an initial assignment and then, guided by those clauses that are not satisfied, by successively choosing a random literal from such a clause and changing the corresponding truth value, try to find a satisfying assignment. Papadimitriou [11] introduced this random approach and applied it to the case of 2-SAT, obtaining an expected O(n ² ) time bound. The novelty here is to restart the algorithm after 3n unsuccessful steps of local search. The analysis shows that for any satisfiable k -CNF formula with n variables the expected number of repetitions until a satisfying assignment is found this way is (2⋅ (k-1)/ k) ⁿ . Thus, for 3-SAT the algorithm presented here has a complexity which is within a polynomial factor of (\frac 4 3 ) ⁿ . This is the fastest and also the simplest among those algorithms known up to date for 3-SAT achieving an o(2 ⁿ ) time bound. Also, the analysis is quite simple compared with other such algorithms considered before.     

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.