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 求解器是各种应用中最重要和最有用的工具之一，从寻找约束下问题的解决方案到检查需要其作为证明方法的软件和硬件系统的正确性和安全性。该项目还将探索解决特定计算问题时固有的资源权衡，例如计算顺序统计和使用能够抵御最坏情况错误的高质量纠错码对数据进行编码。 这种纠错码在网络世界中变得越来越重要，在网络世界中，对手可能会故意破坏网络流量。