2018-12-27 | Jiawei Gao:The Fine-Grained Complexity of Strengthenings of First-Order Logic

2018-12-27   


Abstract

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) [GIKW17]. This work 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 the improved OV algorithm of [AWY15, CW16] 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.

 

Time

1227日(周四)14:00-15:00

 

Speaker

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

 

Venue

信息管理与工程学院602

上海财经大学(第三教学楼西侧)

上海市杨浦区武东路100