一种基于搜索路径识别的CDCL命题逻辑求解器延迟重启算法

适当的重启有助于求解器跳出局部最优,但频繁重启会严重降低效率。为解决CDCL求解器重启触发条件随意性大的问题,提出一种基于搜索路径识别的延迟重启算法。该算法使用Luby序列触发延时重启判断,将当前搜索路径和已搜索路径转换为向量空间模型,通过计算向量空间相似度来判断当前搜索过程是否会进入重复搜索空间。若向量空间相似度达到设定阈值,则触发重启,否则延迟重启。采用SAT国际竞赛的实例,与两个主流的求解器进行了对比实验。结果表明,所提算法能够有效规避重复搜索空间问题,并显著提高求解效率。     

基于动态奖惩的CDCL SAT求解器分支启发式算法

分支启发式算法在CDCL SAT求解器中有着非常重要的作用,传统的分支启发式算法在计算变量活性得分时只考虑了冲突次数而并未考虑决策层和冲突决策层所带来的影响。为了提高SAT问题的求解效率,受EVSIDS和ACIDS的启发,提出了基于动态奖惩DRPB的分支启发式算法。每当冲突发生时,DRPB通过综合考虑冲突次数、决策层、冲突决策层和变量冲突频率来更新变量活性得分。用DRPB替代VSIDS算法改进了Glucose 3.0,并测试了SATLIB基准库、2015年和2016年SAT竞赛中的实例。实验结果表明,与传统、单一的奖励变量分支策略相比,所提分支策略可以通过减少搜索树的分支和布尔约束传播次数来减小搜索树的规模并提高SAT求解器的性能。     

利用近似解加速求解SAT问题的启发式完全算法

结合DPLL完全算法能够证明可满足性(SAT)问题的不可满足性和局部搜索算法快速的优点,提出利用近似解加速求解SAT问题的启发式完全算法.首先利用局部搜索算法快速地得到一个近似解,并将该近似解作为完全算法的初始输入,用于其中分支变量的相位决策.该算法引导完全算法优先搜索近似解所在的子空间,加速解决器找到可满足解的过程,为SAT问题的求解提供了一种新的有效途径.实验结果表明,该算法有效地提高了决策的精度和SAT解决器的效率,对很多实例非常有效.     

基于SystemC的SAT求解器设计

该文描述了可满足性问题(SAT)求解器的设计及性能。首先,基于DPLL算法设计了一个单核SAT求解器的SystemC模型。校准这个模型,使之与工作站级计算机的软件性能相匹配,结果发现通过不连续内存访问数可以准确地估计运行时间。接着,设计了一个多核SAT求解器模型,使之能共享学习短句。通过广泛地仿真,演示了这个方法的并行效率。针对DPLL算法并行化水平低时的性能退化问题,进行了算法改进,结果得到了明显的改善。     

基于回跳层数的SAT求解器学习子句删除策略

目前学习子句删除策略广泛采用的是基于LBD的评估方式,LBD评估方式在每次执行删除时都会删除前一半LBD值大的学习子句,这种方式对LBD值大的学习子句的删除过于激进。针对此问题,提出了一种利用冲突回跳层数（back-jump levels）的评估方式来保留LBD值较大的相关学习子句。以CDCL（conflict driven clause learning）完备算法为框架,在子句删除环节形成了BJL删除算法。通过测试2017年SAT国际竞赛例,对新改进的版本与原版求解器进行了对比实验。实验表明,所提策略可显著提高求解器的求解性能和求解效率。     

基于改进K 支配排序的高维多目标进化算法

为提高4目标以上高维多目标优化问题的求解性能,提出一种基于改进K支配排序的高维多目标进化算法(KS-MODE).该算法针对K支配的支配关系和排序方法进行改进,避免循环支配并增强选择压力;设计新的全局密度估计方法提高局部密度估计精确性;设计新的精英选择策略和适应度值评价函数;采用CAO局部搜索算子加速收敛.在4～30个目标标准测试函数上的实验结果表明,KS-MODE能够在保证解集分布性的同时大幅提升收敛性和稳定性,能够有效求解高维多目标优化问题.     

