https://scholars.lib.ntu.edu.tw/handle/123456789/607475
標題: | Towards a more efficient approach for the satisfiability of two-variable logic | 作者: | Lin T.-W Lu C.-H TONY TAN |
關鍵字: | Graph theory;Temporal logic;Graph-theoretic problem;Independent set;Lower complexity;Reduction yield;Satisfiability problems;SIMPLE algorithm;Succinct representation;Time complexity;Computer circuits | 公開日期: | 2021 | 卷: | 2021-June | 來源出版物: | Proceedings - Symposium on Logic in Computer Science | 摘要: | 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 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. ? 2021 IEEE. |
URI: | https://www.scopus.com/inward/record.uri?eid=2-s2.0-85113895281&doi=10.1109%2fLICS52264.2021.9470502&partnerID=40&md5=5b28f49994b3b14cba073d9eb2f2cd11 https://scholars.lib.ntu.edu.tw/handle/123456789/607475 |
ISSN: | 10436871 | DOI: | 10.1109/LICS52264.2021.9470502 |
顯示於: | 資訊工程學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。