We present a quantum adiabatic algorithm for a set of quantum 2-satisfiability(Q2SAT)problem,which is a generalization of 2-satisfiability(2SAT)problem.For a Q2SAT problem,we construct the Hamiltonian which is similar...We present a quantum adiabatic algorithm for a set of quantum 2-satisfiability(Q2SAT)problem,which is a generalization of 2-satisfiability(2SAT)problem.For a Q2SAT problem,we construct the Hamiltonian which is similar to that of a Heisenberg chain.All the solutions of the given Q2SAT problem span the subspace of the degenerate ground states.The Hamiltonian is adiabatically evolved so that the system stays in the degenerate subspace.Our numerical results suggest that the time complexity of our algorithm is O(n^(3.9))for yielding non-trivial solutions for problems with the number of clauses m=dn(n-1)/2(d■0.1).We discuss the advantages of our algorithm over the known quantum and classical algorithms.展开更多
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...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.展开更多
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.展开更多
Maximum satisfiability (MAX SAT) problem is an optimization version of the satisfiability (SAT) problem. This problem arises in certain applications in expert systems and knowledge base revision. MAX SAT problem is NP...Maximum satisfiability (MAX SAT) problem is an optimization version of the satisfiability (SAT) problem. This problem arises in certain applications in expert systems and knowledge base revision. MAX SAT problem is NP-hard Some algorithms can solve this problem, but they are not adapted to the special cases where the number of variables is larger than the number of clauses. Usually, the number of variables has great impact on the efficiency of these algorithms. Thus, a polynomial-time algorithm is proposed to reduce the number of variables. Let T be any instance of the MAX SAT problem. The algorithm transforms T into another instance P of which the number of variables is smaller than the number of clauses of T. Using other algorithms, the optimal solution to P can be found, and it can be used to construct the optimal solution of T. Therefore, this algorithm is an efficient preprocessing step.展开更多
当前基于神经网络的端到端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%。展开更多
基金Project supported by the National Key R&D Program of China(Grant Nos.2017YFA0303302 and 2018YFA0305602)the National Natural Science Foundation of China(Grant No.11921005)Shanghai Municipal Science and Technology Major Project,China(Grant No.2019SHZDZX01)。
文摘We present a quantum adiabatic algorithm for a set of quantum 2-satisfiability(Q2SAT)problem,which is a generalization of 2-satisfiability(2SAT)problem.For a Q2SAT problem,we construct the Hamiltonian which is similar to that of a Heisenberg chain.All the solutions of the given Q2SAT problem span the subspace of the degenerate ground states.The Hamiltonian is adiabatically evolved so that the system stays in the degenerate subspace.Our numerical results suggest that the time complexity of our algorithm is O(n^(3.9))for yielding non-trivial solutions for problems with the number of clauses m=dn(n-1)/2(d■0.1).We discuss the advantages of our algorithm over the known quantum and classical algorithms.
基金the National Natural Science Foundation of China (Grant Nos. 90207002, 90307017, 60773125 and 60676018)National Science Foundation (Grant Nos. CCR-0306298)+1 种基金China Postdoctoral Science Foundation (Grant No. KLH1202005)the Natural Science Foundation of Shanghai City (Grant No. 06ZR14016)
文摘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.
基金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.
基金Porject supported by the National Natural Science Foundation of China and by the National "863" Hi-Tech Program.
文摘Maximum satisfiability (MAX SAT) problem is an optimization version of the satisfiability (SAT) problem. This problem arises in certain applications in expert systems and knowledge base revision. MAX SAT problem is NP-hard Some algorithms can solve this problem, but they are not adapted to the special cases where the number of variables is larger than the number of clauses. Usually, the number of variables has great impact on the efficiency of these algorithms. Thus, a polynomial-time algorithm is proposed to reduce the number of variables. Let T be any instance of the MAX SAT problem. The algorithm transforms T into another instance P of which the number of variables is smaller than the number of clauses of T. Using other algorithms, the optimal solution to P can be found, and it can be used to construct the optimal solution of T. Therefore, this algorithm is an efficient preprocessing step.