基于DPLL的混合遗传算法求解SAT问题

基于"聚类排序选择"优化遗传算法求解SAT问题时,引入交叉算子和变异算子,并根据适应度函数及问题本身特性,调节阈值δ,生成新的种群聚类。这种遗传算法有效地抑制了算法的延迟收敛,从而保证了为可满足性公式能够快速找到一个可满足性指派。同时,在遗传算法中引入了DPLL算法,对部分变元进行消解,提高了算法的求解效率。相关的实验数据表明,本算法的性能明显优于同类算法。     

基于全局排序的高维多目标优化研究

目标数超过4的高维多目标优化是目前进化多目标优化领域求解难度最大的问题之一,现有的多目标进化算法求解该类问题时,存在收敛性和解集分布性上的缺陷,难以满足实际工程优化需求.提出一种基于全局排序的高维多目标进化算法GR-MODE,首先,采用一种新的全局排序策略增强选择压力,无需用户偏好及目标主次信息,且避免宽松Pareto支配在排序结果合理性与可信性上的损失;其次,采用Harmonic平均拥挤距离对个体进行全局密度估计,提高现有局部密度估计方法的精确性;最后,针对高维多目标复杂空间搜索需求,设计新的精英选择策略及适应度值评价函数.将该算法与国内外现有的5种高性能多目标进化算法在标准测试函数集DTLZ{1,2, 4,5}上进行对比实验,结果表明,该算法具有明显的性能优势,大幅提升了4~30维高维多目标优化的收敛性和分布性.     

采用放松支配关系的高维多目标微分进化算法

为了提高进化算法在求解高维多目标优化问题时的收敛性和多样性,提出了采用放松支配关系的高维多目标微分进化算法。该算法采用放松的Pareto支配关系,以增加个体的选择压力;采用群体和外部存储器协同进化的方案,并通过混合微分变异算子,生成子代群体;采用基于指标的方法计算个体的适应度并对群体进行更新;采用基于Lp范数（0相似文献   

基于新的适应度函数和多搜索策略的高维多目标进化算法

为提高高维多目标进化算法的性能,提出了一个基于新的适应度函数和多搜索策略的高维多目标进化算法。该算法提出了一个新的适应度函数来平衡多样性和收敛性,并且设计了一个多搜索策略来帮助交叉算子产生优秀的后代进而提高收敛性。该适应度函数首先从当前种群和新产生的后代中挑出收敛性较好的个体,然后计算这些个体的稀疏程度;该多搜索策略选择稀疏且收敛的解来执行全局和局部搜索。数值实验测试了CEC2018高维多目标竞赛的15个测试问题,每个测试问题的目标个数分别为5、10、15。实验结果表明,该算法能找到一组比四种代表性算法（如NSGAIII、MOEA/DD、KnEA、RVEA）具有更好的多样性和收敛性的解集。     

A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers

Because of the inherent NP-completeness of SAT, many SAT problems currently cannot be solved in a reasonable time. Usually, in order to tackle a new class of SAT problems, new ad hoc algorithms must be designed. Another way to solve a new problem is to use a generic solver and employ parallelism to reduce the solve time. In this paper we propose a parallelization scheme for a class of SAT solvers based on the DPLL procedure. The scheme uses a dynamic load-balancing mechanism based on work-stealing techniques to deal with the irregularity of SAT problems. We parallelize Satz, one of the best generic SAT solvers, with our scheme to obtain a parallel solver called PSatz. The first experimental results on random 3-SAT problems and a set of well-known structured problems show the efficiency of PSatz. PSatz is freely available and runs on any networked workstations under Unix/Linux.     

Solving SAT problem by heuristic polarity decision-making algorithm

