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

在这个项目中，PI和他的团队研究了广泛使用的可满足性算法（SAT解算器）和证明复杂性之间的关系，目的是表征使用冲突导向子句学习的完整SAT解算器的证明强度。该项目还侧重于推导证明所需的运行时间和存储（空间）之间的内在权衡，以及这对SAT求解器的影响。SAT解算器是广泛应用中最重要和最有用的工具之一，从寻找约束下问题的解决方案到检查软件和硬件系统的正确性和安全性，在这些应用中，它们作为证明方法是必需的。该项目还将探索在解决特定计算问题时固有的资源权衡，例如计算顺序统计和使用高质量的纠错码对最坏情况的错误进行编码。这种纠错码在网络世界中变得越来越重要，因为对手可能会故意破坏网络流量。

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.