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 (ESM) property. Whether it can be determinized 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 two simple algorithms for it with run time O(1.4423^n) and O(1.6181^n), where n is the number of vertices in the graph. We also show that unless the "Strong Exponential Time Hypothesis" (SETH) fails, there is no algorithm for CIS with run time O(1.4141^n). We show that without the equality predicate SAT(FO2) is in fact equivalent to CIS in succinct representation. This yields two algorithms for SAT(FO2) without the equality predicate with run time O(1.4423^{2^n}) and O(1.6181^{2^n}), where n is the number of predicates. To the best of our knowledge, these are the first exact algorithms for an NEXP-complete decidable logic with run time significantly lower than O(2^{2^n}). We also identify a few lower complexity fragments of FO2 which correspond to the tractable fragments of CIS. Similar to CIS, unless SETH fails, there is no algorithm for SAT(FO2) with run time O(1.4141^{2^n}). 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 with a small constant blow-up in the number of predicates. Finally, we also perform some small experiments which show that our approach is indeed more promising than the existing method (based on the ESM property). The experiments also show that although theoretically it has the worse run time, the second algorithm in general performs better than the first one.


翻译:我们重新审视了两个可变的逻辑的可变性问题, 以 SAT (FO 2) 表示, 并使用运行时间 O( 1.442) 和 O( 1. 181) 表示, 上界通常源自其众所周知的直观大小模型( ESM) 属性。 它能否被高效地确定是一个尚未解决的问题。 在本文中, 我们展示了一种不同的方法, 将它降为我们称之为“ 共解独立系统( CIS) ” 的新的图形理论问题。 我们显示, 独联体的平面( FO 2) 以简洁的表达方式为事实上, 以运行时间 O (1. 4423) 和 O( 1.6 181) 表示, 其中n 直径直径( 直径) 直径模型数为 N.

0
下载
关闭预览

相关内容

SAT是研究者关注命题可满足性问题的理论与应用的第一次年度会议。除了简单命题可满足性外,它还包括布尔优化(如MaxSAT和伪布尔(PB)约束)、量化布尔公式(QBF)、可满足性模理论(SMT)和约束规划(CP),用于与布尔级推理有明确联系的问题。官网链接:http://sat2019.tecnico.ulisboa.pt/
专知会员服务
15+阅读 · 2021年5月21日
专知会员服务
81+阅读 · 2021年5月10日
Fariz Darari简明《博弈论Game Theory》介绍,35页ppt
专知会员服务
110+阅读 · 2020年5月15日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
152+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
已删除
将门创投
3+阅读 · 2019年4月12日
Ray RLlib: Scalable 降龙十八掌
CreateAMind
9+阅读 · 2018年12月28日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
强化学习 cartpole_a3c
CreateAMind
9+阅读 · 2017年7月21日
Arxiv
0+阅读 · 2022年1月31日
Arxiv
0+阅读 · 2022年1月31日
Arxiv
0+阅读 · 2022年1月30日
VIP会员
相关资讯
已删除
将门创投
3+阅读 · 2019年4月12日
Ray RLlib: Scalable 降龙十八掌
CreateAMind
9+阅读 · 2018年12月28日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
强化学习 cartpole_a3c
CreateAMind
9+阅读 · 2017年7月21日
Top
微信扫码咨询专知VIP会员