Hubie Chen, Birkbeck University of London
A Personal Perspective on SAT and CSP: Tractability, Complexity, Quantification, Proofs
Departmental Seminar: a talk for everyone giving a good introduction to a topic.
I will give a guided, personal tour of some theoretical results on SAT, 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 QBF proof systems and proof complexity.