一句话：将双变量逻辑可满足性归约为条件独立集问题，并给出首个显著优于 O(2^{2n}) 的确定/随机算法。
双变量逻辑 SAT(FO2) 已知为 NEXP 完全，其上界通常来自指数模型性质，高效确定化/随机化仍是开放问题。本文将其归约到新图论问题“条件独立集”（CIS），证明 CIS 为 NP 完全，并给出确定性、零错误随机和小单侧错误随机三个简单算法，运行时间分别为 O(1.4423^n)、O(1.6181^n)、O(1.3661^n)。在无等词谓词时 SAT(FO2) 与 CIS 的简洁表示等价，对应得到 O(1.4423^{2n})、O(1.6181^{2n})、O(1.3661^{2n}) 的算法（n 为谓词数），这是首个对 NEXP 完全可判定逻辑显著低于 O(2^{2n}) 的确定性/随机算法。作者还识别了对应 CIS 易解片段的低复杂度 FO2 片段，并对含等词片段给出到无等词片段的线性时间多一归约。
We revisit the satisfiability problem for two-variable logic, denoted by SAT(FO2), which is known to be NEXP-complete. The upper bound is usually derived from its well known exponential size model property. Whether it can be determinized/randomized efficiently is still an open question.In this paper we present a different approach by reducing it to a novel graph-theoretic problem that we call Conditional Independent Set (CIS). We show that CIS is NP-complete and present three simple algorithms for it: Deterministic, randomized with zero error and randomized with small one-sided error, with run time O(1.4423n), O(1.6181n) and O(1.3661n), respectively.We then show that without the equality predicate SAT(FO2) is in fact equivalent to CIS in succinct representation. This yields the same three simple algorithms as above for SAT(FO2) without the the equality predicate with run time O(1.4423(2n)), O(1.6181(2n)) and O(1.3661(2n)), respectively, where n is the number of predicates in the input formula. To the best of our knowledge, these are the first deterministic/randomized algorithms for an NEXP-complete decidable logic with time complexity significantly lower than O(2(2n)). We also identify a few lower complexity fragments of FO2which correspond to the tractable fragments of CIS.For the fragment with the equality predicate, we present a linear time many-one reduction to the fragment without the equality predicate. The reduction yields equi-satisfiable formulas and incurs a small constant blow-up in the number of predicates.
DOI 原文 ·
@inproceedings{paperbot6220,
title = {Towards a more efficient approach for the satisfiability of two-variable logic},
author = {Ting-Wei Lin and Chia-Hsuan Lu and Tony Tan},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470502}
}