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.展开更多
DNA computation （DNAC） has been proposed to solve the satisfiability （SAT） problem due to operations in parallel on extremely large numbers of strands. This paper attempts to treat the DNA-based bio-molecular solu...DNA computation （DNAC） has been proposed to solve the satisfiability （SAT） problem due to operations in parallel on extremely large numbers of strands. This paper attempts to treat the DNA-based bio-molecular solution for the SAT problem from the quantum mechanical perspective with a purpose to explore the relationship between DNAC and quantum computation （QC）. To achieve this goal, it first builds up the correspondence of operations between QC and DNAC. Then it gives an example for the case of two variables and three clauses for details of this theory. It also demonstrates a three-qubit experiment for solving the simplest SAT problem with a single variable on a liquid-state nuclear magnetic resonance ensemble to verify this theory. Some discussions are made for the potential application and for further exploration of the present work.展开更多
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.展开更多
The random K-satisfiability （K-SAT） problem is very diffcult when the clause density is close to the satisfiability threshold. In this paper we study this problem from the perspective of solution space coupling. We ...The random K-satisfiability （K-SAT） problem is very diffcult when the clause density is close to the satisfiability threshold. In this paper we study this problem from the perspective of solution space coupling. We divide a given difficult random K-SAT formula into two easy sub-formulas and let the two corresponding solution spaces to interact with each other through a coupling field x. We investigate the statistical mechanical property of this coupled system by mean field theory and computer simulations. The coupled system has an ergodicity-breaking （clustering） transition at certain critical value Xd of the coupling field. At this transition point, the mean overlap value between the solutions of the two solution spaces is very close to 1. The mean energy density of the coupled system at its clustering transition point is less than the mean energy density of the original K-SAT problem at the temperature-induced clustering transition point. The implications of this work for designing new heuristic K-SAT solvers are discussed.展开更多
波动方程系数矩阵对称化是整合不同类别波动方程、降低波传播模拟难度的有效方法,目前已成功应用于声波方程、各向同性与各向异性介质弹性波动方程。该研究将推导出双项介质波动方程的系数矩阵对称式;随后,引入多轴完全匹配层,采用迎风...波动方程系数矩阵对称化是整合不同类别波动方程、降低波传播模拟难度的有效方法,目前已成功应用于声波方程、各向同性与各向异性介质弹性波动方程。该研究将推导出双项介质波动方程的系数矩阵对称式;随后,引入多轴完全匹配层,采用迎风格式分部求和-一致逼近项(summation by parts-simultaneous approximation terms,SBP-SAT)有限差分方法离散波动方程,并通过能量法进行稳定性评估。通过数值仿真,表明所提出的离散框架具有整合度高,稳定性好和拓展性强等特点。此外,该方法可以稳定模拟曲线域中的波传播并降低其实现成本,表明了波动方程系数矩阵对称化方法及其离散框架在波传播模拟领域具有广泛的应用前景。展开更多
The efficient implementation of the Advanced Encryption Standard(AES)is crucial for network data security.This paper presents novel hardware implementations of the AES S-box,a core component,using tower field represen...The efficient implementation of the Advanced Encryption Standard(AES)is crucial for network data security.This paper presents novel hardware implementations of the AES S-box,a core component,using tower field representations and Boolean Satisfiability(SAT)solvers.Our research makes several significant contri-butions to the field.Firstly,we have optimized the GF(24)inversion,achieving a remarkable 31.35%area reduction(15.33 GE)compared to the best known implementations.Secondly,we have enhanced multiplication implementa-tions for transformation matrices using a SAT-method based on local solutions.This approach has yielded notable improvements,such as a 22.22%reduction in area(42.00 GE)for the top transformation matrix in GF((24)2)-type S-box implementation.Furthermore,we have proposed new implementations of GF(((22)2)2)-type and GF((24)2)-type S-boxes,with the GF(((22)2)2)-type demonstrating superior performance.This implementation offers two variants:a small area variant that sets new area records,and a fast variant that establishes new benchmarks in Area-Execution-Time(AET)and energy consumption.Our approach significantly improves upon existing S-box implementations,offering advancements in area,speed,and energy consumption.These optimizations contribute to more efficient and secure AES implementations,potentially enhancing various cryptographic applications in the field of network security.展开更多
基金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.
基金Project supported by the National Natural Science Foundation of China (Grant Nos 10774163 and 10574143)the National Basic Research Program of China (Grant No 2006CB921203)
文摘DNA computation （DNAC） has been proposed to solve the satisfiability （SAT） problem due to operations in parallel on extremely large numbers of strands. This paper attempts to treat the DNA-based bio-molecular solution for the SAT problem from the quantum mechanical perspective with a purpose to explore the relationship between DNAC and quantum computation （QC）. To achieve this goal, it first builds up the correspondence of operations between QC and DNAC. Then it gives an example for the case of two variables and three clauses for details of this theory. It also demonstrates a three-qubit experiment for solving the simplest SAT problem with a single variable on a liquid-state nuclear magnetic resonance ensemble to verify this theory. Some discussions are made for the potential application and for further exploration of the present work.
文摘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 by the Knowledge Innovation Program of Chinese Academy of Sciences under Grant No.KJCX2-EW-J02the Natural National Science Foundation of China under Grant Nos.11121403 and 11225526
文摘The random K-satisfiability （K-SAT） problem is very diffcult when the clause density is close to the satisfiability threshold. In this paper we study this problem from the perspective of solution space coupling. We divide a given difficult random K-SAT formula into two easy sub-formulas and let the two corresponding solution spaces to interact with each other through a coupling field x. We investigate the statistical mechanical property of this coupled system by mean field theory and computer simulations. The coupled system has an ergodicity-breaking （clustering） transition at certain critical value Xd of the coupling field. At this transition point, the mean overlap value between the solutions of the two solution spaces is very close to 1. The mean energy density of the coupled system at its clustering transition point is less than the mean energy density of the original K-SAT problem at the temperature-induced clustering transition point. The implications of this work for designing new heuristic K-SAT solvers are discussed.
文摘波动方程系数矩阵对称化是整合不同类别波动方程、降低波传播模拟难度的有效方法,目前已成功应用于声波方程、各向同性与各向异性介质弹性波动方程。该研究将推导出双项介质波动方程的系数矩阵对称式;随后,引入多轴完全匹配层,采用迎风格式分部求和-一致逼近项(summation by parts-simultaneous approximation terms,SBP-SAT)有限差分方法离散波动方程,并通过能量法进行稳定性评估。通过数值仿真,表明所提出的离散框架具有整合度高,稳定性好和拓展性强等特点。此外,该方法可以稳定模拟曲线域中的波传播并降低其实现成本,表明了波动方程系数矩阵对称化方法及其离散框架在波传播模拟领域具有广泛的应用前景。
基金supported in part by the National Natural Science Foundation of China(No.62162016)in part by the Innovation Project of Guangxi Graduate Education(Nos.YCBZ2023132 and YCSW2023304).
文摘The efficient implementation of the Advanced Encryption Standard(AES)is crucial for network data security.This paper presents novel hardware implementations of the AES S-box,a core component,using tower field representations and Boolean Satisfiability(SAT)solvers.Our research makes several significant contri-butions to the field.Firstly,we have optimized the GF(24)inversion,achieving a remarkable 31.35%area reduction(15.33 GE)compared to the best known implementations.Secondly,we have enhanced multiplication implementa-tions for transformation matrices using a SAT-method based on local solutions.This approach has yielded notable improvements,such as a 22.22%reduction in area(42.00 GE)for the top transformation matrix in GF((24)2)-type S-box implementation.Furthermore,we have proposed new implementations of GF(((22)2)2)-type and GF((24)2)-type S-boxes,with the GF(((22)2)2)-type demonstrating superior performance.This implementation offers two variants:a small area variant that sets new area records,and a fast variant that establishes new benchmarks in Area-Execution-Time(AET)and energy consumption.Our approach significantly improves upon existing S-box implementations,offering advancements in area,speed,and energy consumption.These optimizations contribute to more efficient and secure AES implementations,potentially enhancing various cryptographic applications in the field of network security.
