做网站互联网公司有哪些,2024很有可能再次封城吗,网络建设规范和网络维护管理规范属于,北京公司电话大全黄页 摘要#xff1a;布尔可满足性问题#xff08;Boolean Satisfiability Problem#xff0c;简称SAT问题#xff09;是逻辑学和计算机科学中的一个问题#xff0c;它的目的是确定是否存在一种解释#xff0c;使给定的布尔公式成立。换句话说#xff0c;它询问给定布尔公… 摘要布尔可满足性问题Boolean Satisfiability Problem简称SAT问题是逻辑学和计算机科学中的一个问题它的目的是确定是否存在一种解释使给定的布尔公式成立。换句话说它询问给定布尔公式的变量是否可以被一致地替换为真值或假值使公式求值为真。如果是这样那么这个公式就是可满足的。另一方面如果不存在这样的赋值那么该公式所表示的函数对于所有可能的变量赋值都为假该公式不可满足1。 追根溯源SAT是第一个已知的NP-Complete问题多伦多大学的Stephen Cook在1971年国家科学院的Leonid Levin在1973年均独立证明了这一问题。在此之前NP-Complete问题的概念甚至不存在。另外证明显示复杂性类NP中的每个决策问题都可以简化为CNF公式的SAT问题有时也称为“CNFSAT”。
值得注意的是SAT问题是计算机科学领域最基本的问题之一有着重要的理论意义和实际应用。在理论研究中SAT问题是一个经典的判定问题同样是第一个被证明为NP-Complete的问题。这个决策问题在包括理论计算机科学、复杂性理论、算法、密码学和人工智能等计算机科学的各个领域都至关重要。
在现实场景应用中SAT是很多工业场景里面的核心工具。尤其在一些包括芯片测试、电路等价性验证、电路模型检测、智慧园区及无线设备的布局、操作系统、航空等对精确度要求很高的核心领域都需要SAT求解器的重磅参与。例如芯片SAT分析是一种系统级应用测试分析方法通过对芯片的性能和可靠性进行全面的测试和分析以评估芯片在实际应用中的表现。
另外在腾讯地图中的语音序列调度中采用SAT算法中的约束加权方法播报失败率从6.20%可降至2.85%降幅54%同时把地图路网更新的内存消耗量降低一半更新周期缩短一半。
5月16日北京玻色量子科技有限公司以下简称“玻色量子”在新品发布会上推出的100量子比特相干光量子计算机真机——“天工量子大脑”旨在快速、且高效地求解NP难的组合优化问题尤其是Ising问题。而布尔可满足性(SAT)和最大可满足性(Max-SAT)是NP-Complete问题和NP难问题的一类两者同等重要且更切合实际的组合优化问题。
目前求解布尔SAT的方法有很多比如量子退火和经典的随机局部搜索(SLS)求解器。然而它们都需要巨量步骤来解决困难的SAT问题这将耗费大量的时间和精力。随着量子计算技术的发展一个SAT问题可以转化为一个Ising/QUBO问题从而可由玻色量子的“天工量子大脑”快速高效地求出全局最优解。
那么为了更清楚的理解SAT问题下面首先介绍一些基本术语。
基本定义和术语
SAT问题简单地说就是确定是否存在满足给定布尔公式解释的问题它需要判断给定布尔公式的变量是否可以一致地替换为值 TRUE 或 FALSE以使公式的计算结果为 TRUE。如果是这种情况则公式称为“满足”。否则若不存在这样的赋值则公式表示的函数对于所有可能的变量赋值都是 FALSE并且公式是不满足的。例如公式“a AND NOT b”是可以满足的因为可以找到值a TRUE和b FALSE这使得a AND NOT b TRUE。相反“a AND NOT a”是无法被满足的因为找不到这样的a的值。
命题逻辑公式也称为布尔表达式由变量运算符AND连接也用∧表示、OR分离∨、NOT否定¬和括号构成。如果通过为其变量分配适当的逻辑值即TRUEFALSE可以使公式为TRUE则称该公式是可满足的。给定公式布尔可满足性问题SAT是检查它是否可满足。
布尔可满足性问题有几种特殊情况其中公式需要具有特定结构。文字是一个变量称为正文字或变量的否定称为负文字。子句是文字或单个文字的分离。如果一个子句最多包含一个正文字则该子句称为Horn子句。如果公式是条款或单个子句的连接则公式为合取范式CNF。
例如x1是正文字¬x2是负文字x1∨¬x2是子句x1∨¬x2∧¬x1∨x2∨x3∧x1是联合范式的公式它的第一和第三个条款是Horn条款但它的第二个条款不是。
最大可满足性问题Max-SAT是确定给定布尔公式以合取范式表示中最多有多少个子句可以通过对公式变量赋真值来使其成立。它是布尔可满足性问题的推广后者询问是否存在一种真值赋值使所有子句都成立。
问题描述
2-SAT和3-SAT问题是SAT问题的两种形式它们的区别在于每个子句中包含的变量数量不同。
具体来说2-SAT问题中每个子句最多包含两个变量形如(a∨b)、¬a∨c等其中∨表示逻辑或¬表示逻辑非。而3-SAT问题中每个子句最多包含三个变量形如(a∨¬b∨c)、(¬a∨b∨¬c)等。
因为2-SAT问题中每个子句最多包含两个变量所以可以使用一些特殊的算法如Kosaraju算法和Tarjan算法在多项式时间内求解。而3-SAT问题则是NP-Complete问题目前还没有已知的多项式时间算法可以解决。由于二元变量存在0/1或者-1/1表达形式的区别常见模型有两种建模思路在这里分别进行说明。
建模思路一
我们以Max 2-SAT问题进行讨论将文字表示为0/1的变量建立QUBO模型。每个子句由两个文字组成如果其中一个或两个文字都为真则满足一个子句。对于这个问题有三种可能的子句类型每一种都有一个传统的约束如果子句是真的则必须满足。
下面是三种常见的转换情况
① 无负文字
例如(xi∨xj)
传统约束(xixj)≥1
QUBO惩罚项(1-xi-xjxixj)
② 一个负文字
例如xi∨¬xj
传统约束xi¬xj≥1
QUBO惩罚项xj-xixj)
③ 两个负文字
例如¬xi∨¬xj
传统约束¬xi¬xj≥1
QUBO惩罚项xixj
注由于变量xj为1/0所以¬xj1-xj
对于每个子句类型如果满足传统约束则对应的惩罚等于0如果不满足传统约束则二次惩罚等于1。给定这种一一对应的关系我们可以通过等价地最小化不满足的子句数量来逼近子句数量最大化问题。通过这种形式我们可以构建一个QUBO模型。
所以对于给定的Max 2-SAT算例我们可以添加与问题子句相关的二次惩罚项得到一个我们想要最小化的复合惩罚函数。由于惩罚项均为二次型因此该惩罚函数采用QUBO模型形式min yxTQx。如果在最小化QUBO模型时等于零这意味着我们有一个满足所有子句的解如果等于5这意味着我们有一个满足除5以外的所有子句的解。
我们用以下4个变量和12个子句的例子来说明这个算例的建模和求解过程。 将惩罚项加在一起给出了我们的QUBO模型表达式
min y3x1-2x4-x2x3x2x42x3x4 (1)
或QUBO模型的矩阵形式 min y3xTQx (2)
则Q矩阵表达为 求解这个QUBO模型可以得到y3-21其中x1x2x30x41。意思是除一个子句外的所有子句都满足。
注上述QUBO方法已在Kochenberger等人的研究中得到成功应用[2]研究解决了含有数百个变量和数千个子句的Max 2-SAT问题。这种方法求解Max 2-SAT问题的一个有趣的特点是得到的待求解QUBO模型的大小与问题中的子句数无关仅由变量的个数决定。因此一个含有200个变量和30000个子句的Max 2-SAT问题可以建模为一个只含有200个变量的QUBO模型并求解。
建模思路二
为了更好地理解这个问题我们将文字表示为-1/1的变量继续讨论一个3-Sat问题。 我们讨论一个3-Sat子句
x1∨x2∨x3
该子句通过引入-1/1辅助变量可以映射成二次函数 在x0x1x2的任意取值中都有一个使得K最小的值a。如果我们假设a总是被设置为这个最优值那么除了x0x1x2-1时能量为1外其他取值的最低能量都是-7。下表总结了有关变量的取值其中加粗的数字是给定x0x1x2变量的最低可能能量。 使用这种方法如果xi在子句中被否定我们可以通过将xi替换为-xi来编码任意3-Sat子句。现在如果我们对求和这些每个子句对应的二次函数我们可以得到一个关于Nxi自旋变量和Maj辅助自旋的二次函数从而得到一个大小为NM的Ising/QUBO问题。如果该问题是可满足的那么最小的Ising能量将是-7M如果该问题是不可满足的问题那么最小的Ising能量为-7Msat其中Msat是可满足子句的个数。
问题拓展
MAX-SAT是最大可满足性问题是SAT问题的推广。它要求最大数量的条款任何转让都可以满足。它具有有效的近似算法但是NP时间难以精确解决。
在量子计算领域2023年6月NTT最新的研究提出了一种相干SAT求解器(CSS)的新技术。使用图形处理器(GPU)实现的Cyber-CSS与现有的SLS求解器(如probSAT)相比有一定的竞争力。未来通过量子计算实现SAT问题的快速求解将成为一种新的有效方法。
如今玻色量子已基于自研的相干光量子计算机真机——“天工量子大脑”在SAT问题求解上具有显著的算力优势代表了其在NP-Complete问题上的实用性以进一步拓展更多可实用化量子计算应用场景。
玻色量子还将启动“燎原计划”开发者平台并持续对外开放“天工量子大脑”的真机测试热忱欢迎更多不同领域的研究伙伴前来了解相干量子计算的原理和能力在此基础上展开共同研发用量子计算去解决更多真实场景中的问题让量子计算的超强算力能真正服务于各行各业满足未来时代对于计算的需求。 [参考文献]
[1] Glover, Fred, Kochenberger, Gary, Du, Yu. Quantum Bridge Analytics I: a tutorial on formulating and using QUBO models[J]. 4OR: Quarterly Journal of the Belgian, French and Italian Operations Research Societies,2019,17(4):335-371. DOI:10.1007/s10288-019-00424-y.
[2] Kochenberger G , Glover F , Alidaee B ,et al.Using the unconstrained quadratic program to model and solve Max 2-SAT problems[J].International Journal of Operational Research, 2005, 1(1/2):89--100.DOI:10.1504/IJOR.2005.007435.
[3] Reifenstein S, Leleu T, McKenna T, et al. Coherent SAT solvers: a tutorial[J]. Advances in Optics and Photonics, 2023, 15(2): 385-441.
[4] 百度百科
https://baike.baidu.com/item/%E5%B8%83%E5%B0%94%E5%8F%AF%E6%BB%A1%E8%B6%B3%E6%80%A7%E9%97%AE%E9%A2%98/4715567?fraladdin