This paper presents a heuristic polarity decision-making algorithm for solving Boolean satisfiability (SAT). The algorithm inherits many features of the current state-of-the-art SAT solvers, such as fast BCP, clause recording, restarts, etc. In addition, a preconditioning step that calculates the polarities of variables according to the cover distribution of Karnaugh map is introduced into DPLL procedure, which greatly reduces the number of conflicts in the search process. The proposed approach is implemented as a SAT solver named DiffSat. Experiments show that DiffSat can solve many "real-life" instances in a reasonable time while the best existing SAT solvers, such as Zchaff and MiniSat, cannot. In particular, DiffSat can solve every instance of Bart benchmark suite in less than 0.03 s while Zchaff and MiniSat fail under a 900 s time limit. Furthermore, DiffSat even outperforms the outstanding incomplete algorithm DLM in some instances.     

基于社交信任和标签偏好的景点推荐方法

针对现有的景点推荐算法在处理用户关系时忽视了用户隐性信任和信任传递问题,以及当用户处于新城市时由于缺乏用户历史记录无法做出准确推荐的情况,本文提出一种综合用户信任关系和标签偏好的个性化景点推荐方法.在仅仅考虑用户相似度时推荐质量差的情况下引入信任度,通过挖掘用户隐性信任关系解决了现有研究在直接信任难以获取时无法做出推荐的情况,有效缓解了数据稀疏性和冷启动问题.同时在用户兴趣分析过程中将景点和标签的关系扩展到了用户、景点和标签三者的相互关系,把用户的兴趣偏好分解成对不同景点标签的长期偏好,有效地缓解了缺乏用户历史游览记录时推荐质量不佳的问题.通过在Flickr网站上收集的数据进行实验验证,结果表明本文提出的混合推荐算法有效地提高了推荐精度,在一定程度上缓解了冷启动和新城市问题.     

Limitations of restricted branching in clause learning

