In this paper we present a classical parallel quantum algorithm for the satisfiability problem. We have exploited the classical parallelism of quantum algorithms developed in [G.L. Long and L. Xiao, Phys. Rev. A 69 （...In this paper we present a classical parallel quantum algorithm for the satisfiability problem. We have exploited the classical parallelism of quantum algorithms developed in [G.L. Long and L. Xiao, Phys. Rev. A 69 （2004） 052303], so that additional acceleration can be gained by using classical parallelism. The quantum algorithm first estimates the number of solutions using the quantum counting algorithm, and then by using the quantum searching algorithm, the explicit solutions are found.展开更多
As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the ...As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland(DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability(SAT) and Satisfiability Modulo Theories(SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.展开更多
The maximum satisfiability problem (MAX-SAT) refers to the task of finding a variable assignment that satisfies the maximum number of clauses (or the sum of weight of satisfied clauses) in a Boolean Formula. Most loca...The maximum satisfiability problem (MAX-SAT) refers to the task of finding a variable assignment that satisfies the maximum number of clauses (or the sum of weight of satisfied clauses) in a Boolean Formula. Most local search algorithms including tabu search rely on the 1-flip neighbourhood structure. In this work, we introduce a tabu search algorithm that makes use of the multilevel paradigm for solving MAX-SAT problems. The multilevel paradigm refers to the process of dividing large and difficult problems into smaller ones, which are hopefully much easier to solve, and then work backward towards the solution of the original problem, using a solution from a previous level as a starting solution at the next level. This process aims at looking at the search as a multilevel process operating in a coarse-to-fine strategy evolving from k-flip neighbourhood to 1-flip neighbourhood-based structure. Experimental results comparing the multilevel tabu search against its single level variant are presented.展开更多
当前基于神经网络的端到端SAT求解模型在各类SAT问题求解上展现了巨大潜力。然而SAT问题难以容忍误差存在,神经网络模型无法保证不产生预测误差。为利用SAT问题实例特性来减少模型预测误差,提出了错误偏好变量嵌入架构(architecture of ...当前基于神经网络的端到端SAT求解模型在各类SAT问题求解上展现了巨大潜力。然而SAT问题难以容忍误差存在,神经网络模型无法保证不产生预测误差。为利用SAT问题实例特性来减少模型预测误差,提出了错误偏好变量嵌入架构(architecture of embedding error-preference variables, AEEV)。该架构包含错误偏好变量嵌入调整算法和动态部分标签训练模式。首先,为利用参与越多未满足子句的变量越可能被错误分类这一特性,提出了错误偏好变量嵌入调整算法,在消息传递过程中根据变量参与的未满足子句个数来调整其嵌入。此外,提出了动态部分标签监督训练模式,该模式利用了SAT问题实例的变量赋值之间存在复杂依赖关系这一特性,避免为全部变量提供标签,仅为错误偏好变量提供一组来自真实解的标签,保持其他变量标签为预测值不变,以在训练过程管理一个更小的搜索空间。最后,在3-SAT、k-SAT、k-Coloring、3-Clique、SHA-1原像攻击以及收集的SAT竞赛数据集上进行了实验验证。结果表明,相较于目前较先进的基于神经网络的端到端求解模型QuerySAT,AEEV在包含600个变量的k-SAT数据集上准确率提升了45.81%。展开更多
在分布式环境中,垂直分割是一种保护用户隐私的有效方法。然而,当前的垂直分割策略假设参与数据存储的各个云服务提供商(cloud service provider,CSP)之间不存在共谋。针对实际场景中CSP之间可能存在的共谋问题,探讨了如何在这种情况下...在分布式环境中,垂直分割是一种保护用户隐私的有效方法。然而,当前的垂直分割策略假设参与数据存储的各个云服务提供商(cloud service provider,CSP)之间不存在共谋。针对实际场景中CSP之间可能存在的共谋问题,探讨了如何在这种情况下保护用户数据隐私。假设有n个CSP参与数据存储,其中最多k个CSP可能会共谋,给出了垂直分割的(k,n)-安全定义,并提出了MLVP(machine learning vertical partitioning)方案。该方案利用机器学习算法分析属性之间的关联性,对得到的所有关联性进行优化,并将计算垂直分割方法问题转化成可满足性问题,再利用可满足性问题求解器得到分割方法。此外,对MLVP方案的安全性进行理论分析,并在真实数据集上进行实验,比较不同机器学习算法和隐私保护强度对分割效果和性能的影响;与两个不考虑CSP存在共谋的垂直分割方案(Oriol方案和Ciriani方案)在计算速度和查询速度上进行了比较。实验结果表明:在计算速度上,因为要保证CSP共谋时的安全性,MLVP方案略慢,在查询速度上,MLVP方案相较Oriol方案和Ciriani方案分别提升了32.6%和8.8%。展开更多
For bipartite angle consensus tracking and vibration suppression of multiple Timoshenko manipulator systems with time-varying actuator faults,parameter and modeling uncertainties,and unknown disturbances,a novel distr...For bipartite angle consensus tracking and vibration suppression of multiple Timoshenko manipulator systems with time-varying actuator faults,parameter and modeling uncertainties,and unknown disturbances,a novel distributed boundary event-triggered control strategy is proposed in this work.In contrast to the earlier findings,time-varying consensus tracking and actuator defects are taken into account simultaneously.In addition,the constructed event-triggered control mechanism can achieve a more flexible design because it is not required to satisfy the input-to-state condition.To achieve the control objectives,some new integral control variables are given by using back-stepping technique and boundary control.Moreover,adaptive neural networks are applied to estimate system uncertainties.With the proposed event-triggered scheme,control inputs can reduce unnecessary updates.Besides,tracking errors and vibration states of the closed-looped network can be exponentially convergent into some small fields,and Zeno behaviors can be excluded.At last,some simulation examples are given to state the effectiveness of the control algorithms.展开更多
Dear Editor,This letter studies finite-time input-to-state stability(FTISS)for impulsive switched systems.A set of Lyapunov-based conditions are established for guaranteeing FTISS property.When constituent modes gover...Dear Editor,This letter studies finite-time input-to-state stability(FTISS)for impulsive switched systems.A set of Lyapunov-based conditions are established for guaranteeing FTISS property.When constituent modes governing continuous dynamics are FTISS and discrete dynamics involving impulses are destabilizing,the FTISS can be retained if impulsive-switching signals satisfy an average dwell-time(ADT)condition.展开更多
基金supported by 973 Program under Grant No.2006CB921106National Natural Science Foundation of China under Grant No.60635040the Key Grant Project of the Ministry of Education under Grant No.306020
文摘In this paper we present a classical parallel quantum algorithm for the satisfiability problem. We have exploited the classical parallelism of quantum algorithms developed in [G.L. Long and L. Xiao, Phys. Rev. A 69 （2004） 052303], so that additional acceleration can be gained by using classical parallelism. The quantum algorithm first estimates the number of solutions using the quantum counting algorithm, and then by using the quantum searching algorithm, the explicit solutions are found.
基金Supported by the National Natural Science Foundation of China(Nos.61063002,61100186,61262008)Guangxi Natural Science Foundation of China(2011GXNSFA018164,2011GXNSFA018166,2012GXNSFAA053220)the Key Project of Education Department of Guangxi
文摘As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland(DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability(SAT) and Satisfiability Modulo Theories(SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.
文摘The maximum satisfiability problem (MAX-SAT) refers to the task of finding a variable assignment that satisfies the maximum number of clauses (or the sum of weight of satisfied clauses) in a Boolean Formula. Most local search algorithms including tabu search rely on the 1-flip neighbourhood structure. In this work, we introduce a tabu search algorithm that makes use of the multilevel paradigm for solving MAX-SAT problems. The multilevel paradigm refers to the process of dividing large and difficult problems into smaller ones, which are hopefully much easier to solve, and then work backward towards the solution of the original problem, using a solution from a previous level as a starting solution at the next level. This process aims at looking at the search as a multilevel process operating in a coarse-to-fine strategy evolving from k-flip neighbourhood to 1-flip neighbourhood-based structure. Experimental results comparing the multilevel tabu search against its single level variant are presented.
基金supported in part by the National Key R&D Program of China(2021YFB3202200)the Natural Science Foundation of China(62203141)the Guangdong Basic and Applied Basic Research Foundation(2021B1515120017)。
文摘For bipartite angle consensus tracking and vibration suppression of multiple Timoshenko manipulator systems with time-varying actuator faults,parameter and modeling uncertainties,and unknown disturbances,a novel distributed boundary event-triggered control strategy is proposed in this work.In contrast to the earlier findings,time-varying consensus tracking and actuator defects are taken into account simultaneously.In addition,the constructed event-triggered control mechanism can achieve a more flexible design because it is not required to satisfy the input-to-state condition.To achieve the control objectives,some new integral control variables are given by using back-stepping technique and boundary control.Moreover,adaptive neural networks are applied to estimate system uncertainties.With the proposed event-triggered scheme,control inputs can reduce unnecessary updates.Besides,tracking errors and vibration states of the closed-looped network can be exponentially convergent into some small fields,and Zeno behaviors can be excluded.At last,some simulation examples are given to state the effectiveness of the control algorithms.
基金the National Natural Science Foundation of China(61833005)。
文摘Dear Editor,This letter studies finite-time input-to-state stability(FTISS)for impulsive switched systems.A set of Lyapunov-based conditions are established for guaranteeing FTISS property.When constituent modes governing continuous dynamics are FTISS and discrete dynamics involving impulses are destabilizing,the FTISS can be retained if impulsive-switching signals satisfy an average dwell-time(ADT)condition.
