ACM通信
评论文章
当满足性求解满足符号计算
信贷:Ztarstock
长期以来，数学家一直对那些表现出非常好的组合特性的物体着迷。然而，通常很难确定是否存在满足给定组合特性的对象。有时，明确回答存在问题的唯一可行方法是简单地进行系统的搜索。一个著名的例子是四色定理-四种颜色足以用不同颜色的相邻区域对平面地图的区域进行着色的概念。3.自1977年以来，这个定理就被认为是正确的，但每个已知的证明都在某种程度上依赖于计算机计算。数学论证用于将反例的搜索减少到有限的情况，然后使用自定义编写的计算机程序对这些情况进行彻底检查，以排除任何反例。
关键的见解
在过去50年里，计算机科学家在开发通用程序方面取得了重大进展，这些程序可以自动解决各种数学问题。可满足性求解而且符号计算是计算机科学的两个重要分支，各自专门解决数学问题。这两个领域都有着悠久的历史，并产生了令人印象深刻的工具——前者是可满足性(SAT)求解器，后者是计算机代数系统(CASs)。最初，SAT求解器是用来解决逻辑问题的，而CASs是用来操作和简化代数表达式的工具。正如我们将看到的，这些工具已经在这些原始领域之外发现了大量的新应用程序。
尽管SAT和CAS在解决数学问题方面有共同的专长，但它们是独立发展的。1一般来说，SAT社区关注的是有效的搜索方法，而CAS社区关注的是有效的数学算法。最近，这两个社区开始进行跨界合作，比如sc广场项目。一个，2由于这些团体的见解在很大程度上是互补的，将他们结合在一起就产生了解决任何一个团体单独无法解决的问题的新方法，并在涉及非线性实数计算的问题上产生了进步，13线性整数运算,12和布尔多项式,28举几个例子。在本文中，我们将重点介绍我们自己对这个正在进行的项目的贡献——一个名为MathCheck的SAT和CAS混合系统b我们已经应用于图论中的数学问题，45有限的几何,5组合,9和数论。c，11
可满足性求解。SAT求解器是一个从布尔逻辑中解决可满足性问题的程序——给出一个合取规范形式的公式，是否有一个对其变量的赋值，使表达式为真?乍一看，SAT的求解者似乎与大多数数学家和工程师关心的问题无关。然而，在过去的几十年里，SAT解决的应用取得了惊人的进展43导致了SAT解题应用的惊人多样性——从生成或解决数独8软件验证30.和硬件设计。36这场“SAT革命”甚至导致了数十年前的数学问题的解决，比如布尔毕达哥拉斯的三重问题26以及第五个舒尔数的确定。25要解决这些问题，首先要将它们简化为布尔逻辑中的一组约束。为SAT求解者提供约束条件，使其搜索约束条件的解，并在不存在解时提供不存在证书。
问题中的搜索空间是巨大的，如果没有非常聪明和强大的搜索方法，永远无法穷尽地搜索。事实上，SAT求解器是目前唯一能够解决这些问题的工具，这说明了它们卓越的搜索能力。然而，SAT的解题者确实在某些问题上遇到了困难——尤其是那些解题者不知道的数学结构。
作为这一现象的一个简单例子，考虑以下问题:找到一种方法来放置n鸽子在n- 1个洞，因为每个洞只够容纳一只鸽子。稍作思考就会发现这个问题是无法解决的，这可以通过一个简单的计数论证来证明。这个问题也直接用布尔逻辑表示，但令人尴尬的是，众所周知，SAT求解器使用最直接的编码来解决它要花费大量的时间。23问题是，在还原到布尔逻辑的过程中，问题的数学上下文丢失了;SAT求解者根本没有意识到一个计数参数足以排除一个解的存在。在这种情况下，有额外的数学事实可以编码到布尔逻辑，并允许SAT求解者有效地表明问题是无法满足大n。然而，在许多问题中——比如我们在本文中考虑的问题——大大减少搜索空间的数学事实在布尔逻辑中不容易表达。似乎我们要么必须忽略数学事实，要么完全避免使用SAT解算器。
符号计算。CASs是一种可以操作和简化数学表达式和对象的程序。它们有着悠久的历史，通常包含广泛的数学主题的功能，包括多项式算术和因式分解、计算代数几何、算法数论、符号组合、符号积分和微分方程的解、精确线性代数和量词消去。大量的研究——包括1999年诺贝尔物理学奖d-依赖计算机代数系统的精确计算。例如，它们在开普勒1611年的猜想中发挥了重要作用，该猜想认为包裹球体的最有效方式是金字塔形。24这个证明使用了许多CAS功能，包括线性规划、全局非线性优化和区间算法。
数字使用识别工具进行野蛮推理可以搜索指数级大的干草堆。
CASs在解决具有大量结构的问题时特别有效，这些问题可以通过一种不需要借助于一般搜索的算法来解决。e正因如此，CASs在解决问题时往往效率更高。例如，许多CASs都有用于查找多项式分解因子的例程，这比通过一般搜索查找因子要快得多。CASs能够利用因式分解问题中固有的代数结构，从而避免进行一般性搜索的需要。
另一方面，CASs不像现代SAT求解器那样，典型地优化为带学习的搜索。1请注意，数学对象的搜索空间通常是指数大小的，这将很快压倒任何没有设计来应对这种巨大的空间。简单地说，在指数级的大海捞针中寻找一根针，需要专门设计的工具，以找到巧妙的方法，将搜索空间修剪到一个可管理的大小，这在传统上不是符号计算研究的领域。
两全其美。虽然SAT和CAS都被用于解决非常困难的数学问题，但它们在传统上一直是孤立应用的——SAT求解器应用于布尔约束问题，涉及巨大的搜索空间，而CASs应用于涉及最小搜索的复杂数学问题。虽然每种工具都能有效地解决各自领域的问题，但我们工作的一个驱动动机是有许多问题的解决方案需要在两个世界都有效。
2015年，Ábrahám提议将SAT和CAS世界的技术结合在一起，以便单独使用任一世界的技术来解决难以解决的问题。1独立地，MathCheck项目开始了，并通过改进一些图论猜想中最著名的边界，证明了这种组合的有效性。46然而，MathCheck的应用范围要广泛得多，在过去五年中，MathCheck已经解决了各种数学分支的问题。在本文的其余部分，我们将描述如何将MathCheck应用于有限几何和组合矩阵理论中的两个长期存在的问题。本文的灵感来自于Heule和Kullmann的《蛮力的科学》26它描述了SAT求解者如何使用“蛮力”推理来解决搜索空间巨大的问题。在这个框架中，SAT+CAS求解器的推理变得“不那么残酷”。
林的问题
Lam的问题的根源可以追溯到公元前300年，当时欧几里得定义了他认为具有几何特征的五个公设。虽然所有五个假设都被认为是显而易见的，但第五个或“平行”的假设明显比他的其他假设更复杂。2000多年来，这个问题一直困扰着一些数学家，他们多次尝试用欧几里得的其他公设来证明平行公设。
令人惊讶的是，直到19世纪人们才最终意识到这个任务是不可能的——因为有一些替代几何满足欧几里得的前四条公设，但平行公设却不成立。例如，这发生在投影平面中，它是点和线的集合，满足以下两个公理:
- 有一条直线通过任意两点。
- 任何两条线在唯一一点相交。
这些公理在图1．第一个公理在通常的欧几里得平面中成立，并在其中显示出来图1一个．第二个公理在通常的欧几里得平面中不成立——如果两条线是歪斜的(如图1 b)他们将相交在一个唯一的点上，但如果直线是平行的，它们根本不会相交，更不用说在一个唯一的点上了。为了弥补这种情况，通常的欧几里得平面可以用一条“无穷远的线”来扩大，在这条线上任何两条平行线将相交(如图1 c)．得到的结构同时满足公理(1)和公理(2)。
图1。投影平面公理的视觉演示
现在可以提出一个有趣的问题:还有其他结构也满足这些公理吗?例如，是否存在点数量有限的射影平面?有一些平凡的方法可以满足公理——例如，如果平面由一条包含每个点的直线组成。取消这些琐碎的例子，计数参数可以用来表明，如果一个有限投影平面存在，那么它包含相同数量的线和点，并且每个点位于相同数量的线。如果每个点都在n+ 1条线，那么这个平面就是有序的n它将包含精确n2+n+ 1分。确定投射平面的可能阶数集在200多年来一直是一个重要的数学兴趣，今天它仍然是一个主要的开放问题。
最多三个级的投射平面可以通过中所示的结构显式地可视化图2．通过检查，人们可以验证这样的公理:任意两点位于一条唯一的直线上，任意两条直线相交于一个唯一的点。有些人可能会抗议说，这些平面中的“线”不一定用直线表示——但只要这些线满足公理，我们可以用任何方式来画它们!
图2。1-3阶投影平面的视觉描述。每个点和线都用单独的颜色绘制。
图3演示了小的秩序，其中投影平面是已知的存在。立即跳出来的是投影平面做一般以小阶存在，除了在阶6，当一个投影平面包含43个点。这个订单有什么特别之处吗?1949年，Bruck和Ryser证明了如果射影平面的阶为n≡1,2 (mod 4) thenn必须是两个整数平方和。14由于6满足同余条件，但不是两个平方和，因此6阶射影平面不存在。然而，Bruck-Ryser定理不能用来排除10阶，因为10是两个平方和(32和12)．这个案例吸引了大量的兴趣，因为10阶的射影平面是未知的——然而没有人知道为什么它不存在的理论原因。林的问题是要解决这个难题并确定如何正确地完成缺失的条目吗图3．
图3。关于射影平面存在顺序为10级的摘要。Lam的问题是确定一个10阶的投影平面是否存在。
一个计算的解决方案。林的问题最终在20世纪80年代末得到了解决，他使用了一个复杂的案件分解和大量的计算来分别搜索每个案件。32没有找到解的情况，从而否定了10阶射影平面的存在。
这种分解是基于与一个假设的10阶投影平面相关联的二进制纠错码必须满足的性质。这个代码是从射影平面派生出来的关联矩阵-{0,1}-矩阵包含1在其(我，j)第一个条目确切地当我这条线与jth点(见图4)．一个码字是关联矩阵行空间(mod 2)中的一个{0,1}向量，码字的权重是它有多少非零项。通过一些强有力的编码理论定理分析这些码字的性质，可以发现10阶投影平面必须产生至少一个15、16或19权重的码字，从而将搜索分为三种情况。
图4。二阶射影平面的关联矩阵。
重量15的案子在1973年在一台大型计算机上用了几个小时就解决了，351986年，在一台超级计算机上使用了2000小时，解决了重量16的问题33在超级计算机上工作100个小时，151989年解决了重量19的问题在超级计算机上用了2万小时在超级计算机上用了2000小时。34这些搜索是使用专门为每种情况编写的代码执行的，作者承认，错误是切实可能的。源代码是不公开的，即使它们是公开的，它们被设计为在不再生产的专门计算机上运行。要相信兰姆的问题实际上已经解决，我们现在必须解决一个不同的和严重的问题——如何验证这些搜索?
漫画林:32我想强调的是，这只是一个实验结果，迫切需要独立的验证。
一个新的希望。可满足性检验和符号计算领域的发展为Lam的问题提供了希望，可以更有效地解决，也可以解决到更高的严格标准。这是因为SAT解算器——尽管是复杂的软件——经过了良好的测试，并产生了证书，允许他们的结果被外部证书验证者验证。这意味着不再需要相信复杂搜索算法的实现。相反，只需要信任证书验证器。
自然地，SAT解算器将被用作“组合主力”，在每个可能的情况下搜索一个投影平面。但是CAS在搜索中有什么用呢?为了回答这个问题，想象你有一个草堆，你知道它的左右两边是完全对称的。如果你想在这堆草堆里找到一根针，一个绝妙的主意是把草堆从中间分开，只搜索一边——因为左边的东西会出现在右边，反之亦然。
同样的推理也适用于更普遍的情况。当在搜索空间中检测到对称时，理想情况下应该将搜索空间分割并简化为单个非对称分量。在许多由SAT求解者解决的问题中25，26这是通过引入额外的“对称破缺”约束来实现的，它阻止SAT求解器探索搜索空间的相同部分。这种添加“静态”约束的方法要求预先知道阻塞的对称，并且当存在一组能够阻塞这些对称的简洁约束时，这种方法的效果最好。不幸的是，Lam的问题包含了一些复杂的对称性，不太容易阻止。然而，如果在搜索过程中可以检测到这些对称性，那么就有可能动态地阻止它们，这种方法已经成功地应用于各种SAT求解器中。18，38，42计算对称性是CASs擅长的事情之一——包括Lam问题中出现的复杂对称性。因此，SAT+CAS系统非常适合利用SAT求解器和CASs的优势。
SAT求解器和CAS如何沟通?基本的联系概述在图5．当SAT求解器搜索时，它会找到“部分”投影平面——在某些点上满足投影平面约束的结构。这些被提供给CAS, CAS将返回额外的对称阻塞约束，从搜索空间中移除其他部分投影平面(与被发现的对称)。
图5。概述用于搜索投影平面的SAT+CAS方法。SAT求解器为CAS提供了一个局部投影平面，用于计算存在的对称性。这个例子展示了将部分平面旋转180度的对称性。
这种连接的灵感来自Davis-Putnam-Logemann-Loveland DPLL(T)算法39用一阶逻辑T-solver替换为CAS。该连接还利用了现代SAT求解器使用的冲突驱动子句学习，因为在生成阻塞约束后，它形成了一个冲突SAT求解器可以用来控制搜索应该回溯多少。我们强调这种联系是非常普遍的，可以应用于除对称破缺(我们将讨论)之外的许多其他情况。的确，CASs的优势之一是其大量的数学功能——可以利用这些功能来学习SAT解算器无法了解的各种数学事实。这也使得SAT+CAS方法比“SAT模理论”(SMT)求解器应用于更广泛的问题，这些求解器也类似于使用DPLL(T)算法。然而，SMT求解器通常仅限于解决固定数量的理论(如整数理论、实数理论或字符串理论)中指定的问题。
SAT+CAS的有效性。与以前的方法相比，SAT+CAS方法的有效性如何?权重15搜索在1973年首次被解决35已经被至少四个独立的实现所证实，其中一些需要在现代桌面上运行80分钟。6据我们所知，之前最快的实现使用了高度优化的C代码，大约需要30秒才能完成。16使用一个简单的SAT简化方法可以在大约6分钟内用一个现代的SAT求解器解决这个问题——已经比一些搜索更快了专门写执行此搜索。这说明了现代SAT求解器的效率，因为搜索空间的数学分析揭示了许多SAT求解器忽略的对称性。使用一个SAT+CAS解算器来做这个(如描述图5)搜寻工作大约在7秒内完成，这是目前最快的接近速度。6
与权重15搜索相比，权重16搜索涉及的内容明显更多，搜索空间也更大。权重16搜索空间中的大部分对称性可以通过理论手段进行分析，并通过将搜索分解为十个不同的情况来去除。然而，在某些情况下，它们的搜索空间中仍然有超过1000个对称，这很难处理——当CAS可以检测和删除这些对称时，会导致运行时间的显著加快。在1986年完成对该空间的全面搜索之后，15，33我们只知道一个单独的先前的独立确认:一个使用CAS库的优化的C实现37在2011年，这需要16000个小时的台式机集群。41相比之下，去除CAS对称性的SAT方法可以在30小时内解决这个问题。5
权重19搜索甚至比权重16搜索更复杂，而且是继1989年的穷举搜索之后34据我们所知，唯一的独立确认在2011年需要19000小时。41这个案件的第一步是将搜索分为大约65万个不同的案件。之前基于CAS的搜索需要大约7个小时来完成初始化步骤，而我们基于sat的不需要CAS对称破缺的方法需要62个小时。加入CAS对称破缺后，计算速度提高了150倍，初始化在25分钟内完成。不幸的是，在初始化步骤之后，搜索空间通常不是很对称，这意味着我们不能期望通过对称破缺来实现很大的加速。即便如此，在没有任何专门的搜索算法的情况下，SAT+CAS方法在大约16000小时内完成了搜索4比2011年确认兰姆问题时使用的专用代码在相同硬件上的基准测试平均快25%。
SAT+CAS方法的最后一个优点是求解器产生的证书可以由独立的一方进行验证。他们只需要相信SAT编码和cas生成的约束——而不是用来生成证书的实际程序。这并不能证明我们的搜索是没有错误的，但确实大大降低了必要的信任程度。对于缺乏正式证明的“实验”结果，这是一个特别重要的考虑因素，因为我们几乎可以肯定定制编写的程序包含bug。这不是对作者的轻视，而是软件开发的一个简单现实:如果没有广泛的正式验证，即使是使用最良好和测试最良好的软件也不可能没有bug。
事实上，我们的搜索发现了之前几次搜索中的错误，包括1989年的最初搜索和2011年的确认。当这些搜索的中间结果(例如，声称不存在一个部分解决方案)与SAT求解器发现的部分解决方案相矛盾时，可以检测到错误。例如，2011年对权重15的确认是基于对51列部分投影平面的不存在的证明，而51列部分投影平面实际上是存在的，并且在图6．请注意，很容易检查这样的矩阵实际上是一个部分投影平面，因为每一列包含相同数量的1，并且任何两个不同的列在相同的位置共享一个1。
图6。一个51列的部分投影平面以前声称不存在。红色项表示预先知道的1s，蓝色项表示由MathCheck确定的1s。
总之，SAT+CAS方法在Lam的问题中工作得很好，因为它允许使用现代SAT求解器强大的搜索例程来搜索投影平面，同时允许计算机代数系统揭示的数学特性来极大地限制搜索空间。此外，它消除了编写定制的特殊用途搜索算法的需要，因此最终使执行搜索成为一个更直接和可信的过程。
威廉姆森猜想
接下来，我们讨论了SAT+CAS方法对组合矩阵理论的一些影响。我们从一个激励人心的例子开始:假设你需要通过一个嘈杂的信道与某人交流。换句话说，您发送的数据可能不是接收到的数据。怎样才能提高收件人完全恢复原始信息的可能性呢?一种方法是首先使用一组你和你的收件人事先同意的编码词来编码你的信息。由于码字在发送时可能被损坏，因此选择尽可能不同的码字是有意义的。例如，如果你有n长度的二进制码字n你可以尝试最大化码字的最小两两汉明距离。编码理论中的普罗金约束40这个最小距离不能严格大于n/ 2。在某些情况下，有可能达到这个界限并找到一个集合n长度的二进制码字n使任何两个不同码字的汉明距离是精确的n/ 2。
在这种情况下，可以方便地将二进制码字表示为{±1}向量。然后是两个码字的长度n汉明距离为n/2，当它们是正交向量和n这种成对汉明距离为的码字n/2形式的矩阵行一个使得非对角元素AAT为零。这样的矩阵称为阿达玛矩阵1893年，法国数学家雅克·哈达玛研究了它们。22尽管它们已经被广泛研究了125年，但关于它们还有许多悬而未决的问题——我们甚至还不知道它们存在的所有顺序。阿达玛能够证明，如果一个阿达玛矩阵的阶大于2，那么它的阶一定是4的倍数。的阿达玛猜想这个必要条件也是充分的。
由于阿达玛猜想的证明还没有到来，数学家和计算机科学家已经用尽可能多的顺序构建了阿达玛矩阵;目前n= 167是4阶阿达玛矩阵的最小情况n尚不清楚。因为一般的哈达玛矩阵的搜索空间是如此巨大，所以专注于有更多结构可以利用的特殊结构是有意义的。数学家约翰·威廉姆森(John Williamson)在1944年提出了一个这样的结构。44在这个构造中，我们有四个对称的{±1}-矩阵一个，B，C，D的订单n为了简单起见，我们假设它是循环的(每一行都是前一行的循环移位)。如果一个2+B2+C2+D2单位矩阵是4的倍数吗n然后是4阶的阿达玛矩阵n存在并显式地呈现在图7．在这种情况下，矩阵一个，B，C，D被称为威廉姆森矩阵集。
图7。通过威廉姆森结构构造的阿达玛矩阵的一般形式。
20世纪60年代，NASA喷气推进实验室(Jet Propulsion Laboratory)的科学家在开发航天器通信代码时，发现了第一组23阶威廉姆森矩阵，并推测威廉姆森矩阵对于所有的值都存在n。21这个猜想在1993年被证明是错误的，当时有一个反例n= 35是通过计算机穷举搜索得到的。19当时人们注意到，这是最小的奇数反例，但对偶数阶知之甚少——尽管威廉姆森自己发现了一些偶数阶的例子，包括2的所有幂次n= 32。他表示有兴趣证明一个存在性定理，这个定理可以推广这种模式，但他无法这样做。2的下一个幂的搜索空间n= 64超出了计算搜索的可行性范围，因此在75年的时间里，64阶Williamson矩阵是否存在是未知的。
一个坐在+ CAS的解决方案。MathCheck能够极大地提高我们对Williamson矩阵的知识，通过在许多阶中穷尽搜索Williamson矩阵n≤70(见图8一个例子)。两个直接的惊喜被发现了:首先，威廉姆森矩阵存在于所有偶数阶中n≤70(包括n= 64)，其次，当威廉姆森矩阵的顺序可以被2的大幂整除时，威廉姆森矩阵会更加丰富。例如，单是64阶的Williamson矩阵就有超过70000组，而在所有奇阶到64阶的Williamson矩阵则少于100组。此外，对64阶Williamson矩阵结构的分析揭示了一个可以推广到2的所有幂的结构。因此，由于MathCheck的搜索结果，我们改进了Williamson的结果:2阶Williamson矩阵k存在与k≤5;我们现在知道这种形式的威廉姆森矩阵实际上对所有人都存在k．10这些结果提出了Williamson矩阵存在于所有偶阶的可能性，这被称为甚至威廉姆森猜想。
图8。由一组70阶威廉姆森矩阵生成的280阶哈达玛矩阵。彩色项代表1，白色项代表-1。
由于威廉姆森矩阵的算术定义关系可以用简单的算术电路直接编码，所以SAT求解器可以用于搜索威廉姆森矩阵。然而，这种编码完全不能与特殊用途的解算器竞争，最多可以达到30左右。7特殊用途求解器更有效的原因是，它们可以利用威廉姆森矩阵已知满足的数学性质。其中一个例子就是功率谱密度PSD的条件。
j·威廉姆森:44确定这篇论文的结果是孤立的结果还是某些一般定理的特殊情况将是有趣的。
简单地说，就是向量的PSDX= (X0、……Xn－1的离散傅里叶变换的模的平方向量X。换句话说kPSD(X)是
ω是一个基元n单位方根。令人惊讶的是,如果一个为Williamson矩阵的第一行，则PSD(一个)最多4个n。这是一个非常有用的条件，因为绝大多数{±1}-向量都不满足它——因此利用它可以极大地减少搜索空间的大小。当然，问题在于SAT求解器对PSD值是什么没有概念，而且这个条件不容易编码到布尔逻辑中。
然而，CASs擅长使用快速傅里叶变换计算PSD值。因此，当一个SAT求解器发现一个它认为可能出现在一组威廉姆森矩阵中的矩阵时，它可以将这个矩阵提供给CAS。CAS检查是否可以使用PSD条件排除它，如果可以，因为矩阵的第一行的PSD值大于4n-然后将矩阵从搜索空间中移除。SAT解算器将继续搜索满足约束条件的矩阵，直到找到一组威廉姆森矩阵，或者能够证明在给定的顺序中不存在威廉姆森矩阵。这种通用方法在图9．
图9。SAT+CAS方法用于搜索威廉姆森矩阵的概述。当提供给CAS的矩阵的PSD值太大时，它将被阻塞。
使用PSD滤波的SAT+CAS方法轻松优于单独使用SAT求解器或单独使用CASs的方法，特别是在大的阶数中，SAT+CAS方法可以更快地执行数量级。970阶Williamson矩阵的搜索空间大小约为24 (70/2)≈1042让人惊讶的是，这样的空间竟然能被搜索到详尽。但是，使用SAT求解器的强大搜索例程，再加上CASs中提供的复杂数学能力(以及一些额外的强大过滤标准)20.)使得这个搜索可以在现代CPU上轻松完成，用时不到1000小时。威廉森猜想的最小反例(n= 35)可以在几分钟内验证。
结论
将SAT求解器的搜索能力与CASs的表达能力和丰富的数学知识相结合，将其与CASs的数学约束相结合，可以有效地搜索由数学约束指定的大空间。虽然在这篇概述中，我们关注的是有限几何和组合数学的应用，但这种范式是相当通用的，我们也使用Math-Check来改进图论中猜想的已知界45和数论。11图论和数论应用程序提供了更多依赖于CAS功能的可能性，如旅行销售人员求解器、最短路径求解器和非线性实际优化器。最近，我们使用MathCheck导出了Kochen-Specker系统大小的一个新的下界——一个来自量子力学的对象，用来证明“自由意志定理”，即如果人类有自由意志，那么基本粒子也有自由意志。
用SAT+CAS方法解决的问题有两个主要特点。首先，这个问题在某种程度上是“布尔化”的——换句话说，搜索空间的很大一部分可以用布尔逻辑指定，从而允许利用SAT求解器的搜索能力。第二，有一些数学属性、定理或不变量不能轻易地在布尔逻辑中指定，但可以显著地减少搜索空间的大小。这些约束在CAS的驾驶室中完美地存在，正如我们所看到的，它们可以显著地提高求解器的效率。最重要的是，它们不局限于数学的任何一个分支，事实上，SAT+CAS方法已经被应用于各种令人惊讶的问题，比如密码分析，27程序合成,29和电路验证。31这些应用程序以及由SC-square项目等项目开创的应用程序17使我们相信SAT+CAS方法将会伴随我们很长一段时间——解决比我们以前认为可能的更大的问题。
致谢我们感谢审稿人的深刻评论。3阶投影平面的可视化是基于一个最初由Petr Vojtchovský提出的表示。
参考文献
1.在符号计算和可满足性检查之间建立桥梁。在2015年ACM论文集实习生。计算机协会。符号和代数计算, 2015年1 - 6。美国林惇,艾德。
2.Ábrahám, E.，等。SC2:当满足性检查和符号计算结合时。G.和Traytel, D.编辑。在学报1圣实习生。自动化推理工作坊:挑战、应用、方向、示范成果。计算机工程学报，2017,6 - 10。
3.Appel, K.和Haken, W.每个平面地图都有四种颜色。第一部分:卸货。伊利诺斯州J.数学， 3(1977)， 429-490。
4.Bright, C.，张，K.， Stevens, B.， Kotsireas, I.，和Ganesh, V.基于sat的Lam问题的解决方案。在35年的会议记录th人工智能研讨会, 2021, 3669 - 3676。
5.Bright, C.，张，K.， Stevens, B.， Kotsireas, I.，和Ganesh, V.在Lam问题中权重16码字的不可满足性证明。在29年的会议记录th实习生。关于人工智能的联合声明, 2020, 1460 - 1466。
6.Bright, C.，张，K.， Stevens, B.， Roy, D.， Kotsireas, I.， and Ganesh, V.关于权重为15码字的10阶投影平面的不存在证明。工程、通信和计算中的应用代数， 3(2020)， 195-213。
7.Bright, C.， Ganesh, V.， Heinle, A.， Kotsireas, I.， Nejati, S.，和Czarnecki, K. MathCheck2:组合猜想的SAT+CAS验证器。在十八届立法会会议记录th实习生。科学计算中的计算机代数研讨会, 2016, 117 - 133。V. Gerdt, W. Koepf, W. Seiler和E. Vorozhtsov编。施普林格。
8.Bright, C.， Gerhard, J.， Kotsireas, I.和Ganesh, V.有效的问题解决使用SAT解决程序。枫叶在数学教育与研究，公社。计算机与信息科学,(2020), 205 - 219。施普林格。
9.Bright, C.， Kotsireas, I.和Ganesh, V.将计算机代数系统与SAT解算器应用于Williamson猜想。J.符号计算100(2020), 187 - 209。
10.Bright, C.， Kotsireas, I.和Ganesh, V.新的无限完美四元数序列和Williamson序列。IEEE反式。论信息论66， 12(2020)， 7739-7751。
11.Bright, C.， Kotsireas, I.， Heinle, A.，和Ganesh, V. Complex Golay配对长度为28:通过计算机代数和程序SAT的搜索。J.符号计算102(2021), 153 - 172。
12.一个完整的和终止的线性整数求解方法。J.符号计算100(2020年9月),102 - 136。
13.Brown, C.和Vale-Enriquez, F.从简化到非线性实多项式约束的部分理论解算器。J.符号计算100(2020年9月),72 - 101。
14.Bruck, R.和Ryser, H.有限投影平面的不存在性。加拿大J.数学1， 1(1949)， 88-93。
15.卡特,J。关于十阶射影平面的存在性。博士论文，加州大学伯克利分校，1974年。
16.关于10阶射影平面上最大6弧的不存在性。在25年的海报会议上th实习生。组合算法研讨会，2014。
17.Davenport, J.， England, M.， Griggio, A.， Sturm, T.和Tinelli, C.符号计算和可满足性检验。J.符号计算100(2020年9月),1 - 10。
18.Devriendt, J.， Bogaerts, B.和Bruynooghe, M.对称解释学习:SAT的有效动态对称处理2017年sat合格性测试理论与应用。施普林格实习生。2017年出版,83 - 100。
19.Doković， D. Williamson阶矩阵n为n= 33, 35, 39。离散数学115， 1-3(1993)， 267-271。
20.Doković， D.和Kotsireas, I.周期互补序列的压缩及其应用。设计、密码和密码学， 2(2015)， 365-377。
21.葛洛姆(S.)和鲍默特(L.)。《美国数学月刊， 1(1963)， 12-17。
22.阿达玛，J. Résolution d'une question relatiaux déterminants。科学公报数学， 1(1893)， 240-246。
23.哈肯:解决问题的难处。理论计算机39(1985), 297 - 308。
24.黑尔，T.和弗格森，S。开普勒猜想:黑尔斯-弗格森证明。施普林格科学与商业媒体，2011。
25.Heule, M. Schur五号。在32届会议的会议记录nd人工智能研讨会, 2018, 6598 - 6606。S. McIlraith和K. Weinberger编。AAAI出版社。
26.Heule, M.和Kullmann, O.:蛮力的科学。Commun。ACM 60， 8(2017)， 70-79。
27.密码分析的代数和逻辑求解方法，Horáček，;博士学位论文。帕绍大学，2020年。
28.Horáček, J.和Kreuzer, M.关于从CNF到ANF的转换。J.符号计算100(2020年9月),164 - 186。
29.高珊珊，孔珊珊，杨晓燕，杨晓燕，杨晓燕。基于数值优化的SAT求解方法，2018;arXiv: 1802.04408。
30.Jhala, R.和Majumdar, R.软件模型检查。ACM计算调查414(2009), 1-54。
31.考夫曼博士，Biere博士，和考尔斯博士，SAT，计算机代数，乘数。5th和6th计算机领域EPiC系列的吸血鬼工作坊71。L. Kovács和A. Voronkov编。安乐椅,2020队。
32.10阶有限投影平面的搜索。《美国数学月刊， 1(1991)， 305-318。
33.Lam, C.， Thiel, L.和Swiercz, S. 10阶投影平面中权重为16的码字的不存在性。42 .《组合理论， 2(1986)， 207-214。
34.林，林，Thiel, L.和Swiercz, S. 10阶有限射影平面的不存在性。加拿大J.数学41， 6(1989)， 1117-1123。
35.关于10阶射影平面的存在性。组合理论A系列， 1(1973)， 66-78。
36.马奎斯-席尔瓦，J.， Sakallah, K.布尔电子设计自动化的可满足性。在37年的会议记录th年度设计自动化会议。, 2000, 675 - 680。
37.McKay, B.和Piperno, A.实用图同构，2。J.符号计算60(2014年1月),页94 - 112。
38.Metin, H.， Baarir, S.， Colange, M.和Kordon, F. CDCLSym:在SAT求解中引入有效的对称破缺。构建和分析系统的工具和算法。施普林格实习生。2018年出版,99 - 114。
39.Nieuwenhuis, R.， Oliveras, A.和Tinelli, C.求解SAT和SAT模理论:从一个抽象的Davis-Putnam-Logemann-Loveland过程到DPLL(T)．j . ACM 53， 6(2006)， 937-977。
40.指定最小距离的二进制代码。愤怒的反式。论信息论6， 4(1960)， 445-450。
41.10阶投影平面的不存在性的确认。硕士论文，卡尔顿大学，2011年。
42.Sabharwal, a . SymChaff:利用结构感知的满足度求解器中的对称性。约束14,4(2008年10月)，478-505。
43.布尔可满足性:理论与工程。Commun。ACM 57， 3(2014)， 5。
44.威廉森，J.哈达玛的行列式定理和四平方和。杜克数学J. 11， 1(1944)， 65-81。
45.Zulkoski, E.， Bright, C.， Heinle, A.， Kotsireas, I.， Czarnecki, K.， and Ganesh, V.结合SAT求解器和计算机代数系统来验证组合猜想。J.自动推理， 3(2017)， 313-339。
46.Zulkoski, E.， Ganesh, V.和Czarnecki, K. MathCheck:通过计算机代数系统和SAT解算器的组合的数学助手。在A. Felty和A. Middeldorp, eds。在25年的会议记录th实习生。自动扣费确认;计算机科学讲义9195(2015), 607 - 622。施普林格。
脚注
c.关于SAT+CAS范例的更多应用，请参阅概述文章17刊登在特刊上符号计算学报致力于SAT和CAS的协同作用。
数字图书馆是由计算机协会出版的。版权所有©2022 ACM股份有限公司
没有发现记录