A personal perspective on SAT and CSP: tractability, complexity, quantification, proofs

Hubie Chen, Birkbeck, University of London. Part of the Algebra, Logic, and Algorithms Seminar Series.

I will give a guided, personal tour of some theoretical results on the classical satisfiability problem (SAT), the constraint satisfaction problem (CSP), and their quantified versions.  In particular, I will study the impact of the variable interactions on the complexity; here, the graph-theoretic measure of treewidth, and generalizations thereof, play a key role.  In this context, I will also present results on the existence of proofs certifying unsatisfiability of problem instances.  Parallels between the quantified and non-quantified cases will be highlighted, and open problems and directions will be offered.  I will end with a general discussion of proof systems and proof complexity for QBF, the quantified version of SAT.