Complexity of Satisfiability Problems
University of Hanover, Germany.
The problem to decide if a given propositional formula is satistiable is the classical NP-complete problem, whose study has influenced computational complexity theory in a tremendous way. It is common folklore that certain syntactically restricted formula classes allow efficient algorithms to test satisfiability. Lewis in the 1980s parameterized the problem SAT by a finite set B of propositional connectives, i.e., SAT(B) is the satisfiability problem for propositional formulas with connectives only from B. He then classified the complexity of SAT(B) as a function of B.
In this talk we will introduce a general approach to the study of algorithmic problems such as the above for propositional formulas and Boolean circuits. We will consider satisfiability and model checking problems for (fragments of) temporal logics, non-monotonic logics, dependence logic, etc., and outline some recent results.