A Personal Perspective on SAT and CSP: Tractability, Complexity, Quantification, Proofs
- Speaker: Dr. Hubie Chen, Department of Computer Science and Information Systems, Birkbeck, University of London
- Date: Tuesday, 26 February 2019 from 17:00 to 18:00
- Location: Room 151
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.