Towards a more efficient approach for the satisfiability of two-variable logic

We revisit the satisfiability problem for two-variable logic, denoted by SAT(FO
²
), 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
ⁿ
), O(1.6181
ⁿ
) and O(1.3661
ⁿ
), respectively.We then show that without the equality predicate SAT(FO
²
) is in fact equivalent to CIS in succinct representation. This yields the same three simple algorithms as above for SAT(FO
²
) without the the equality predicate with run time O(1.4423
⁽²ⁿ⁾
), O(1.6181
⁽²ⁿ⁾
) and O(1.3661
⁽²ⁿ⁾
), 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
⁽²ⁿ⁾
). We also identify a few lower complexity fragments of FO
²
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.