Abstract

The class of model checkingfor first-order formulas on sparse graphs has a complete problem with respectto fine-grained reductions, Orthogonal Vectors (OV) [GIKW17]. This work studiesextensions of this class or more lenient parameterizations. We consider classesobtained by allowing function symbols; first-order on ordered structures;adding various notions of transitive closure operations; and stratifications offirst-order properties by quantifier depth and variable complexity, rather thannumber of quantifiers. For some of these classes, OV is still a completeproblem, in that significant improvement for the entire class is equivalent tosignificant improvement for OV algorithms. For these classes, we can also usethe improved OV algorithm of [AWY15, CW16] to get moderate improvements onalgorithms for the entire class. For other classes, we show that model checkingbecomes harder than for first-order, under well-studied conjectures such asSETH. For other classes, we show hardness follows from weaker assumptions thanSETH.

Surprisingly, whether anextension increases the complexity of model checking seems independent ofwhether it increases the expressive power of the logic. For example, addingfunction 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 modelchecking, although it increases the logic’s expressive power.

Joint work with Russell Impagliazzo.

Time

12月27日（周四）14:00-15:00

Speaker

Jiawei Gao is aPhD student in University of California, San Diego. She is mainly interested infine-grained complexity.

Venue

信息管理与工程学院602室

上海财经大学（第三教学楼西侧）

上海市杨浦区武东路100号