The class of model checking for first-order formulas on sparse graphs has a complete problem with respect to fine-grained reductions, Orthogonal Vectors (OV) In this talk, we studies extensions of this class or more lenient parameterizations We consider classes obtained by allowing function symbols; first-order on ordered structures; adding various notions of transitive closure operations; and stratifications of first-order properties by quantifier depth and variable complexity, rather than number of quantifiers For some of these classes, OV is still a complete problem, in that significant improvement for the entire class is equivalent to significant improvement for OV algorithms For these classes, we can also use an improved OV algorithm to get moderate improvements on algorithms for the entire class For other classes, we show that model checking becomes harder than for first-order, under well-studied conjectures such as SETH For other classes, we show hardness follows from weaker assumptions than SETH Surprisingly, whether an extension increases the complexity of model checking seems independent of whether it increases the expressive power of the logic For example, adding function symbols does not change which problems are expressible by first-order, but does increase the time for model checking under SETH On the other hand, adding an ordering does not change the fine-grained complexity of model checking, although it increases the logic’s expressive power Joint work with Russell Impagliazzo

Jiawei Gao is a Ph.D. student in University of California, San Diego. She is mainly interested in fine-grained complexity.