The techniques for making decisions, that is, branching, play a central role in complete methods for solving structured instances of constraint satisfaction problems (CSPs). In this work we consider branching heuristics in the context of propositional satisfiability (SAT), where CSPs are expressed as propositional formulas. In practice, there are cases when SAT solvers based on the Davis-Putnam-Logemann-Loveland procedure (DPLL) benefit from limiting the set of variables the solver is allowed to branch on to so called input variables which provide a strong unit propagation backdoor set to any SAT instance. Theoretically, however, restricting branching to input variables implies a super-polynomial increase in the length of the optimal proofs for DPLL (without clause learning), and thus input-restricted DPLL cannot polynomially simulate DPLL. In this paper we settle the case of DPLL with clause learning. Surprisingly, even with unlimited restarts, input-restricted clause learning DPLL cannot simulate DPLL (even without clause learning). The opposite also holds, and hence DPLL and input-restricted clause learning DPLL are polynomially incomparable. Additionally, we analyze the effect of input-restricted branching on clause learning solvers in practice with various structured real-world benchmarks. This is an extended version of a paper [27] presented at the 13th International Conference on Principles and Practice of Constraint Programming (CP 2007) in Providence, RI, USA. The first author gratefully acknowledges financial support from Helsinki Graduate School in Computer Science and Engineering, Academy of Finland (grants #211025 and #122399), Emil Aaltonen Foundation, Jenny and Antti Wihuri Foundation, Finnish Foundation for Technology Promotion TES, and Nokia Foundation. The second author gratefully acknowledges the financial support from Academy of Finland (grant #112016).     

SMELS: Satisfiability Modulo Equality with Lazy Superposition

We consider the problem of checking satisfiability of quantified formulae in First Order Logic with Equality. We propose a new procedure for combining SAT solvers with Superposition Theorem Provers to handle quantified formulae in an efficient and complete way. In our procedure, the input formula is converted into CNF as in traditional first order logic theorem provers. The ground clauses are given to the SAT solver, which runs a DPLL method to build partial models. The partial model is reduced, and then passed to a Superposition procedure, along with justifications of literals. The Superposition procedure then performs an inference rule, which we call Justified Superposition, between the ground literals and the nonground clauses, plus usual Superposition rules with the nonground clauses. Any resulting ground clauses are provided to the DPLL engine. We prove the completeness of our procedure, using a nontrivial modification of the Bachmair and Ganzinger’s model generation technique. We have implemented a theorem prover based on this idea by reusing state-of-the-art SAT solver and Superposition Theorem Prover. Our theorem prover inherits the best of both worlds: a SAT solver to handle ground clauses efficiently, and a Superposition theorem prover which uses powerful orderings to handle the nonground clauses. Experimental results are promising, and hereby confirm the viability of our method.     

Distributed SAT

We present DPLL ABT, a distributed Satisfiability solver (SAT) (Ansótegui and Manyà in IberoAm J Artif Intell 7(20):43–56, 2003) designed to solve distributed SAT problem instances. Since SAT is a particular case of constraint satisfaction, we propose a solving method based on the Asynchronous Backtracking algorithm (ABT) (Yokoo et al. in IEEE Trans Knowl Data Eng 10(5):673–685, 1998) developed for distributed constraint reasoning. In addition, we have applied the Davis-Putnam procedure (DPLL) in every agent, plus the minimum conflict heuristic in case DPLL does not detect any inconsistency. The resulting algorithm improves the performance in terms of communication cost and computational effort versus the basic ABT. The SAT instance is distributed into agents, which cooperate to solve SAT instances just sharing the minimum information. We also present the experimental results that demonstrate the performance of the method in terms of communication and execution time comparing the performance with the basic ABT algorithm.     

Exploiting multivalued knowledge in variable selection heuristics for SAT solvers

We show that we can design and implement extremely efficient variable selection heuristics for SAT solvers by identifying, in Boolean clause databases, sets of Boolean variables that model the same multivalued variable and then exploiting that structural information. In particular, we define novel variable selection heuristics for two of the most competitive existing SAT solvers: Chaff, a solver based on look-back techniques, and Satz, a solver based on look-ahead techniques. Our heuristics give priority to Boolean variables that belong to sets of variables that model multivalued variables with minimum domain size in a given state of the search process. The empirical investigation conducted to evaluate the new heuristics provides experimental evidence that identifying multivalued knowledge in Boolean clause databases and using variable selection heuristics that exploit that knowledge leads to large performance improvements.      

A Verified SAT Solver Framework with Learn,Forget, Restart,and Incrementality

We developed a formal framework for conflict-driven clause learning (CDCL) using the Isabelle/HOL proof assistant. Through a chain of refinements, an abstract CDCL calculus is connected first to a more concrete calculus, then to a SAT solver expressed in a functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis–Putnam–Logemann–Loveland (DPLL) calculus. The imperative program relies on the two-watched-literal data structure and other optimizations found in modern solvers. We used Isabelle’s Refinement Framework to automate the most tedious refinement steps. The most noteworthy aspects of our work are the inclusion of rules for forget, restart, and incremental solving and the application of stepwise refinement.     

结合用户兴趣度聚类的协同过滤推荐算法

针对传统的协同过滤算法忽略了用户兴趣源于关键词以及数据稀疏的问题,提出了结合用户兴趣度聚类的协同过滤推荐算法。利用用户对项目的评分,并从项目属性中提取关键词,提出了一种新的RF-IIF （rating frequency-inverse item frequency）算法,根据目标用户对某关键词的评分频率和该关键词被所有用户的评分频率,得到用户对关键词的偏好,形成用户—关键词偏好矩阵,并在该矩阵基础上进行聚类。然后利用logistic函数得到用户对项目的兴趣度,明确用户爱好,在类簇中寻找目标用户的相似用户,提取邻居爱好的前◢N◣个物品对用户进行推荐。实验结果表明,算法准确率始终优于传统算法,对用户爱好判断较为准确,缓解了数据稀疏问题,有效提高了推荐的准确率和效率。