Abstract
I will describe prior and current work on connecting the art of finding good satisfiability algorithms with the art of proving complexity lower bounds: proofs of limitations on what problems can be solved by good algorithms. Surprisingly, even minor algorithmic progress on solving the circuit satisfiability problem faster than exhaustive search can be applied to prove strong circuit complexity lower bounds. These connections have made it possible to prove new complexity lower bounds that had long been conjectured, and they suggest concrete directions for further progress.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Williams, R.: Improving exhaustive search implies superpolynomial lower bounds. In: ACM Symposium on Theory of Computing, pp. 231–240 (2010)
Williams, R.: Non-uniform ACC circuit lower bounds. To appear in IEEE Conference on Computational Complexity (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Williams, R. (2011). Connecting SAT Algorithms and Complexity Lower Bounds. In: Sakallah, K.A., Simon, L. (eds) Theory and Applications of Satisfiability Testing - SAT 2011. SAT 2011. Lecture Notes in Computer Science, vol 6695. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21581-0_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-21581-0_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21580-3
Online ISBN: 978-3-642-21581-0
eBook Packages: Computer ScienceComputer Science (R0)