权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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的每两个点的颜色不同？同样的技术在工业中也是验证硬件和软件的关键。机械化数学最近和未来成功的一个关键方面是大规模并行计算的使用。小心处理这些计算资源对于开发其巨大潜力至关重要。复杂的分裂算法和编码需要将给定的问题划分为许多子问题，这些子问题可以并行有效地解决。不幸的是，今天的发展，这样的算法主要取决于专家知识，这个问题和明智的手动optimization.This研究提供了先进的自动化建设的复杂算法，以及改进的编码常用的数学运算。除了自动解决长期存在的开放问题外，该研究还打算从解决方案中提取信息，以获得有用的数学见解。著名的数学挑战，如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

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