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.4423^n), O(1.6181^n) and O(1.3661^n), 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^(2^n)), O(1.6181^(2^n)) and O(1.3661^(2^n)), 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^(2^n)). We also identify a few lower complexity fragments of SAT(FO2) which 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.
翻译:我们用SAT( FO2) 重新审视了两种可变逻辑的相容性问题, 代之以已知为 NEXP 完整的 SAT (FO2) 。 上界通常源自其众所周知的“ 耗尽大小模型” 属性。 它能否被确定/ 调整有效仍是一个尚未解决的问题 。 在本文中, 我们提出了一个不同的方法, 将它降为我们称之为“ 有条件独立集” (CIS) 的新型图形理论问题 。 我们显示, 独联体是NP( FO2) 完整的, 并提出了三种简单的算法 : 确定性, 随机化为零复杂性, 随机化为零, 随机化为小规模的单向一面的错, 运行时间为 O( I. 4423 ) 。 O( 1.6 ) 18 e. ( ) r. ( N. ) 和 O( 1.36 ) 中, 最高级的O.