| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | January 8, 2020 |
| Latest Amendment Date: | January 8, 2020 |
| Award Number: | 2015445 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Pavithra Prabhakar
pprabhak@nsf.gov (703)292-2585 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | November 2, 2019 |
| End Date: | February 29, 2024 (Estimated) |
| Total Intended Award Amount: | $500,000.00 |
| Total Awarded Amount to Date: | $500,000.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
5000 FORBES AVE PITTSBURGH PA US 15213-3815 (412)268-8746 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
5000 Fornes Ave WQED Bldg Pittsburgh PA US 15213-3815 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | Software & Hardware Foundation |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
The key to automating activities that are traditionally performed by humans, such as assembly-line work or organizational tasks, is to break these activities down into numerous simple steps that can be handled easily. While this approach has also been used to automate logical reasoning, breaking reasoning tasks into overly simple steps has two important shortcomings. First, it can prevent today's methods from solving some seemingly easy problems. Second, a long sequence of these simple steps is often impossible to understand for humans. This project explores a novel approach to automated reasoning that deals with this issue by allowing more elaborate, but also understandable, steps.
Over half a century, research regarding reasoning systems has centered on the existence of short arguments that could in theory be found by computers, without addressing the issue of how to actually find these arguments in practice. The novel reasoning systems studied in this project aim at automatically finding arguments that are usually used by mathematicians, in particular arguments "without loss of generality," which can be automated efficiently. The main goals of the research are (1) solving problems that are too hard for existing reasoning techniques, (2) producing short arguments for problems for which we only have gigantic arguments, and (3) learning from the results of automated reasoning.
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.
PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH
Note:
When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external
site maintained by the publisher. Some full text articles may not yet be available without a
charge during the embargo (administrative interval).
Some links on this page may take you to non-federal websites. Their policies may differ from
this site.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
Automated reasoning has become a powerful technology for solving a wide array of problems in both industry and academia, including hardware and software verification, planning, and tackling long-standing mathematical challenges. Despite its success, automated reasoning presents an intriguing challenge: while modern tools can manage massive real-world problems, they often struggle with seemingly simple ones. This poor performance is frequently due to the reliance on reasoning techniques that only learn logically implied facts. Recently, new reasoning systems have been developed to address this issue by learning facts that, while not logically implied, preserve "satisfaction". Preserving satisfaction means that if solutions exist for a problem, then one will remain after the learning process, although the shape of solutions and their quantity may be impacted. Remarkably, these new reasoning systems are exceptionally powerful, even without introducing new definitions. New definitions are the cornerstone of compact proofs found in proof-complexity literature.
The project achieved three major milestones in the field of "without-loss-of-satisfaction" reasoning: solving a mathematical challenge, theoretically analyzing the reasoning systems, and making the technology accessible to a broader audience. First, the research team solved a decades-old mathematical problem known as the packing chromatic number of the infinite square grid. Although various researchers had made progress on this problem using automated reasoning tools over the past decade, the final solution remained out of reach. The breakthrough occurred when without-loss-of-satisfaction reasoning was applied, reducing computational costs by a factor of 100. Second, the team thoroughly analyzed the landscape of these new reasoning systems, providing valuable insights into their relative strengths and weaknesses. Third, a preprocessing tool was developed to make without-loss-of-satisfaction reasoning accessible to anyone using automated reasoning tools. This tool was submitted to the premier international automated reasoning competition, where it proved to be the crucial technology behind the winning solver.
Last Modified: 06/08/2024
Modified by: Marienus Heule
Please report errors in award information by writing to: awardsearch@nsf.gov.
