A personal perspective on SAT and CSP: tractability, complexity, quantification, proofs
- Date: Wednesday 13 March 2019, 16:00 – 17:00
- Location: Mathematics Level 8, MALL 1, School of Mathematics
- Type: Algebra, Logic and Algorithms, Seminars, Pure Mathematics
- Cost: Free
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.