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.