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.

0
下载
关闭预览

相关内容

SAT是研究者关注命题可满足性问题的理论与应用的第一次年度会议。除了简单命题可满足性外,它还包括布尔优化(如MaxSAT和伪布尔(PB)约束)、量化布尔公式(QBF)、可满足性模理论(SMT)和约束规划(CP),用于与布尔级推理有明确联系的问题。官网链接:http://sat2019.tecnico.ulisboa.pt/
【CVPR2021】用于目标检测的通用实例蒸馏
专知会员服务
23+阅读 · 2021年3月22日
商业数据分析,39页ppt
专知会员服务
159+阅读 · 2020年6月2日
因果图,Causal Graphs,52页ppt
专知会员服务
246+阅读 · 2020年4月19日
《DeepGCNs: Making GCNs Go as Deep as CNNs》
专知会员服务
30+阅读 · 2019年10月17日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
carla 学习笔记
CreateAMind
9+阅读 · 2018年2月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
Arxiv
0+阅读 · 2021年6月16日
Arxiv
0+阅读 · 2021年6月16日
Logically-Constrained Reinforcement Learning
Arxiv
3+阅读 · 2018年12月6日
VIP会员
相关资讯
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
carla 学习笔记
CreateAMind
9+阅读 · 2018年2月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
Top
微信扫码咨询专知VIP会员