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

University Of Washington, Seattle WA

Investigators

Abstract

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 their role 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.