AF: Small:Tradeoffs among Measures in Computational and Proof Complexity

AF：小：计算和证明复杂性措施之间的权衡

• 批准号: 1217099
• 负责人: Paul Beame
• 金额: $ 44万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-08-01 至 2016-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1217099&HistoricalAwards=false
• 关键词: AF; Small; Tradeoffs; among; Measures

In this project, the PI and his team study the relationship between widely-used satisfiability algorithms (SAT solvers) and the complexity of proofs, with the goal of characterizing the proof strength of complete SAT solvers that use conflict-directed clause learning. The project also focuses on the inherent tradeoffs between the running time and storage (space) required to derive proofs and the impact that this has on SAT solvers. SAT solvers are among the most important and useful tools in a wide range of applications, from finding solutions to problems under constraints to checking the correctness and safety of software and hardware systems where theirrole as methods of proof is required.This project will also explore resource tradeoffs inherent in solving specific computational problems such as computing order statistics and encoding data using good quality error-correcting codes that are resilient to worst-case errors. Such error-correcting codes are becoming increasingly important in a networked world in which adversaries may deliberately corrupt network traffic.

在这个项目中，PI及其团队研究了广泛使用的满足性算法（SAT求解器）与证明的复杂性之间的关系，目的是表征使用使用冲突定向子句学习的完整SAT求解器的证明强度。 该项目还重点关注运行时间和存储时间（空间）之间的固有权衡，以获得证据以及对SAT求解器的影响。 SAT solvers are among the most important and useful tools in a wide range of applications, from finding solutions to problems under constraints to checking the correctness and safety of software and hardware systems where theirrole as methods of proof is required.This project will also explore resource tradeoffs inherent in solving specific computational problems such as computing order statistics and encoding data using good quality error-correcting codes that are resilient to worst-case errors. 在对手可能故意破坏网络流量的网络世界中，这种错误纠正的代码变得越来越重要。