SHF: Small: MaPaMaP: Massively Parallel Solving of Math Problems

SHF：小型：MaPaMaP：数学问题的大规模并行解决

基本信息

批准号：
2006363
负责人：
Marienus Heule
金额：
$ 32.89万
依托单位：
Carnegie-Mellon University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2019
资助国家：
美国
起止时间：
2019-11-01 至 2023-09-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2006363&HistoricalAwards=false
关键词：
SHF Small MaPaMaP Massively Parallel

项目摘要

State-of-the-art automated theorem proving tools have been making progress on, and in some cases resolve, longstanding unsolved problems of mathematics like: can the positive integers be sorted into two buckets, so that neither bucket contains a Pythagorean triple (a solution to a^2+b^2=c^2), or can the points on the plane be colored 5 colors, so that every two points at distance 1 apart are colored differently? The same techniques are also crucial in industry to verify hardware and software. A key aspect of recent and future successes in mechanized mathematics is the use of massively parallel computation. Handling these computing resources carefully is vital to exploit their great potential. Sophisticated splitting heuristics and encodings are required to partition a given problem into many sub-problems that can be efficiently solved in parallel. Unfortunately, today the development of such heuristics depends predominantly on expert knowledge about this problem and on sensible manual optimization.This research offers advances towards automated construction of sophisticated heuristics, as well as improved encodings of commonly used mathematical operations. Apart from solving long-standing open problems automatically, the research intents to extract information from the solutions to acquire useful mathematical insights. Famous mathematical challenges like the Collatz conjecture and the Hadwiger-Nelson problem are motivating examples that are driving this work and they could help making this technology go mainstream. The investigators will involve both graduate and undergraduate students in this research.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

最先进的自动定理证明工具在解决长期未解决的数学问题上取得了进展，并在某些情况下解决了这些问题，例如：能否将正整数分类到两个桶中，以便两个桶都不包含毕达哥拉斯三元组（ a^2+b^2=c^2的解），或者可以将平面上的点着色为5种颜色，使得相距1的每两个点着色不同？同样的技术对于工业界验证硬件和软件也至关重要。机械化数学近期和未来成功的一个关键方面是大规模并行计算的使用。仔细处理这些计算资源对于挖掘其巨大潜力至关重要。需要复杂的分割启发式方法和编码来将给定问题划分为许多可以有效并行解决的子问题。不幸的是，如今这种启发式方法的发展主要取决于有关该问题的专家知识和明智的手动优化。这项研究为复杂启发式的自动构建以及常用数学运算的编码的改进提供了进展。除了自动解决长期存在的开放问题之外，该研究还旨在从解决方案中提取信息以获得有用的数学见解。 Collatz 猜想和 Hadwiger-Nelson 问题等著名的数学挑战正在激发推动这项工作的例子，它们可以帮助使这项技术成为主流。研究人员将让研究生和本科生参与这项研究。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

期刊论文数量（14）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

SAT Competition 2018

DOI：
10.3233/sat190120
发表时间：
2019-09
期刊：
J. Satisf. Boolean Model. Comput.
影响因子：
0
作者：
E. Hirsch;Daniel Le Berre;Laurent Simon;A. Balint;A. Belov;Matti Järvisalo;Marijn J. H. Heule;Daniel Diepold;Tomás Balyo
通讯作者：
E. Hirsch;Daniel Le Berre;Laurent Simon;A. Balint;A. Belov;Matti Järvisalo;Marijn J. H. Heule;Daniel Diepold;Tomás Balyo

Chinese Remainder Encoding for Hamiltonian Cycles

哈密顿循环的中文余数编码